The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

Hello all,

I recently ran into what I think is the situation described here:

    
http://coq.inria.fr/cocorico/Induction%20over%20a%20type%20containing%20pairs

Though it was a little different.  Here's a fragment of a global/thread-local
semantics equivalence proof:

    Definition state := nat -> nat.
    Inductive expr :=
      | Read : nat -> expr
      | Lit : nat -> expr.
    Inductive label :=
      | lRead : nat -> nat -> label.
    Inductive top : label -> expr -> expr -> Prop :=
      | tRead : forall n v, top (lRead n v) (Read n) (Lit v).
    Inductive op : state * expr -> state * expr -> Prop :=
      | oRead : forall s n, op (s, Read n) (s, Lit (s n)).

We can define our communication semantics in two ways:

    Inductive cop : state * expr -> state * expr -> Prop :=
      | cRead : forall e e' n s l, l = lRead n (s n) -> top l e e' -> cop (s, 
e) (s, e').

    Inductive cop' : (state * expr) -> (state * expr) -> Prop :=
      | cRead' : forall e e' n s, top (lRead n (s n)) e e' -> cop' (s, e) (s, 
e').

In the first case, the proof goes through; in the second case, it fails.

    Lemma cop_op : forall se se', cop se se' -> op se se'.
      induction 1. destruct H0. injection H. intros. rewrite H0. rewrite H1. 
apply oRead.
    Qed.

    Lemma cop'_op : forall se se', cop' se se' -> op se se'.
      induction 1. destruct H.
    Abort.

Based on the Cocorico page, I expect the way to prevent 'destruct' from
throwing away useful info is to rewrite H into a form using all primitive
variables (though the specific incant eludes me).  But now I wonder why I
wouldn't just write all my inductive propositions like cop and not like cop'
(except maybe aesthetic reasons.)

Question: Is this the same thing? Is the cop definition reasonable, or
should I fix things in proof land? Why does Coq have this limitation?

Cheers,
Edward