Stream: Coq users

Topic: How to do induction?


view this post on Zulip 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?

view this post on Zulip 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 .

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Feb 13 2024 at 12:35):

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

view this post on Zulip 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..

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC