MPRI PRFA — Proof Assistants

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, but it's actually must better to perform induction on m.

Lemma add_sub :
  forall n m,
    (n + m) - m = n.forall n m : nat, n + m - m = n
Proof.forall n m : nat, n + m - m = n
  intros n m.n, m: nat
n + m - m = n induction m as [| m ih].n: nat
n + 0 - 0 = n
n, m: nat
ih: n + m - m = n
n + S m - S m = n
  -n: nat
n + 0 - 0 = n rewrite <- plus_n_O.n: nat
n - 0 = n destruct n.0 - 0 = 0
n: nat
S n - 0 = S n all: reflexivity.
  -n, m: nat
ih: n + m - m = n
n + S m - S m = n rewrite <- plus_n_Sm.n, m: nat
ih: n + m - m = n
S (n + m) - S m = n simpl.n, m: nat
ih: n + m - m = n
n + m - m = n assumption.
Qed.add_sub is defined

Shadowing

We have several ways to write the definition of subtraction, depending on whether we reuse the name of the argument or not in the pattern matching. If we reuse the name, the original name is then shadowed which is fine as long as we don't want to mention it again. Sometimes, it is useful to mention it.

Fixpoint sub_1 (n m : nat) :=
  match n, m with
  | 0, m => m
  | S n, 0 => S n
  | S n, S m => sub_1 n m
  end.sub_1 is defined
sub_1 is recursively defined (guarded on 1st argument)

Fixpoint sub_2 (n m : nat) :=
  match n, m with
  | 0, _ => m
  | S _, 0 => n
  | S n, S m => sub_2 n m
  end.sub_2 is defined
sub_2 is recursively defined (guarded on 1st argument)

Discriminating by hand

We write instructions in the document in the form of comments, please follow them! This includes writing the induction principle, or not using certain tactics or libraries, so that you can learn. 🧑‍🎓 When we told you to prove true ≠ false, we were expecting the following.

Lemma true_neq_false : true <> false.true <> false
Proof.true <> false
  intros e.e: true = false
False
  change (if true then False else True).e: true = false
if true then False else True
  rewrite e.e: true = false
True split.
Qed.true_neq_false is defined

Using custom induction principles

When you prove an induction principle, you can use it directly with the induction tactic. Much nicer than applying it by hand.

Lemma strong_nat_ind :
  forall (P : nat -> Prop),
    (forall n, (forall m, m < n -> P m) -> P n) ->
    forall n, P n.forall P : nat -> Prop, (forall n : nat, (forall m : nat, m < n -> P m) -> P n) -> forall n : nat, P n
Admitted.strong_nat_ind is declared

From Stdlib Require Import Lia.

Fixpoint even3 (n : nat) : Prop :=
  match n with
  | 0 => True
  | 1 => False
  | S (S n) => even3 n
  end.even3 is defined
even3 is recursively defined (guarded on 1st argument)

Inductive even4 : nat -> Prop :=
| evenO : even4 0
| evenS n : even4 n -> even4 (S (S n)).even4 is defined
even4_ind is defined
even4_sind is defined

Lemma even3_to_even4 : forall n, even3 n -> even4 n.forall n : nat, even3 n -> even4 n
Proof.forall n : nat, even3 n -> even4 n
  intros n h.n: nat
h: even3 n
even4 n
  induction n as [n ih] using strong_nat_ind.n: nat
ih:= forall m: nat, m < n -> even3 m -> even4 m
h: even3 n
even4 n
  destruct n as [| [| n]].ih:= forall m: nat, m < 0 -> even3 m -> even4 m
h: even3 0
even4 0
ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: even3 1
even4 1
n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 (S (S n))
  -ih:= forall m: nat, m < 0 -> even3 m -> even4 m
h: even3 0
even4 0 constructor.
  -ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: even3 1
even4 1 simpl in h.ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: False
even4 1 contradiction.
  -n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 (S (S n)) constructor.n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 n apply ih.n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
n < S (S n)
n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even3 n
    +n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
n < S (S n) lia.
    +n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even3 n assumption.
Qed.even3_to_even4 is defined

SELF-EVALUATION TIME

Finally, we would like you to try to do the following on paper, that is without using Rocq 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?

Goal forall P Q, P \/ Q -> Q \/ P.forall P Q : Prop, P \/ Q -> Q \/ P
Proof.forall P Q : Prop, P \/ Q -> Q \/ P
  intros P Q h.P, Q: Prop
h: P \/ Q
Q \/ P
  destruct h as [h | h].P, Q: Prop
h: P
Q \/ P
P, Q: Prop
h: Q
Q \/ P
  -P, Q: Prop
h: P
Q \/ P left.P, Q: Prop
h: P
Q

Here, what is the goal?

Abort.

EXERCISE

Prove 0 ≠ 1 without automation.