coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] eta zeta!, Floyd Lee, 05/29/2013
- Re: [Coq-Club] eta zeta!, Guillaume Brunerie, 05/29/2013
- <Possible follow-up(s)>
- Re: [Coq-Club] eta zeta!, Floyd Lee, 05/29/2013
- Re: [Coq-Club] eta zeta!, Guillaume Brunerie, 05/29/2013
- Re: [Coq-Club] eta zeta!, Floyd Lee, 05/29/2013
Archive powered by MHonArc 2.6.18.