MPRI PRFA — Proof Assistants

Reviewing session 3

Proving with proof terms

If you find it hard, it's perfectly normal! It takes some time to get used to it, but it is worth it. Now when programming you can use proof-theoretic intuition, and when proving you can use programmer's intuition, this is a very powerful tool!

Let us look again at Russel for the exercises. We'll do it step by step.

Definition Russel X : ~ (X <-> ~ X).X: Prop
~ (X <-> ~ X)
Proof.X: Prop
~ (X <-> ~ X)

We want to prove a negation, that's just a function to False

  refine (fun h => _).X: Prop
h: X <-> ~ X
False

Now we have X <-> ~ X which is a conjunction, so we match on it.

  refine (match h with conj f g => _ end).X: Prop
h: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
False

What can we do now? To prove False, there is not much else we can do besides applying f since f _ is of type ~ X which is X -> False. In other words f _ _ is of type False. What does f expect as two arguments? In both cases X, so we might as well just prove it once with a let.

  refine (let x := _ in f x x).X: Prop
h: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
X

Again, we don't really have a choice but to apply g.

  refine (g _).X: Prop
h: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
~ X

We know the drill.

  refine (fun x => _).X: Prop
h: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
x: X
False

It might seem like we're back where we started, but not really… We have x : X now!

  refine (f x x).
Abort.

If we combine all of that, we get

Definition Russel X : ~ (X <-> ~ X) :=
  fun h =>
    let 'conj f g := h in
    let x : X := g (fun x => f x x) in
    f x x.Russel is defined

Remark. The X in the definition above is on the left of the colon : so it needs not be introduced (with fun X => _) in the body of the definition.

Implicit arguments

When writing proof terms, implicit arguments become all the more important. Let's look at one of the very first exercises.

Inductive lt (n : nat) : nat -> Prop :=
| lt_B : lt n (S n)
| lt_S m : lt n m -> lt n (S m).lt is defined
lt_ind is defined
lt_sind is defined

Definition lt_plus_4 n m : lt n m -> lt n (4 + m) :=
  fun h => lt_S _ _ (lt_S _ _ (lt_S _ _ (lt_S _ _ h))).lt_plus_4 is defined

Now we make lt_S easier to use by making n, m implicit

Arguments lt_S {n m}.

Definition lt_plus_4' n m : lt n m -> lt n (4 + m) :=
  fun h => lt_S (lt_S (lt_S (lt_S h))).lt_plus_4' is defined

Impredicative encodings

Before there were inductive types, logical connectives were defined using so-called impredicative encodings.

Note: Even datatypes were defined this way, in the advanced exercises, this was the case of the Church encoding of natural numbers.

Impredicative encodings essentially define a type as their eliminator. In other words, think about how you use it.

For False, elimination states that you can prove any other proposition from it, hence the following definition:

Definition iFalse :=
  forall (P : Prop), P.iFalse is defined

Notice the similarity with False_ind.

Check False_ind.False_ind
     : forall P : Prop, False -> P

For conjunction, it's the same idea.

Check and_ind.and_ind
     : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P

Definition iAnd (A B : Prop) :=
  forall (P : Prop), (A -> B -> P) -> P.iAnd is defined

Now apply plays the role of destruct for such a proof.

Lemma iAnd_and :
  forall A B,
    iAnd A B ->
    A /\ B.forall A B : Prop, iAnd A B -> A /\ B
Proof.forall A B : Prop, iAnd A B -> A /\ B
  intros A B h.A, B: Prop
h: iAnd A B
A /\ B

With A /\ B the following would be destruct h as [hA hB].

  apply h.A, B: Prop
h: iAnd A B
A -> B -> A /\ B intros hA hB.A, B: Prop
h: iAnd A B
hA: A
hB: B
A /\ B
  split.A, B: Prop
h: iAnd A B
hA: A
hB: B
A
A, B: Prop
h: iAnd A B
hA: A
hB: B
B all: assumption.
Qed.iAnd_and is defined

Now for exists x, P x.

Check ex_ind.ex_ind
     : forall (A : Type) (P : A -> Prop) (P0 : Prop), (forall x : A, P x -> P0) -> (exists y, P y) -> P0

Definition iEx A (P : A -> Prop) :=
  forall (Q : Prop),
    (forall x, P x -> Q) ->
    Q.iEx is defined

Lemma iEx_ex :
  forall A P,
    iEx A P ->
    exists x, P x.forall (A : Type) (P : A -> Prop), iEx A P -> exists x : A, P x
Proof.forall (A : Type) (P : A -> Prop), iEx A P -> exists x : A, P x
  intros A P h.A: Type
P: A -> Prop
h: iEx A P
exists x : A, P x
  apply h.A: Type
P: A -> Prop
h: iEx A P
forall x : A, P x -> exists x0 : A, P x0 intros x hx.A: Type
P: A -> Prop
h: iEx A P
x: A
hx: P x
exists x0 : A, P x0
  exists x.A: Type
P: A -> Prop
h: iEx A P
x: A
hx: P x
P x assumption.
Qed.iEx_ex is defined

SELF-EVALUATION TIME

We'll do again some paper proving.

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS n : even n -> even (S (S n)).even is defined
even_ind is defined
even_sind is defined

EXERCISE

Write down the induction principle for even.

REMINDER

Inductive or (A B : Prop) : Prop := | or_introl : A -> A / B | or_intror : B -> A / B.

Notation "A \/ B" := (or A B).

EXERCISE

What is a proof term of the following type?

Definition or_imp :
  forall (P Q R : Prop), (P -> R) -> (Q -> R) -> P \/ Q -> R.forall P Q R : Prop, (P -> R) -> (Q -> R) -> P \/ Q -> R
Abort.

EXERCISE

What is the goal after the following script?

Lemma true_false :
  true <> false.true <> false
Proof.true <> false
  intro 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

Here.

Abort.

EXERCISE

Inductive le (n : nat) : nat -> Prop := | le_n : n <= n | le_S : forall m, n <= m -> n <= S m.

EXERCISE

What is the goal after the following script?

Lemma le_n_S :
  forall n m,
    n <= m ->
    S n <= S m.forall n m : nat, n <= m -> S n <= S m
Proof.forall n m : nat, n <= m -> S n <= S m
  intros n m h.n, m: nat
h: n <= m
S n <= S m
  induction h.n: nat
S n <= S n
n, m: nat
h: n <= m
IHh: S n <= S m
S n <= S (S m)
  -n: nat
S n <= S n constructor.
  -n, m: nat
h: n <= m
IHh: S n <= S m
S n <= S (S m)

Here.

Abort.