Proof irrelevance for Z.lt and Z.le · Coq users

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

Michael Soegtrop (Sep 11 2021 at 10:21):

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.

Gaëtan Gilbert (Sep 11 2021 at 10:35):

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

Karl Palmskog (Sep 11 2021 at 11:20):

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.

Enrico Tassi (Sep 11 2021 at 19:34):

The most general lemma about proof irrelevance in MathComp is eq_irrelevance which shows that all eqTypes 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).

Karl Palmskog (Sep 11 2021 at 20:10):

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

Mukesh Tiwari (Sep 11 2021 at 23:05):

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.

Gaëtan Gilbert (Sep 12 2021 at 08:34):

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)

Enrico Tassi (Sep 12 2021 at 16:17):

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.

Emilio Jesús Gallego Arias (Sep 13 2021 at 14:15):

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.

Stream: Coq users

Topic: Proof irrelevance for Z.lt and Z.le

Mukesh Tiwari (Sep 11 2021 at 04:49):