Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof irrelevance for Z.le

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance for Z.le


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page