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: Oct 13 2024 at 01:02 UTC