Lots of people have weighed in already, but another intuition is the
observation that an induction principle looks like:
P-satisfies-the-same-intro-rules-as-indR ==> (!x. indR x ==> P x)
Note that you can view the conclusion as
!x. x IN indR ==> x IN P
and then as
indR SUBSET P
And then it’s clear that the induction principle is saying that indR is smaller
than every other predicate satisfying the same introduction rules.
Conversely, the conclusion to the coinduction principle flips the arguments to
the implication, and so is clearly saying P SUBSET indR, or that indR is
biggest.
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Friday, 20 January 2017 at 22:07
To: "Norrish, Michael (Data61, Canberra City)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to prove this theorem about relations?
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
--
---
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
