PRFA.review2
Reviewing session 2
Think before you prove
We all jump right in the proof and it can be quite fun, but sometimes just
thinking a little will save some trouble.
Let us look at the add_sub example from the exercise session.
It might be tempting to prove things by induction on n, after all it's the
first variable we have in the context.
Lemma add_sub :
∀ n m,
(n + m) - m = n.
Proof.
intros n m. induction m as [| m ih].
- rewrite <- plus_n_O. destruct n. all: reflexivity.
- rewrite <- plus_n_Sm. simpl. assumption.
Qed.
Generalising
We don't always get the induction hypothesis we hoped for. But often it's
just a question of generalising the goal before applying induction.
Fixpoint eq_nat (x y : nat) : bool :=
match x, y with
| 0, 0 ⇒ true
| 0, S _ ⇒ false
| S _, 0 ⇒ false
| S x', S y' ⇒ eq_nat x' y'
end.
Lemma eq_nat_spec :
∀ n m,
eq_nat n m = true ↔ n = m.
Proof.
intros n. (* Note how we do not introduce m yet. *)
induction n as [| n ih].
- intros m. destruct m.
+ simpl. split. all: reflexivity.
+ simpl. split. all: discriminate.
- intros m. destruct m.
+ simpl. split. all: discriminate.
+ simpl. split.
× intro h. f_equal. apply ih. assumption.
× intro h. apply ih. inversion h. reflexivity.
Qed.
Proving strong results
Sometimes the above is not sufficient and we need to actually state something
stronger. This is for instance what we get with strong induction on natural
numbers (this is also called course-of-value induction).
EXERCISE
Lemma strong_nat_ind :
∀ (P : nat → Prop),
(∀ n, (∀ m, m < n → P m) → P n) →
∀ n, P n.
Proof.
intros P h n.
assert (hn : ∀ m, m ≤ n → P m).
{ induction n as [| n ih].
- intros m hm. inversion hm.
apply h. intros k hk. lia. (* lia knows there can't be k < 0 *)
- intros m hm. inversion hm.
+ apply h. intros k hk. apply ih. lia.
+ apply ih. lia.
}
apply hn. lia.
Qed.
∀ (P : nat → Prop),
(∀ n, (∀ m, m < n → P m) → P n) →
∀ n, P n.
Proof.
intros P h n.
assert (hn : ∀ m, m ≤ n → P m).
{ induction n as [| n ih].
- intros m hm. inversion hm.
apply h. intros k hk. lia. (* lia knows there can't be k < 0 *)
- intros m hm. inversion hm.
+ apply h. intros k hk. apply ih. lia.
+ apply ih. lia.
}
apply hn. lia.
Qed.
Remember that you can use those with the induction tactic.
Fixpoint even2 (n : nat) :=
match n with
| 0 ⇒ true
| 1 ⇒ false
| S (S n) ⇒ even2 n
end.
Fixpoint even3 (n : nat) : Prop :=
match n with
| 0 ⇒ True
| 1 ⇒ False
| S (S n) ⇒ even3 n
end.
Lemma even2_iff_even3 : ∀ n, even2 n = true ↔ even3 n.
Proof.
intros n.
induction n as [n ih] using strong_nat_ind.
destruct n as [| [| n]].
- simpl. split.
+ intro. constructor.
+ reflexivity.
- simpl. split.
+ discriminate.
+ contradiction.
- simpl. apply ih. lia.
Qed.
SELF-EVALUATION TIME
Finally, we would like to try and do the following on paper, that is without
using Coq on your computer to tell you the answer!
EXERCISE
Write down the induction principle for list.
EXERCISE
What is the goal after the following script?