coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <devriese AT cs.tcd.ie>
- To: Adam Chlipala <adamc AT hcoop.net>
- Cc: coq-club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Dependent rewrite question (probably simple answer! :)
- Date: Fri, 20 Feb 2009 15:57:16 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi Adam,
That was great! Thanks a million. Using chapter 9 from your book I could now finish the proof. For posteriority's sake, the completed script is below. By the way, are these axioms about equality implementable? Or does extraction become impossible when one of these axioms is used?
Require Import Arith.
Require Import Omega.
Require Import JMeq.
Require Import Eqdep.
Inductive T : nat -> Set :=
| MkT : forall (n:nat), T n
| MkT2 : forall (n:nat), T n.
Variable U : nat.
Definition a : T U := MkT U.
Lemma foo : U = U + 1 - 1.
Proof.
omega.
Qed.
Definition b : T (U + 1 - 1).
Proof.
rewrite <- foo.
exact (MkT U).
Defined.
Lemma a_is_b : JMeq a b.
Proof.
cbv beta delta -[minus plus].
generalize foo.
rewrite <- foo.
intros.
rewrite (UIP_refl _ _ e).
apply JMeq_refl.
Qed.
Inductive X : forall (n:nat), T n -> Set := .
Lemma bar : X (U + 1 - 1) b = X U a.
Proof.
generalize a_is_b.
generalize b.
rewrite <- foo.
intros.
rewrite H.
reflexivity.
Qed.
Edsko
- [Coq-Club] Dependent rewrite question (probably simple answer! :), Edsko de Vries
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Adam Chlipala
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Edsko de Vries
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Adam Chlipala
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :), Edsko de Vries
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Adam Chlipala
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Edsko de Vries
- Re: [Coq-Club] Dependent rewrite question (probably simple answer! :),
Adam Chlipala
Archive powered by MhonArc 2.6.16.