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?

@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.
```

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.

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.

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.
```

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