## Stream: Coq users

### Topic: ✔ Declaring that a property is hProp

#### Ayhon (Apr 10 2024 at 14:17):

TLDR : To use `eq_sig_hprop` to prove `proj1_sig a = proj1_sig a' -> a = a'` for `a: { z: Z | z = 1 \/ z = -1 }` I need to prove that `P := forall (z: Z), z = 1 \/ z = -1` is an `hProp`, or equivalently `forall (x : A) (p q : P x), p = q`. How could I set out to do that?

For one of my proofs I've declared the following type

``````Definition pmUnit := { l : Z | l = 1 \/ l = -1}.
``````

in order to define `term`s, which in this case are instances of `±x` for a variable `x`, represented by a `nat`.
I have to show that `t = t' <-> eqb t t'` where

``````Record term := {a: pmUnit;x: nat}.
Program Definition eqb(t t': term) :=
(t.(a) =? t'.(a))%Z && (t.(x) =? t'.(x))%nat.
``````

To do so I need at some point to show that `proj1_sig a = proj1_sig a' -> a = a'`, which seems to correspond to the theorem `eq_sig_hprop`. However this requires that I prove that `forall (x: Z), x= 1 \/ x = -1` is an `hProp`, which is where I'm currently stuck. When I try to look for information about `hProp` I get redirected to papers about univalent mathematics, which seems a bit far away from what I was trying to achieve.

What is an `hProp`, in layman terms? Is this the only way of achieving what I'm set out to do? Should I drop the `sig`?

#### Ike Mulder (Apr 10 2024 at 14:33):

I am not sure about the terminology, but there is a useful related lemma that states that if equality is decidable (where we say that `P` is decidable, if there is a program that gives you a witness of `{P} + {¬ P}`), then all proofs of equality are actually equal. Perhaps you could extend this proof to your case, where you are looking for integers equal to 1 or -1?

In stdpp, that lemma is called eq_pi.

#### Johannes Hostert (Apr 10 2024 at 14:33):

In Coq's stdlib, it's `UIP_dec`, and you can use it in your proof like this:

``````From Coq Require Import Eqdep_dec.
Definition P z := z = 1 \/ z = -1.
Goal forall (x : Z) (p q : P x), p = q.
Proof.
intros z p q. destruct p, q; try lia.
all: f_equal. all: eapply UIP_dec.
(* Decidable equality on Z should be somewhere in the standard library but I could not immediately find it *)
all: repeat decide equality.
Qed.
``````

#### Meven Lennon-Bertrand (Apr 10 2024 at 14:39):

An hProp (homotopy proposition) is a type where any two elements are equal. Indeed, it's mostly used in the context of homotopy type theory, but there is a very useful theorem usually called Hedberg's theorem, which states that if a type has decidable equality, then it is an hProp. This is what the stdlib calls `UIP_dec`. Using it, you should be able to obtain that `x = 1 \/ x = -1` is an hProp, and be able to apply your `eq_sig_hprop` theorem.

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:40):

@Ayhon if you're deep into this kind of trouble, you probably set your definitions wrong. The ssr design pattern is to consider pairs where the second component is of the form `foo x = true`, which enjoy uip for free.

#### Meven Lennon-Bertrand (Apr 10 2024 at 14:42):

Pierre-Marie Pédrot said:

Ayhon if you're deep into this kind of trouble, you probably set your definitions wrong. The ssr design pattern is to consider pairs where the second component is of the form `foo x = true`, which enjoy uip for free.

I don't remember the theorem, but I'm pretty sure there is something in ssreflect which indeed says that any pair with a second component of this form (alternatively, any component which is `reflect`ed by a boolean) has the property your are looking for, ie that the first projection is injective

#### Ayhon (Apr 10 2024 at 14:44):

Pierre-Marie Pédrot said:

Ayhon if you're deep into this kind of trouble, you probably set your definitions wrong. The ssr design pattern is to consider pairs where the second component is of the form `foo x = true`, which enjoy uip for free.

The lemma I'm trying to prove is

``````Lemma eqb_spec(t t': term) : Bool.reflect (t = t') (t =? t').
``````

with `=?` being the `eqb` for `term`. My strategy was to then apply `iff_reflect`, as they do in the `IndProp.v` chapter of Logical Foundations (in the proof of `eqbP`). Should I have defined it in some other way?

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:46):

a proposition being reflected by a boolean is not enough to be hprop

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:47):

(consider e.g. the equivalent of bool in Prop, which is inhabited but has two inhabitants)

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:48):

what I'm saying is that stuffing arbitrary propositions P in {x : A | P} is looking for hott-like trouble

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:48):

if you stay in the fragment where you only build dependent pairs {x : A | f x = true} you'd have a much easier time

#### Pierre-Marie Pédrot (Apr 10 2024 at 14:48):

even better (if you like bleeding-edge stuff) you can also consider using SProp directly

#### Pierre Roux (Apr 10 2024 at 14:49):

I guess, the suggestion was rather about the definition of

``````Definition pmUnit := { l : Z | l = 1 \/ l = -1}.
``````

that would be easier as

``````Definition pmUnit := { l : Z | l == 1 || l == -1}.
``````

#### Ayhon (Apr 10 2024 at 14:51):

Pierre-Marie Pédrot said:

even better (if you like bleeding-edge stuff) you can also consider using SProp directly

I think I'd first need to finish Logical Foundations though, I'll leave it for later :P

#### Ayhon (Apr 10 2024 at 14:51):

Thank you very much to everyone!

#### Notification Bot (Apr 10 2024 at 14:51):

Ayhon has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC