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
