Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page