Skip to Content.
Sympa Menu

coq-club - Re: Re[Coq-Club] writing and eta rule

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re[Coq-Club] writing and eta rule


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





Archive powered by MhonArc 2.6.16.

Top of Page