Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Induction/destruct over a type with extra structure, redux

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Induction/destruct over a type with extra structure, redux


chronological Thread 
  • 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].



Archive powered by MhonArc 2.6.16.

Top of Page