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
