Skip to Content.
Sympa Menu

coq-club - [Coq-Club]

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]


Chronological Thread 
  • From: Benoît Viguier <beviguier AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club]
  • Date: Wed, 30 Mar 2016 13:12:35 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f171.google.com
  • Ironport-phdr: 9a23:m9iqaRV1QZBJecHnLnKl5ZmoM/zV8LGtZVwlr6E/grcLSJyIuqrYZhGBt8tkgFKBZ4jH8fUM07OQ6PCwHzZQqs3d+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VOVUD32b1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3XerwkXPRDET4kPmsprI2y7ViQBTeIs3AbSyAdlgdCKwnD9hDzGJnr4QXgse8o8iScOkvqeo41Vimj4r0jHBXlliYIKj806knYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PHDJM


Hi,

I have this proof I would like to use with some list ordering.

Require Import FunctionalExtensionality.
Require Import Bool.
Require Import Arith.

Definition Unit := nat.
Definition orderb := Nat.leb.
Definition order := le.

Fact orderbleb : (fun a b : Unit =>
     is_true (orderb a b)) = order.
Proof.
apply functional_extensionality.
intro a.
apply functional_extensionality.
intro b.
unfold orderb.
unfold is_true.
unfold order.
Check Nat.leb_le.
rewrite Nat.leb_le.
(*Error*)

Can someone explain me why I am not allowed to complete this proof ? Using the functionnal extensionality, it should be right. No ?

Kind regards.

Benoît.



Archive powered by MHonArc 2.6.18.

Top of Page