The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

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