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`

?

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.

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

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.

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

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

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?

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

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

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

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

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

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}.
```

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

Thank you very much to everyone!

Ayhon has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC