The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Well, I would love to have functionnal extensionality but it is not for now, for sure (plus I am not sure it would mix well with some theories like HoTT, for which, if I have correctly understood, one does not have UIP).

Actually, in HoTT, univalence implies functional extensionality.

(section 4.9 of HoTT book)

Univalence does refute UIP, though.

 

2013/12/4 Adam Chlipala <adamc AT csail.mit.edu>

Maybe I've missed the point here, but [simpl; rewrite T] seems to have the same effect as [setoid_rewrite T].  Why is [setoid_rewrite] so much more "useful" here?

On 12/04/2013 10:30 AM, Ilmārs Cīrulis wrote:

Yay!
setoid_rewrite is incredibly useful! :)

Theorem T n: match n with O => O | _ => O end = O.
 destruct n; reflexivity.
Qed.

Require Import Setoid.
Theorem T0 n: (fix f1 n m :=
  match n with
  | 0 => match m with
         | 0 => 0
         | S _ => 0
         end
  | S n' => n + f1 n' m
  end) 0 n = 0.
Proof.
 setoid_rewrite T.
 reflexivity.
Qed.

--
.../Sedrikov\...