The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I am stuck in a proof that involves a dependent rewrite (I think) -- I  
need to rewrite two variables simulatenously in order to complete the  
proof. Unfortunately, dependent rewrite gives the error

  "User error: Cannot find a well-typed generalization of the goal  
that makes the proof progress"

Here is a simplified stand-alone script that demonstrates the problem:

Require Import Arith.
Require Import Omega.
Require Import JMeq.
Require Import EqdepFacts.

Inductive T : nat -> Set := MkT : forall (n:nat), T n.
Variable U : nat.

Definition a : T U := MkT U.

Lemma foo : U + 1 - 1 = U.
Proof.
 omega.
Qed.

Definition b : T (U + 1 - 1).
Proof.
 rewrite foo.
 exact (MkT U).
Defined.

Lemma a_is_b : JMeq a b.
Proof.
  generalize b ; intro b'.
  dependent inversion b'.
  unfold a.
  rewrite foo.
  apply JMeq_refl.
Qed.

Inductive X : forall (n:nat), T n -> Set := .

Lemma bar : X (U + 1 - 1) b = X U a.
Proof.
  (* now what? *)

It seems that if we can simultaneously rewrite (U + 1 - 1) to U and b  
to a then we're done. However, a simple

Proof.
  dependent rewrite foo.

Gives the error mentioned above. Explicitly constructing an existT  
lemma gets us a little further:

Proof.
  cut (existT T (U + 1 - 1) b = existT T U a) ; intros.
  dependent rewrite H ; auto.

But now we are left to prove

  existT T (U + 1 - 1) b = existT T U a

Based on SearchAbout(existT), The only introduction for existT is  
eq_dep_eq_sigT, leaving

  eq_dep nat T (U + 1 - 1) b U a

But now I'm really stuck. None of the facts about eq_dep seem to be  
helpful. There is one fact relating eq_dep and JMeq, which looks very  
promising -- we need to relate it to lemma a_is_b after all. However,  
that lemma is too specific (requires Type rather than *a* Type such as  
nat).

Can anyone help?

Edsko