(Here is the final part of my argument)
When a group of rules like ( .. ==> R x y) /\ ( ... ==> R x y) /\ ... are
used to defined a relation, either in HOL's Hol_reln or Hol_coreln, the
resulting relation should be always understood as the least relation
satisfying these rules, because the maximal relation (R x y = T) satisfy
the rules too. So leastness is NOT captured by R_rules.
Instead, the leastness is indeed captured by R_cases. It's this theorem (R
x y = ... \/ ... \/ ...) who guarantees relations like (R x y = T) doesn't
hold.
Induction and co-induction theorems only represent the general
(co)inductive principles and help us to prove theorems related to relation
(of which the leastness is already determined by R_cases).
And if the behavior of Hol_coreln is correct, I think it can be merged into
Hol_reln as well: just let Hol_reln generate the coinduction theorem too
but no need to return it explicitly, like the R_strongind theorem.
On 20 January 2017 at 12:07, Chun Tian (binghe) <binghe.l...@gmail.com>
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> 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>
>> *Date: *Wednesday, 18 January 2017 at 21:58
>> *To: *hol-info <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
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
> --
> ---
>
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
--
---
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
