How can I prove the lemma zpstar_dec?

```
Section ZP.
Context {p : Z} {Hp : prime p}.
(* we define for 1 <= v < p *)
Record Zpstar : Type := mk_zpstar {vt : Z; Hvt : 1 <= vt < p}.
Lemma zpstar_dec: forall x y : Zpstar, {x = y} + {x <> y}.
Proof.
intros x y. destruct x as [x Hx]; destruct y as [y Hy]; simpl.
destruct (Z.eq_dec x y) as [Hl | Hr].
left. subst. apply f_equal.
pose proof (@Eqdep_dec.eq_dep_eq_dec Z Z.eq_dec (fun z => 1 <= z < p) y Hx Hy).
```

Now, I am unable to build a proof term of type EqdepFacts.eq_dep Z (fun z : Z => 1 <= z < p) y Hx y Hy.

```
p: Z
Hp: prime p
y: Z
Hx, Hy: 1 <= y < p
H: EqdepFacts.eq_dep Z (fun z : Z => 1 <= z < p) y Hx y Hy -> Hx = Hy
---------------------------------------------------------------------------------------
Hx = Hy
```

The below two references might give you some insight into this:

- (http://adam.chlipala.net/cpdt/html/Equality.html) search for "UIP"
- (https://coq.inria.fr/refman/addendum/sprop.html#definitional-uip)

As result oriented engineer I would recommend to use a weaker form of equality for Zpstar, e.g. one which uses "<->" instead of "=" for the proof part. It might be a bit of work to set it up such that it works nicely with setoid rewrite, but otherwise there is little disadvantage in using weaker forms of equality (thanks to setoid rewrite). Think of Q where 2/4=1/2 - if one would want to use Leibnitz equality for Q one would have to fully reduce all numbers, which would be a huge effort for large numbers. By contrast it is quite easy to check equality (or equivalence) for non reduced rationals. In your setup you should also ask yourself what advantages you get from a stronger or weaker form of equality, and what it would cost you.

inequality on Z is defined as `Z.le = fun x y : Z => (x ?= y) <> Gt`

so you can't prove equalities about it without funext.

with funext you should be able to prove that `Z.le`

and `Z.lt`

have trivial equalities (`forall x y (H H' : x <= y), H = H'`

and same for `<`

), then instead of that pose proof you do `destruct Hx,Hy;f_equal`

and use the lemmas.

alternatively just assume `proof_irrelevance : forall P : Prop, forall x y : P, x = y`

which implies `Hx = Hy`

PS if you're willing to adapt your definition a bit you can use `Record Zpstar : Type := mk_zpstar {vt : Z; Hvt : 0 < vt < p}.`

because `Z.lt`

doesn't need funext to prove it has trivial equality

sigh, seemingly the only place where one can find irrelevance proofs like this is in MathComp - `lt_irrelevance`

and `le_irrelevance`

for `nat`

. Both this and irrelevance for `Z.lt`

should arguably be easily available in a non-MathComp standard library.

The most general lemma about proof irrelevance in MathComp is `eq_irrelevance`

which shows that all `eqType`

s have unique identity proofs. This lemma is crucial for forming sub-types. More in chapter 7 of the MathCompBook (7.2.2 mentions `eq_irrelevance`

).

completely agree that `eq_irrelevance`

is the most important, but I think people setting up types of form `{ x : some_num_type; Hx : some_num_pred x }`

and getting stumped by absence of irrelevance results (most directly, in stdlib) is very common

Thanks everyone for the insightful discussion. I managed to get it, but let me know if it can be improved. (I also realised that if I have decidable types, then I can turn the Prop into boolean equality and use the Eqdep_dec.eq_proofs_unicity lemma).

```
Record Zpstar : Type := mk_zpstar {vt : Z; Hvt : 0 < vt < p}.
Lemma dec_zero_lt : forall x (Hx Hy: 0 < x ), Hx = Hy.
Proof.
intros; apply Eqdep_dec.eq_proofs_unicity;
intros u v; destruct u; destruct v; auto;
try (right; intro Hpp; inversion Hpp).
Qed.
Lemma dec_lt_p : forall x (Hx Hy: x < p), Hx = Hy.
Proof.
intros; apply Eqdep_dec.eq_proofs_unicity;
intros u v; destruct u; destruct v; auto;
try (right; intro Hpp; inversion Hpp).
Qed.
Lemma dec_proof : forall x (Hx Hy: 0 < x < p), Hx = Hy.
Proof.
intros x Hx Hy. destruct Hx as [Hxl Hxr].
destruct Hy as [Hyl Hyr].
f_equal; [apply dec_zero_lt | apply dec_lt_p].
Qed.
Lemma dec_p : forall x y : Zpstar, {x = y} + {x <> y}.
Proof.
destruct x as [x Hx]; destruct y as [y Hy]; simpl.
destruct (Z.eq_dec x y) as [Hl | Hr].
left. subst. f_equal. apply dec_proof.
right. intro H; inversion H;
contradiction.
Qed.
Require Import Coq.Logic.FunctionalExtensionality.
Print Z.lt.
Print Z.le.
Lemma zle_gen : forall x (H1 H2: 1 <= x < p), H1 = H2.
Proof.
intros. destruct H1, H2. f_equal. apply functional_extensionality.
intros. f_equal. apply dec_lt_p.
Qed.
```

Instead of having 2 lemmas `dec_zero_lt`

and `dec_lt_p`

you can just prove the more general `forall x y (Hx Hy : x < y), Hx = Hy`

also in `dec_proof`

you could just do `intros x [? ?] [? ?];f_equal;[apply dec_zero_lt | apply dec_lt_p].`

(or rather apply the general lt_irrelevance lemma)

IMO the easiest path is to show that `op`

has an equivalent `opb`

(a boolean version of it) and then use `eq_irrelevance`

. That proof is quite tricky, way trickier that the usual lemma linking `op`

and `opb`

.

Indeed, I agree with @Enrico Tassi , I think `le_irrelevance`

is in math-comp more as to showcase fancy tactic use than as to be of real utility.

Last updated: Jan 29 2023 at 05:03 UTC