Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] eta zeta!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eta zeta!


Chronological Thread 
  • From: Guillaume Brunerie <guillaume.brunerie AT gmail.com>
  • To: Floyd Lee <undecidable AT secureroot.com>
  • Cc: Coq-Club Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] eta zeta!
  • Date: Tue, 28 May 2013 19:53:45 -0400

Hello,

There is no definitional eta for pairs in Coq 8.4, only for functions.
In particular the term let (y, z) := f x in (y, z) is not
definitionally equal to (f x), only propositionally.

Hence (fun x => let (y, z) := f x in (y, z)) and (fun x => f x) are
only pointwise equal propositionally, hence they have no reason to be
propositionally equal as functions (unless you assume function
extensionality).

Guillaume

2013/5/28 Floyd Lee
<undecidable AT secureroot.com>:
> Hello. I'm having trouble proving eta_let_pair_eq. I'm not sure if it's
> expected that this should be difficult or not...
>
> These theorems obviously rely on 8.4pl2's new eta rule.
>
> (** zeta alone *)
> Theorem let_eq : forall
> {A B : Type}
> (x : A)
> (f : A -> B),
> (let y := f x in y) = f x.
> Proof.
> intros A B x f.
> reflexivity.
> Qed.
>
> (** Reduces to (y, z) = (y, z) *)
> Theorem let_pair_eq : forall
> {A B C : Type}
> (x : A)
> (f : A -> (B * C)),
> (let (y, z) := f x in (y, z)) = f x.
> Proof.
> intros A B C x f.
> destruct (f x).
> reflexivity.
> Qed.
>
> (** eta-zeta convertible *)
> Theorem eta_let_eq : forall
> {A B : Type}
> (f : A -> B),
> (fun x => let y := f x in y) = (fun x => f x).
> Proof.
> intros A B f.
> reflexivity.
> Qed.
>
> (** Crunch! *)
> Theorem eta_let_pair_eq : forall
> {A B C : Type}
> (f : A -> (B * C)),
> (fun x => let (y, z) := f x in (y, z)) = (fun x => f x).
> Proof.
> intros A B C f.
> (* reflexivity.
> Error: Impossible to unify "f x" with "let (y, z) := f x in (y, z)". *)
> (* rewrite (eta_let_eq f).
> Error: Found no subterm matching "fun x : A => let y := f x in y" in
> the current goal. *)
> (* Can't use let_pair_eq due to lacking an A. *)
> Abort.
>
>
>
> _____________________________________________________________
> ---
> http://mail.secureroot.com/ - free mailbox for hackers and geeks



Archive powered by MHonArc 2.6.18.

Top of Page