coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: Thomas Braibant <thomas.braibant AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Proof irrelevance for Z.le
- Date: Tue, 31 Jul 2012 12:18:25 -0700
On Tue, Jul 31, 2012 at 11:33 AM, Thomas Braibant
<thomas.braibant AT gmail.com>
wrote:
> Hi list,
>
> I wonder if there is a way to prove proof-irrelevance for Z.le,
> without using the proof-irrelevance axiom?
It seems highly unlikely, assuming your Z.le is like Zle from Coq
8.3pl4 and reduces to "fun x y => ((x ?= y) = Gt -> False)". Or at
least, without using some form of functional extensionality.
On the other hand, if Zle (and presumably Ple) were defined as
inductive propositions, it would probably be possible. By that, I'm
thinking of something like (read this as pseudo-code):
Inductive Ple : positive -> positive -> Prop :=
| Ple 1 1
| Ple 1 p~0
| Ple 1 p~1
| Ple p q -> Ple (p~0) (q~0)
| Plt p q -> Ple (p~1) (q~0)
...
with Plt : positive -> positive -> Prop :=
| Plt 1 p~0
...
Inductive Zle : Z -> Z -> Prop :=
| Zle 0 0
| Zle 0 (Zpos p)
| Ple p q -> Zle (Zpos p) (Zpos q)
| Ple q p -> Zle (Zneg q) (Zneg p)
...
--
Daniel Schepler
- [Coq-Club] Proof irrelevance for Z.le, Thomas Braibant, 07/31/2012
- Re: [Coq-Club] Proof irrelevance for Z.le, Jason Gross, 07/31/2012
- Re: [Coq-Club] Proof irrelevance for Z.le, Daniel Schepler, 07/31/2012
- Re: [Coq-Club] Proof irrelevance for Z.le, Thomas Braibant, 07/31/2012
Archive powered by MHonArc 2.6.18.