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)
------------------------------------------------------------------------------
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
