The Coq mailing list

["Floyd Lee" <undecidable AT secureroot.com>]

--- 
guillaume.brunerie AT gmail.com
 wrote:
> > Do you happen to know if it's safe to assume eta_let_pair_eq as an axiom?
>
> No problem with that.
> You can more generally assume function extensionality
> (http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html)
> which is enough to prove eta_let_pair_eq.

Nice, thanks.

For the record:

Module FE := Coq.Logic.FunctionalExtensionality.

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.
  apply FE.functional_extensionality.
  intro x.
  destruct (f x).
  reflexivity.
Qed.




_____________________________________________________________
---
http://mail.secureroot.com/ - free mailbox for hackers and geeks