Stream: Coq users

Topic: ✔ SSReflect equality problem

Sebastian Ertel (Mar 28 2023 at 13:18):

Hi,

I'm stuck on a goal where is_true exists in a hypothesis and I cannot manage to rewrite it such that it becomes a proposition.

My issue is related to this stackoverflow entry:
https://stackoverflow.com/questions/64165405/coq-error-unable-to-unify-true-with-is-true-0-a-b-3
Yet I could not apply the solution presented in the answer.

My code is as follows:

From mathcomp Require Import all_ssreflect all_algebra fingroup.fingroup
  prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype.

   Definition f {q:nat} (H : prime q) (a : 'Z_q) : 'Z_q -> 'Z_q :=
      fun b =>
        if b == Zp0 then Zp0 else Zp_mul b a.

    Definition f_inv {q:nat} (H : prime q) (a : 'Z_q) : 'Z_q -> 'Z_q :=
      fun c =>
        if c == Zp0 then Zp0 else Zp_mul c (Zp_inv a).

    Lemma f_inj {q:nat} : forall (a : 'Z_q) (H : prime q), cancel (f H a) (f_inv H a).
    Proof.
      move => a H.
      rewrite /cancel/f/f_inv /=.
      case. case.
      - clear. simpl.

At this point, my proof state is

  q : nat
  a : 'Z_q
  ============================
  ∀ i : is_true (0 < (Zp_trunc q).+2)%N, Zp0 = Ordinal (n:=(Zp_trunc q).+2) (m:=0) i

I can now further unfold Zp0 by:

  rewrite /Zp0 /ord0 => i; f_equal; clear.

Now my proof state is

  q : nat
  i : is_true (0 < (Zp_trunc q).+2)%N
  ============================
  ltn0Sn (Zp_trunc q).+1 = i

At this point, I' stuck.
The term on the left-hand side of the equality has the proper type:

Check (ltn0Sn (Zp_trunc q).+1).
ltn0Sn (Zp_trunc q).+1
     : is_true (0 < (Zp_trunc q).+2)%N

Yet, I cannot resolve this equality because the lemma ltn0Sn is opaque such that I cannot reduce any further.

Instead of unfolding Zp0, I also tried to fold Zp0 from the right-hand side:

  rewrite -/ord0 -/Zp0.

But that did not work either.

Any help on this would be much appreciated.

Gaëtan Gilbert (Mar 28 2023 at 13:21):

Don't you need uniqueness of is_true proofs? ie a lemma forall b (i j : is_true b), i = j
I don't know what mathcomp calls it but it should exist somewhere

Sebastian Ertel (Mar 28 2023 at 13:40):

Ah, thanks so much for this advice. It is called bool_irrelevance and solves the goal.

Notification Bot (Mar 28 2023 at 13:40):

Sebastian Ertel has marked this topic as resolved.

Pierre Jouvelot (Mar 28 2023 at 13:44):

You can also apply val_inj to transform your equality on ordinals to an equality on nat:

move=> lt0; apply: val_inj => //=.

Sebastian Ertel (Mar 28 2023 at 14:26):

That is also a great solution. Thanks! I often forget to make good use of the type classes.

Last updated: Oct 13 2024 at 01:02 UTC