coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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], 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], Benoît Viguier, 03/30/2016
- Re:[Coq-Club], Emilio Jesús Gallego Arias, 03/30/2016
Archive powered by MHonArc 2.6.18.