Hi.

I was trying a simple proof like this:

```
Require Import ssreflect.
Inductive t: Type :=
| Over
| More: t -> t -> t.
Fixpoint teqb (s1 s2: t): bool :=
match s1, s2 with
| Over, Over => true
| More a1 b1, More a2 b2 => andb (teqb a1 a2) (teqb b1 b2)
| _, _ => false
end.
Lemma eqb_same: forall s1 s2: t, teqb s1 s2 = true -> s1 = s2.
Proof.
move => s1 s2.
elim s1 => [|a1 IHa1 b1 IHb1]; first by elim s2.
elim s2 => [|a2 IHa2 b2 IHb2]; first by [].
(*
s1, s2, a1 : t
IHa1 : teqb a1 s2 = true -> a1 = s2
b1 : t
IHb1 : teqb b1 s2 = true -> b1 = s2
a2 : t
IHa2 : teqb (More a1 b1) a2 = true -> More a1 b1 = a2
b2 : t
IHb2 : teqb (More a1 b1) b2 = true -> More a1 b1 = b2
========================= (1 / 1)
teqb (More a1 b1) (More a2 b2) = true -> More a1 b1 = More a2 b2
*)
```

But couldn't figure out how to do the induction.

How can I finish this? Am I doing something wrong?

You need to simplify the premise `teqb (More a1 b1) (More a2 b2) = true`

, extract the two conjuncts from it (I suggest you use `Require Import ssrbool`

and use lemma `andP`

for that) and then use the induction hypothesis.

BTW you do not need to use elim all the time, one is enough on the structurally decreasing argument (`s1`

) and you can use case for all the other .

BTW you do not need to use elim all the time, one is enough on the structurally

decreasing argument (s1) and you can use case for all the other .

Oh.. Thanks! I had been doing this all the time.

Does extracting the conjuncts mean somehow reflecting the bool to Prop? How can that be done?

Could make a `reflect (teqb a1 a2 /\ teqb b1 b2) (teqb a1 a2 && teqb b1 b2)`

value with `andP`

but I guess that's not the way..

I got a rather not-so-good looking proof:

```
Lemma eqb_same: forall s1 s2: t, teqb s1 s2 = true -> s1 = s2.
Proof.
elim => [|a1 IHa1 b1 IHb1]; first by elim.
case => [|a2 b2]; first by [].
rewrite //= => H.
pose proof (Bool.andb_true_iff (teqb a1 a2) (teqb b1 b2)) as [[H1 H2] _]; first by [].
by rewrite (IHa1 a2 H1) (IHb1 b2 H2).
Qed.
```

Presence of `pose proof`

makes it look weird to me. And how could we have used `andP`

here?

Minimal changes to the proof, but now using `andP`

:

```
Lemma eqb_same: forall s1 s2: t, teqb s1 s2 = true -> s1 = s2.
Proof.
elim => [|a1 IHa1 b1 IHb1]; first by elim.
case => [|a2 b2]; first by [].
rewrite //= => /andP [/IHa1 -> /IHb1 ->] //.
Qed.
```

If you like unreadable one liners:

```
Lemma eqb_same: forall s1 s2: t, teqb s1 s2 = true -> s1 = s2.
Proof. elim => [[|]|? IHa1 ? IHb1 [|??]] // /andP [/IHa1-> /IHb1->] //. Qed.
```

You can even save a few more characters but indeed that's debatable in terms of readability:

```
Lemma eqb_same : forall s1 s2 : t, teqb s1 s2 = true -> s1 = s2.
Proof. by elim=> [|? IHa1 ? IHb1] [] // ? ? /andP[/IHa1-> /IHb1->]. Qed.
```

Julin Shaji said:

Presence of

`pose proof`

makes it look weird to me. What could be a better way to write this?

The ssr version of `pose proof`

is `have`

. You can use if both for postulating known facts and facts-to-be-proved:

```
have H := existing_theorem.
have H : statement_to_be_proved.
```

Last updated: Jun 13 2024 at 19:02 UTC