Stream: math-comp users

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


view this post on Zulip 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 ?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Alexander Gryzlov (Feb 13 2023 at 13:18):

The first is in Set, the second is in Prop

view this post on Zulip walker (Feb 13 2023 at 13:22):

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

view this post on Zulip Alexander Gryzlov (Feb 13 2023 at 13:29):

It's the same forall

view this post on Zulip 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"

view this post on Zulip walker (Feb 13 2023 at 13:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Feb 13 2023 at 13:53):

you cannot at least not from that

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Feb 13 2023 at 14:01):

proof irrelevance tells you that the cardinal is at most one

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Feb 13 2023 at 14:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip walker (Feb 13 2023 at 14:12):

and that must be proof irrelevant.

view this post on Zulip 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?

view this post on Zulip walker (Feb 13 2023 at 14:14):

never mind, I guess it is stupid idea.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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: Jul 25 2024 at 17:02 UTC