Hi Chun, I don't think your example captures the distinction, since, as you prove, AList and BList are the same.
you're right about > 1. [] is List > and > 2. If l = h::t and t is List, then l is List. In fact the only subset satisfying these (which is therefore both the least and the greatest) is the set of all lists. Think instead about Hol_reln `P (SUC n) ==> P n` ; (* no numbers *) Hol_coreln `Q (SUC n) ==> Q n` ; (* all numbers *) Cheers, Jeremy On 20/01/17 22:07, Chun Tian (binghe) wrote: > Hi Michael, > > It took me some time to think about your words and learn co-induction. > I'm no expert, but I don't agree with the opinion that "leastness is > captured by the induction principle". Here is my argument: > > 1. Your "AList" definition must come from the following Hol_reln definition: > > val (AList_rules, AList_ind, AList_cases) = Hol_reln > `(!l. (l = []) ==> isAList l) /\ > (!l h t. (l = h::t) /\ isAList t ==> isAList l)`; > > because the generated AList_cases is exactly the same as the one you gave: > > val AList_cases = > |- ∀a0. isAList a0 ⇔ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isAList t: > thm > > val AList_ind = > |- ∀isAList'. > (∀l. (l = []) ⇒ isAList' l) ∧ > (∀l h t. (l = h::t) ∧ isAList' t ⇒ isAList' l) ⇒ > ∀a0. isAList a0 ⇒ isAList' a0: > thm > > val AList_rules = > |- (∀l. (l = []) ⇒ isAList l) ∧ > ∀l h t. (l = h::t) ∧ isAList t ⇒ isAList l: > thm > > 2. You're right that, an co-induction of the same relation (or we should > say, the same rules), would give us the same cases theorem, so let me > define it with a different name, BList: > > val (BList_rules, BList_coind, BList_cases) = Hol_coreln > `(!l. (l = []) ==> isBList l) /\ > (!l h t. (l = h::t) /\ isBList t ==> isBList l)`; > > it generated the following things: > > val BList_cases = > |- ∀a0. isBList a0 ⇔ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isBList t: > thm > > val BList_coind = > |- ∀isBList'. > (∀a0. isBList' a0 ⇒ (a0 = []) ∨ ∃h t. (a0 = h::t) ∧ isBList' t) ⇒ > ∀a0. isBList' a0 ⇒ isBList a0: > thm > > val BList_rules = > |- (∀l. (l = []) ⇒ isBList l) ∧ > ∀l h t. (l = h::t) ∧ isBList t ⇒ isBList l: > thm > > 3. Now I can formally prove AList and BList is really the same thing > (!l. isBList l = isAList l): > > val A2B = store_thm ("A2B", ``!l. isAList l ==> isBList l``, > HO_MATCH_MP_TAC AList_ind > >> RW_TAC bool_ss [BList_rules]); > > val B2A = store_thm ("B2A", ``!l. isBList l ==> isAList l``, > Induct > >| [ RW_TAC bool_ss [AList_rules, BList_rules], > STRIP_TAC > >> ONCE_REWRITE_TAC [BList_cases] > >> ONCE_REWRITE_TAC [AList_cases] > >> REPEAT STRIP_TAC > >| [ ASM_REWRITE_TAC [], > SIMP_TAC list_ss [] > >> `t = l` by PROVE_TAC [CONS_11] > >> PROVE_TAC [] ] ]); > > val AB_same = store_thm ("AB_same", ``!l. isBList l = isAList l``, > PROVE_TAC [A2B, B2A]); > > now I want to say AList_ind and BList_coind are actually derived from > the same rules for the same relation, they themselves didn't show any > essential characteristics of the defined object (AList or BList here). > > P. S. This sounds like we could have another stronger Hol_reln (or > Hol_coreln), which could return both induction and coinduction theorems > at the same time for the same given rules. > > 4. So where are the words "least" and "maximal" coming from inductive > and coinductive definitions? I think for the *same* relation we can > always define it using either inductive or coinductive ways: > > (Inductive) A "List" is defined as the least subset of HOL type "list", > such that: > > 1. [] is List > and > 2. If l = h::t and t is List, then l is List. > > The defined concept "List" is the interaction of all 1-ary relation > satisfying above property. Consider the extreme case: List = (\l. T) > also satisfy above property. > > (Co-inductive) A "List" is defined as the maximal (greatest) subset of > HOL type "list", such that: > > If l is List, then > 1. l is [] > or > 2. ?h t. (l = h::t and t is List) > > The defined concept "List" is the union of all 1-ary relation satisfying > above property. Consider the extreme case: List = (\l. F) also satisfy > above property. > > Both Hol_reln and Hol_coreln only accept the inductive approach when > defining any relation, that is, conjunction clauses having "==> R x y" > as the conclusion part. Thus, we must *always* understand these rules as > the *least* relation satisfying the rules. > > As for the purpose of induction theorems and co-induction theorems, I > think they help us to prove different kinds of theorems on relations. > Watching the position of "P l" in the conclusion part of these > (co)induction theorems: > > val AList_ind = > |- ∀P. > (∀l. l = [] ⇒ P l) ∧ > (∀l. (∀h t. l = h::t ∧ P t) ⇒ P l) ⇒ > ∀l. isAList l ⇒ P l: > thm > > val BList_coind = > |- ∀P. > (∀l. P l ⇒ l = [] ∨ (∃h t. l = h::t ∧ P t)) ⇒ > ∀l. P l ⇒ isBList l: > thm > > Suppose I have a 1-ary relation (or predicate) about "Man". The > induction theorem could help us to prove something like: > > If x is a Man, then ... (e.g. x is an animal) > > (Most of time we want to prove this kind of theorems using the defined > relation) while the co-induction theorem could help us to prove things like: > > If ... (e.g. x is John), then x is a Man. > > Also recall in Wikipedia's "Coinduction" page [1], it says "As a > definition or specification, coinduction describes how an object may be > "observed", "broken down" or "destructed" into simpler objects. As a > proof technique, it may be used to show that an equation is satisfied by > all possible implementations of such a specification." (keyword: > specification) > > [1] https://en.wikipedia.org/wiki/Coinduction > > Comments are welcome ... > > Regards, > > Chun Tian > > > On 19 January 2017 at 00:23, <michael.norr...@data61.csiro.au > <mailto:michael.norr...@data61.csiro.au>> wrote: > > Note that the cases theorem does not capture “leastness”. A > coinductive definition of the same relation would give you the same > cases theorem. The cases theorem is just giving you the fix-point > property. ____ > > __ __ > > One easy example for thinking about these sorts of things is lists. > Imagine you have:____ > > __ __ > > isAList l ól = [] \/ ?h t. l = h::t /\ isAList t____ > > __ __ > > (where l ranges over a type large enough to encompass lists and lazy > lists both, and the isAList predicate is identifying the appropriate > subsets of that type).____ > > __ __ > > If the cases theorem is true for algebraic and co-algebraic lists > then leastness and greatness must be captured elsewhere. In fact, > leastness is captured by the induction principle which says____ > > __ __ > > P [] /\ (!h t. P t ==> P(h::t)) ==> !l. isAList l ==> P l____ > > __ __ > > Michael____ > > __ __ > > __ __ > > *From: *"Chun Tian (binghe)" <binghe.l...@gmail.com > <mailto:binghe.l...@gmail.com>> > *Date: *Wednesday, 18 January 2017 at 21:58 > *To: *hol-info <hol-info@lists.sourceforge.net > <mailto:hol-info@lists.sourceforge.net>> > *Subject: *[Hol-info] How to prove this theorem about relations?____ > > __ __ > > Hi, ____ > > __ __ > > Sorry for disturbing again, but I met new difficulties when proving > theorems about relations.____ > > __ __ > > Suppose I have the following simple recursive datatype and a "sub > formula" relation about it:____ > > __ __ > > val _ = Datatype `form = atom 'a | dot form form`;____ > > __ __ > > val (subF_rules, subF_ind, subF_cases) = Hol_reln____ > > `(!(A:'a form). subF A A) /\____ > > (!(A:'a form) B C. subF A B ==> subF A (dot B C)) `;____ > > __ __ > > Now I need to prove this goal: `!A a. subF A (atom a) ==> (A = atom > a)`.____ > > __ __ > > I have successfully proved some theorems about relations defined by > Hol_reln, but this one brings some difficulties that I never met > before.____ > > __ __ > > The main problem is, "atom" never appears in the definition of > Hol_reln, thus I don't have any theorem talking about it.____ > > __ __ > > But I recall the fact that, an inductive relation defines the > *least* relation satisfying the rules, thus anything undefined is by > default false. I believe this fact has been correctly captured by > (and only by) subF_cases generated from above Hol_reln definition:____ > > __ __ > > val subF_cases =____ > > |- ∀a0 a1. subF a0 a1 ⇔ (a1 = a0) ∨ ∃B C. (a1 = dot B C) ∧ subF > a0 B:____ > > thm____ > > __ __ > > If I do cases analysis on `A`, I got a seeming good start point:____ > > __ __ > > > e (Cases_on `A:'a form`);____ > > OK..____ > > 2 subgoals:____ > > val it =____ > > ∀a. subF (dot f f0) (atom a) ⇒ (dot f f0 = atom a)____ > > ∀a'. subF (atom a) (atom a') ⇒ (atom a = atom a')____ > > 2 subgoals____ > > : proof____ > > __ __ > > But I still don't know how to prove any of these sub-goals. I have > no useful theorems for rewrite or anything else. The relation rules > only tells me that, forall A, (subFor A A) is true, but it didn't > say anything about the other direction: (subF A B) => A = B (if A > and B are both shapes like (atom ...)____ > > __ __ > > Also, I even don't know how to prove this fundamental truth about > datatypes: ``(atom A) = (atom B) ==> A = B``, again, I have no > theorems to use ... because the Datatype definition didn't return > anything that I can (directly) use inside a store_thm().____ > > __ __ > > On the other side, Coq proves the same theorem quite simply:____ > > __ __ > > Lemma subAt :____ > > forall (Atoms : Set) (A : Form Atoms) (at_ : Atoms),____ > > subFormula A (At at_) -> A = At at_.____ > > intros Atoms A at_ H.____ > > inversion H.____ > > reflexivity.____ > > Qed.____ > > __ __ > > Need help ...____ > > __ __ > > Regards,____ > > __ __ > > Chun Tian (binghe)____ > > University of Bologna (Italy)____ > > __ __ > > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info > <https://lists.sourceforge.net/lists/listinfo/hol-info> > > > > > -- > --- > > Chun Tian (binghe) > University of Bologna (Italy) > > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info