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.

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

Ah, thanks so much for this advice. It is called `bool_irrelevance`

and solves the goal.

Sebastian Ertel has marked this topic as resolved.

You can also apply `val_inj`

to transform your equality on ordinals to an equality on `nat`

:

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

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