Stream: math-comp users

Topic: How to go from `Prop` to `bool` (and get proof irrel.)

walker (Feb 13 2023 at 13:06):

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 ?

Gaëtan Gilbert (Feb 13 2023 at 13:11):

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)

Pierre Roux (Feb 13 2023 at 13:12):

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

walker (Feb 13 2023 at 13:17):

I am confused, what is the difference between {P x y} + {~ P x y} and P x y \/ ~ P x y ?

Alexander Gryzlov (Feb 13 2023 at 13:18):

The first is in Set, the second is in Prop

walker (Feb 13 2023 at 13:22):

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

Alexander Gryzlov (Feb 13 2023 at 13:29):

It's the same forall

walker (Feb 13 2023 at 13:33):

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"

walker (Feb 13 2023 at 13:34):

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

Gaëtan Gilbert (Feb 13 2023 at 13:36):

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

Gaëtan Gilbert (Feb 13 2023 at 13:37):

but why are you putting P in Set? in {P} + {Q} P and Q are Prop

Gaëtan Gilbert (Feb 13 2023 at 13:38):

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.

walker (Feb 13 2023 at 13:52):

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

walker (Feb 13 2023 at 13:53):

So Assuming that was able to prove {P x y} + {~ P x y}.
how can I get proof irrelevance for P x y?

Gaëtan Gilbert (Feb 13 2023 at 13:53):

you cannot at least not from that

walker (Feb 13 2023 at 13:55):

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 ?

Gaëtan Gilbert (Feb 13 2023 at 13:59):

they are either going to be the same true

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

Gaëtan Gilbert (Feb 13 2023 at 14:00):

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

Pierre-Marie Pédrot (Feb 13 2023 at 14:00):

In terms of cardinality, P + (P -> False) just tells you that the cardinality of P is either 0 or at least one.

Pierre-Marie Pédrot (Feb 13 2023 at 14:01):

proof irrelevance tells you that the cardinal is at most one

Pierre-Marie Pédrot (Feb 13 2023 at 14:02):

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.

Pierre-Marie Pédrot (Feb 13 2023 at 14:03):

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

walker (Feb 13 2023 at 14:11):

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.

walker (Feb 13 2023 at 14:11):

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.

walker (Feb 13 2023 at 14:12):

and that must be proof irrelevant.

Gaëtan Gilbert (Feb 13 2023 at 14:13):

you can map elements of nat to true or false too
what does that have to do with proof irrelevance?

walker (Feb 13 2023 at 14:14):

never mind, I guess it is stupid idea.

walker (Feb 13 2023 at 15:38):

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.

walker (Feb 13 2023 at 15:40):

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

walker (Feb 13 2023 at 15:42):

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).

Paolo Giarrusso (Feb 14 2023 at 00:43):

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.

walker (Feb 14 2023 at 09:44):

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: Oct 13 2024 at 01:02 UTC