Using the co-induction principle. Q.prove ( `!n. Q n`, rw [] >> irule Q_coind >> qexists_tac `\x. T` >> rw []);
Scott > On 2017/01/20, at 17:10, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > > Hi, > > Well, I tried your definitions about P and Q, they still difference at only > the (co)induction theorems. So if we have: > > val (Q_rules, Q_coind, Q_cases) = Hol_coreln `Q (SUC n) ==> Q n` ; (* all > numbers *) > > how can we prove `!n. Q n` ? > > Regards, > > Chun > >> Il giorno 20 gen 2017, alle ore 14:26, Jeremy Dawson >> <jeremy.daw...@anu.edu.au> ha scritto: >> >> 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 > > ------------------------------------------------------------------------------ > 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