## 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: Jun 15 2024 at 05:01 UTC