Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Dependent rewrite question (probably simple answer! :)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dependent rewrite question (probably simple answer! :)


chronological Thread 
  • From: Edsko de Vries <devriese AT cs.tcd.ie>
  • To: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Dependent rewrite question (probably simple answer! :)
  • Date: Fri, 20 Feb 2009 14:05:05 +0000
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page