## Stream: Coq users

### Topic: How to do induction?

#### Julin Shaji (Feb 13 2024 at 11:50):

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?

#### Cyril Cohen (Feb 13 2024 at 12:04):

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 .

#### Julin Shaji (Feb 13 2024 at 12:29):

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.

#### Julin Shaji (Feb 13 2024 at 12:35):

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

#### Julin Shaji (Feb 13 2024 at 12:39):

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

#### Julin Shaji (Feb 14 2024 at 04:52):

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?

#### Ike Mulder (Feb 14 2024 at 08:53):

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

#### Ike Mulder (Feb 14 2024 at 08:58):

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

#### Pierre Roux (Feb 14 2024 at 09:30):

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

#### Ana de Almeida Borges (Feb 14 2024 at 12:57):

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