coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]

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.

[Coq-Club], Benoît Viguier, 03/30/2016
- Re:[Coq-Club], Pierre Casteran, 03/30/2016
- Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
  - Re:[Coq-Club], Benoît Viguier, 03/30/2016
    - Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
      - Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], roux cody, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
- Re:[Coq-Club], Emilio Jesús Gallego Arias, 03/30/2016