coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Dependent rewrite question (probably simple answer! :), Edsko de Vries
Archive powered by MhonArc 2.6.16.