coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: "Edward Z. Yang" <ezyang AT mit.edu>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Induction/destruct over a type with extra structure, redux
- Date: Thu, 03 Nov 2011 16:27:13 -0400
Edward Z. Yang wrote:
OK, the problem is that in the full development I need the induction
hypothesis.
[...]
Inductive cop : state * expr -> state * expr -> Prop :=
| cTau : forall e e' s l, l = lTau -> top l e e' -> cop (s, e) (s, e')
| cRead : forall e e' n s l, l = lRead n (s n) -> top l e e' -> cop (s,
e) (s, e').
[...]
Lemma cop_op : forall se se', cop se se' -> op se se'.
destruct 1; induction H0; try inversion H; eauto.
Qed.
Inductive cop' : (state * expr) -> (state * expr) -> Prop :=
| cTau' : forall e e' s, top lTau e e' -> cop' (s, e) (s, e')
| cRead' : forall e e' n s, top (lRead n (s n)) e e' -> cop' (s, e) (s,
e').
Lemma cop'_op : forall se se', cop' se se' -> op se se'.
destruct 1; inversion H. apply oPlusL. subst.
Abort.
If you need induction, you shouldn't be writing [inversion]. ;)
This is a common issue that is usually solved by proving (inductively) lemmas with extra variables and equalities. In your example here, you could also prove [forall x y, cop' x y -> cop x y] and then derive [cop'_op] as an easy corollary of [cop_op].
- [Coq-Club] Induction/destruct over a type with extra structure, redux, Edward Z. Yang
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux,
Benedikt AHRENS
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux,
Edward Z. Yang
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux, Adam Chlipala
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux,
Edward Z. Yang
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux,
Benedikt AHRENS
Archive powered by MhonArc 2.6.16.