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
