coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: muad <muad.dib.space AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: Re[Coq-Club] writing and eta rule
- Date: Mon, 1 Jun 2009 14:09:42 -0700 (PDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi Andrej,
Here is how I would do it, since I don't know if this sort of thing exists
already you can write an Ltac script:
Lemma eta_rule (A B : Set) (f : A -> B): (fun x => f x) = f.
Admitted.
Theorem cong_lem_1 {A B} (f g : A -> B) x y : f = g -> x = y -> f x = g y.
intros; congruence.
Qed.
Theorem cong_lem_2 {A B} (x u : A) (y v : B) : x = u -> y = v -> (x,y) =
(u,v).
intros; congruence.
Qed.
Ltac congruence_helper_via_injectivity :=
reflexivity ||
congruence ||
(apply eta_rule; congruence_helper_via_injectivity) ||
(apply cong_lem_1; congruence_helper_via_injectivity) ||
(apply cong_lem_2; congruence_helper_via_injectivity) ||
idtac.
Lemma test1 (A B C : Set) (g : (A -> B) -> C) (f : A -> B): g (fun x => f x)
= g f.
intros.
congruence_helper_via_injectivity.
Qed.
and for comp you can just do unfold comp; which replaces the use with its
definition.
--
View this message in context:
http://www.nabble.com/Rewriting-and-eta-rule-tp23819253p23822354.html
Sent from the Coq mailing list archive at Nabble.com.
- [Coq-Club] Rewriting and eta rule, Andrej Bauer
- Re: Re[Coq-Club] writing and eta rule, muad
- Re: Re[Coq-Club] writing and eta rule, Andrej Bauer
- Re: [Coq-Club] Rewriting and eta rule, Taral
- Re: Re[Coq-Club] writing and eta rule, muad
Archive powered by MhonArc 2.6.16.