Stream: Coq users

Topic: ✔ Declaring that a property is hProp


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

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

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

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

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

view this post on Zulip 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 reflected by a boolean) has the property your are looking for, ie that the first projection is injective

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

view this post on Zulip Pierre-Marie Pédrot (Apr 10 2024 at 14:46):

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

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

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

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

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

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

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

view this post on Zulip Ayhon (Apr 10 2024 at 14:51):

Thank you very much to everyone!

view this post on Zulip Notification Bot (Apr 10 2024 at 14:51):

Ayhon has marked this topic as resolved.


Last updated: Jun 18 2024 at 22:01 UTC