## Stream: Coq users

### Topic: An eqP lemma

#### Julin Shaji (Mar 31 2024 at 12:32):

I got a type like

``````Require Import ssreflect.
Require Import Bool.

Inductive t: Type :=
| Zero: t
| One: t
| More: t -> t -> t.
``````

And have made a equality procedure for it:

``````Fixpoint teqb (a b: t): bool :=
match a, b with
| Zero, Zero => true
| One, One => true
| More a1 b1, More a2 b2 => teqb a1 a2 && teqb b1 b2
| _, _ => false
end.
``````

Now, I am trying to have an `eqP` reflection lemma:

``````Lemma eqtP (a b: t): reflect (a = b) (teqb a b).
Proof.
elim: a b => [b|b|a IHa b IHb].
- case: b.
+ by apply ReflectT.
+ by apply ReflectF.
+ move => a b.
by apply ReflectF.
- case: b.
+ by apply ReflectF.
+ by apply ReflectT.
+ by move => a b; apply ReflectF.
- case.
+ by apply ReflectF.
+ by apply ReflectF.
+ move => x y.
(*
1 subgoal

a : t
IHa : forall b : t, reflect (a = b) (teqb a b)
b : t
IHb : forall b0 : t, reflect (b = b0) (teqb b b0)
x, y : t

========================= (1 / 1)

reflect (More a b = More x y) (teqb (More a b) (More x y))
*)
``````

And am stuck at the induction step.

Any idea how I can proceed from here?

#### Emilio Jesús Gallego Arias (Mar 31 2024 at 12:56):

@Julin Shaji , indeed there are several ways to do this kind of proof, I usually split the proof in several sublemmas, but that's not necessary in this case, as it is pretty simple and you can handle a direct proof:

``````From mathcomp Require Import all_ssreflect.

Inductive t: Type :=
| Zero: t
| One: t
| More: t -> t -> t.

Fixpoint teqb (a b: t): bool :=
match a, b with
| Zero, Zero => true
| One, One => true
| More a1 b1, More a2 b2 => teqb a1 a2 && teqb b1 b2
| _, _ => false
end.

Lemma teqbb a : a = a -> teqb a a.
Proof. by elim: a => //= ? ht1 ? ht2 _; rewrite ht1 ?ht2. Qed.

Lemma teqb_refl a b : a = b -> teqb a b.
Proof. by elim: a b => [||? ? ? ?] [||] // a2 b2 [->->]; rewrite !teqbb. Qed.

Lemma teqb_correct a b : teqb a b -> a = b.
Proof.
by elim: a b => [||t1 ih1 t2 ih2] [||t1' t2'] //= /andP[/ih1->/ih2->].
Qed.

Lemma eqtP (a b: t): reflect (a = b) (teqb a b).
Proof.
by apply: (iffP idP); [apply: teqb_correct|apply: teqb_refl].
Qed.

Lemma eqtP_direct a b : reflect (a = b) (teqb a b).
Proof.
elim: a b => [||a1 iha b1 ihb] [||] //=; try constructor; move=> // t1 t2.
by have [->|hnea]:= iha t1; have [->|hneb] := ihb t2; constructor; try case.
Qed.
``````

#### Emilio Jesús Gallego Arias (Mar 31 2024 at 12:57):

It is often convenient to show that a type has some property by just showing and embedding into some type that already has the structure, tho that will result in an equality that doesn't compute as is.

#### Emilio Jesús Gallego Arias (Mar 31 2024 at 12:58):

The point you are stuck in the proof is because it is time to use the induction hyp; you need to check what the equality on subterms resulted before you can decide what the right result is.

#### Emilio Jesús Gallego Arias (Mar 31 2024 at 13:03):

You can do that a bit more step-by-step as:

``````      + move => x y /=.
have [->|neqa] := IHa x; last by constructor; case.
by have [->|neqb] := IHb y; constructor; try case.
``````

#### Quentin VERMANDE (Mar 31 2024 at 13:43):

You can also use `iffP idP` to turn a goal`reflect P b` into two implications `P -> b` and `b -> P` (you can even apply the reflection you want to `b` instead of `idP`).

Last updated: Jun 13 2024 at 19:02 UTC