I have some porposition `P : Prop`

, I was able to prove that `P x y \/ ~ P x y`

for thisparticular `P`

Now I want to use proof irrelevance properties from mathcomp on that proposition,

I just don't see how to get from there to `eqType`

. I thought I would just implement a function (x -> y -> bool) and reflect, but I wasn't able to write a function for this proposition, so is there a way to start from the lemma `P x y\/ ~ P x y`

and end up with `(a b: P x y) a = b`

?

`P x y \/ ~ P x y`

is not enough to get a bool out, you need `{P x y} + {~ P x y}`

and you're not going to get proof irrelevance for an arbitrary P from decidability, you only get irrelevance of `decide P = true`

(because equality of booleans is irrelevant)

You cannot go from Prop to bool without axioms. So you either need to prove `{P x y} + {~ P x y}. Or use classical logic axioms, for instance as provided in the `

boolp.v` file of mathcomp-classical

I am confused, what is the difference between ` {P x y} + {~ P x y}`

and `P x y \/ ~ P x y`

?

The first is in `Set`

, the second is in `Prop`

alright, the question here is what is the forall equivalent in `Set`

?

It's the same `forall`

That is strange, because for somereason it is not working for me:

```
Definition smap_forall {K: eqType} {V} {M: finMap K} (P: K -> V -> Set):
M V -> Set :=
fun m => forall k v, P k v.
```

gives the error:

```
The term "forall (k : K) (v : V), P k v" has type "Type" while it is expected to have type "Set"
```

Ignore the meaning of the definition for now, I removed pieces of it.

Set is not impredicative unlike Prop

this means that if `A:Type`

`X:A -> Set`

and `P:A -> Prop`

, then `(forall x : A, P x) : Prop`

but `(forall x : A, X x) : Type`

but why are you putting `P`

in Set? in `{P} + {Q}`

P and Q are Prop

the difference is between

```
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.
```

and

```
Inductive sumbool (A B:Prop) : Set :=
| left : A -> {A} + {B}
| right : B -> {A} + {B}
where "{ A } + { B }" := (sumbool A B) : type_scope.
```

I see, I am not sure I fully comprehend the difference yet, but I see that there is a difference.

So Assuming that was able to prove `{P x y} + {~ P x y}`

.

how can I get proof irrelevance for `P x y`

?

you cannot at least not from that

what ? It feels intuitively trivial, that feels a lot like map to bool?

So it is there true or false, so if there are 2 instances of it, they are either going to be the same true of false.

I am not sure what is missing ?

they are either going to be the same true

that is what you are trying to prove, not something you have proven

basically look at

```
Inductive wierd : Prop := Wierd : nat -> wierd.
Definition P (_ _:nat) := wierd.
```

P is decidable (it's always true)

but `Wierd 1`

and `Wierd 2`

are both inhabitants and cannot be proved equal without axioms

In terms of cardinality, `P + (P -> False)`

just tells you that the cardinality of P is either 0 or at least one.

proof irrelevance tells you that the cardinal is at most one

so if P were to be a Type rather than a Prop you could have a situation where `P + (P -> False)`

but P have several distinct elements.

For instance, pick @Gaëtan Gilbert 's example above in Type.

but we can ignore pieces of informaiton ,right?

We can acknowledge that elements of wierd 1 and wierd2 can be mapped to either true or false (in this case true), and this I guess is doable from sum type.

It feels trivial, and I think I know how to do it (correct me if it is not that trivial) but it should just be match on the type if it is left, then true if it is right, then false.

and that must be proof irrelevant.

you can map elements of nat to true or false too

what does that have to do with proof irrelevance?

never mind, I guess it is stupid idea.

actually I figured out I don't really care about `P x y`

,

What I really cared about is that the map from `P x y`

to bool ends up being `true`

.

I got it to work ( with lots of copying from stdpp), but I barely understand the decidability magic and its relation to proof irrelevance.

I guess this is about the time I usually ask for papers on the topic if anyone has good one.

P.S. (I know about google scholar, but it doesn't really help in cases when you are not the expert so you don't know what to look for).

TLDR: Having P decidable doesn't make P proof-irrelevant, it just makes `bool_decide P = true`

proof-irrelevant. The reason is that (1) this is an equality of booleans (2) equality of type P is proof-irrelevant whenever P has decidable equality (this is called Hedberg's theorem) I (3) and booleans do have it. Thankfully, one needn't understand the proof of Hedberg's theorem to use it, but this use-case comes up often.

thanks a lot, I think i ended up exactly doing what you described, I used bool_decide P = true, thanks for the theorm's name

Last updated: Jul 25 2024 at 17:02 UTC