Waterproof Tutorial

Try to solve the exercises below by inspecting the examples. Not sure how to start? You can type Ctrl + space or Command + space to get a list of possible options.

Require Import Rbase.
Require Import Rfunctions.

Require Import Waterproof.Waterproof.
Require Import Waterproof.Notations.Common.
Require Import Waterproof.Notations.Reals.
Require Import Waterproof.Notations.Sets.
Require Import Waterproof.Chains.
Require Import Waterproof.Tactics.
Require Import Waterproof.Libs.Analysis.SupAndInf.
Require Import Waterproof.Automation.

Waterproof Enable Automation RealsAndIntegers.

Open Scope R_scope.
Open Scope subset_scope.
Set Default Goal Selector "!".

Set Nested Proofs Allowed.

Notation "'max(' x , y )" := (Rmax x y)
  (format "'max(' x ,  y ')'").
Notation "'min(' x , y )" := (Rmin x y)
  (format "'min(' x ,  y ')'").

# 1. We conclude that

Example:

Lemma example_reflexivity :
  0 = 0.0 = 0
Proof.0 = 0
Help. (* optional, ask for help, remove from final proof *)The goal can be shown immediately, use
    We conclude that (...).
The goal can be shown immediately, use
    We conclude that (...).
0 = 0
We conclude that (0 = 0).
Qed.

Try it yourself:

Note: Note sure how to continue? You can always write the sentence Help. in your proof to ask for help. Please remove the sentence from your final proof.

Lemma exercise_reflexivity :
  3 = 3.3 = 3
Proof.3 = 3

Admitted.

2. We need to show that

Sometimes it is useful to remind the reader or yourself of what you need to show.

Example

Lemma example_we_need_to_show_that :
  2 = 2.2 = 2
Proof.2 = 2
We need to show that (2 = 2).2 = 2
We conclude that (2 = 2).
Qed.

Try it yourself

Lemma exercise_we_need_to_show_that :
  7 = 7.7 = 7
Proof.7 = 7

Admitted.

3. Show for-all statements: take arbitrary values

Example:

Lemma example_take :
  ∀ x ∈ ℝ,
    x = x.∀ x ∈ ℝ, x = x
Proof.∀ x ∈ ℝ, x = x
Take x ∈ ℝ.x: ℝ
_H: x ∈ ℝ
x = x
We conclude that (x = x).
Qed.

Try it yourself:

Lemma exercise_take :
  ∀ x ∈ ℝ,
    x + 3 = 3 + x.∀ x ∈ ℝ, x + 3 = 3 + x
Proof.∀ x ∈ ℝ, x + 3 = 3 + x

Admitted.

4. Show there-exists statements: choose values

Example

Lemma example_choose :
  ∃ y ∈ ℝ,
    y < 3.∃ y ∈ ℝ, y < 3
Proof.∃ y ∈ ℝ, y < 3
Choose y := (2).y:= 2: ℝ
_defeq: y = 2
Add the following line to the proof:

{ Indeed, (y ∈ ℝ). }

or write:

{ We need to verify that (y ∈ ℝ).

}

if intermediary proof steps are required.
y:= 2: ℝ
_defeq: y = 2
Add the following line to the proof:

We need to show that (y < 3).

or write:

We conclude that (y < 3).

if no intermediary proof steps are required.
*y:= 2: ℝ
_defeq: y = 2
Add the following line to the proof:

{ Indeed, (y ∈ ℝ). }

or write:

{ We need to verify that (
y ∈ ℝ).

}

if intermediary proof steps are required. Indeed, (y ∈ ℝ).
*y:= 2: ℝ
_defeq: y = 2
Add the following line to the proof:

We need to show that (y < 3).

or write:

We conclude that (y < 3).

if no intermediary proof steps are required. We conclude that (y < 3).
Qed.

Try it yourself

Lemma exercise_choose :
  ∃ z > 10,
    z < 14.∃ z > 10, z < 14
Proof.∃ z > 10, z < 14

Admitted.

5. Combine for-all and there-exists statements

Example

Lemma example_combine_quantifiers :
  ∀ a ∈ ℝ,
    ∀ b > 5,
      ∃ c ∈ ℝ,
        c > b - a.∀ a ∈ ℝ, ∀ b > 5, ∃ c ∈ ℝ, c > b - a
Proof.∀ a ∈ ℝ, ∀ b > 5, ∃ c ∈ ℝ, c > b - a
Take a ∈ (ℝ).a: ℝ
_H: a ∈ ℝ
∀ b > 5, ∃ c ∈ ℝ, c > b - a
Take b > 5.a: ℝ
_H: a ∈ ℝ
b: ℝ
_H0: b > 5
∃ c ∈ ℝ, c > b - a
Choose c := (b - a + 1).a: ℝ
_H: a ∈ ℝ
b: ℝ
_H0: b > 5
c:= b - a + 1: ℝ
_defeq: c = b - a + 1
Add the following line to the proof:

{ Indeed, (c ∈ ℝ). }

or write:

{ We need to verify that (c ∈ ℝ).

}

if intermediary proof steps are required.
a: ℝ
_H: a ∈ ℝ
b: ℝ
_H0: b > 5
c:= b - a + 1: ℝ
_defeq: c = b - a + 1
Add the following line to the proof:

We need to show that (c > b - a).

or write:

We conclude that (c > b - a).

if no intermediary proof steps are required.
*a: ℝ
_H: a ∈ ℝ
b: ℝ
_H0: b > 5
c:= b - a + 1: ℝ
_defeq: c = b - a + 1
Add the following line to the proof:

{ Indeed, (c ∈ ℝ). }

or write:

{ We need to verify that (
c ∈ ℝ).

}

if intermediary proof steps are required. Indeed, (c ∈ ℝ).
*a: ℝ
_H: a ∈ ℝ
b: ℝ
_H0: b > 5
c:= b - a + 1: ℝ
_defeq: c = b - a + 1
Add the following line to the proof:

We need to show that (c > b - a).

or write:

We conclude that (c > b - a).

if no intermediary proof steps are required. We conclude that (c > b - a).
Qed.

Try it yourself

Lemma exercise_combine_quantifiers :
  ∀ x > 3,
    ∀ y ≥ 4,
      ∃ z ∈ ℝ,
        x < z - y.∀ x > 3, ∀ y ≥ 4, ∃ z ∈ ℝ, x < z - y
Proof.∀ x > 3, ∀ y ≥ 4, ∃ z ∈ ℝ, x < z - y

Admitted.

6. Make an assumption

Example

Lemma example_assumptions :
  ∀ a ∈ ℝ,
    a < 0 ⇒ - a > 0.∀ a ∈ ℝ, a < 0 ⇨ - a > 0
Proof.∀ a ∈ ℝ, a < 0 ⇨ - a > 0
Take a ∈ (ℝ).a: ℝ
_H: a ∈ ℝ
a < 0 ⇨ - a > 0
Assume that (a < 0).a: ℝ
_H: a ∈ ℝ
_H0: a < 0
- a > 0
We conclude that (- a > 0).
Qed.

Another example with explicit labels

Lemma example_assumptions_2 :
  ∀ a ∈ ℝ,
    a < 0 ⇒ - a > 0.∀ a ∈ ℝ, a < 0 ⇨ - a > 0
Proof.∀ a ∈ ℝ, a < 0 ⇨ - a > 0
Take a ∈ (ℝ).a: ℝ
_H: a ∈ ℝ
a < 0 ⇨ - a > 0
Assume that (a < 0) (i). (* The label here is optional *)a: ℝ
_H: a ∈ ℝ
i: a < 0
- a > 0
By (i) we conclude that (- a > 0).
Qed.

Try it yourself

Lemma exercise_assumptions :
  ∀ a ≥ 2,
    ∀ b ∈ ℝ,
      a > 0 ⇒ (b > 0 ⇒ a + b > - 1).∀ a ≥ 2, ∀ b ∈ ℝ, a > 0 ⇨ b > 0 ⇨ a + b > -1
Proof.∀ a ≥ 2, ∀ b ∈ ℝ, a > 0 ⇨ b > 0 ⇨ a + b > -1

Admitted.

7. Chains of (in)equalities

Example

Section monotone_function.
Variable f : ℝ → ℝ.
Parameter f_increasing : ∀ x ∈ ℝ, ∀ y ∈ ℝ, x ≤ y ⇒ f(x) ≤ f(y).

Lemma example_inequalities:
  2 < f(0) ⇒ 2 < f(1).f: ℝ ⇨ ℝ
2 < f(0) ⇨ 2 < f(1)
Proof.f: ℝ ⇨ ℝ
2 < f(0) ⇨ 2 < f(1)
Assume that (2 < f(0)).f: ℝ ⇨ ℝ
_H: 2 < f(0)
2 < f(1)
By (f_increasing) we conclude that (& 2 < f(0) ≤ f(1)).
Qed.

Try it yourself

Lemma exercise_inequalities:
  f(3) < 5 ⇒ f(-1) < 5.f: ℝ ⇨ ℝ
f(3) < 5 ⇨ f(-1) < 5
Proof.f: ℝ ⇨ ℝ
f(3) < 5 ⇨ f(-1) < 5

Admitted.

8. Backwards reasoning in smaller steps

Example

Lemma example_backwards :
  3 < f(0) ⇒ 2 < f(5).f: ℝ ⇨ ℝ
3 < f(0) ⇨ 2 < f(5)
Proof.f: ℝ ⇨ ℝ
3 < f(0) ⇨ 2 < f(5)
Assume that (3 < f(0)).f: ℝ ⇨ ℝ
_H: 3 < f(0)
2 < f(5)
It suffices to show that (f(0) ≤ f(5)).f: ℝ ⇨ ℝ
_H: 3 < f(0)
f(0) ≤ f(5)
By (f_increasing) we conclude that (f(0) ≤ f(5)).
Qed.

Try it yourself

Lemma exercise_backwards :
  f(5) < 4 ⇒ f(-2) < 5.f: ℝ ⇨ ℝ
f(5) < 4 ⇨ f(-2) < 5
Proof.f: ℝ ⇨ ℝ
f(5) < 4 ⇨ f(-2) < 5

Admitted.

9. Forwards reasoning in smaller steps

Example

Lemma example_forwards :
  7 < f(-1) ⇒ 2 < f(6).f: ℝ ⇨ ℝ
7 < f(-1) ⇨ 2 < f(6)
Proof.f: ℝ ⇨ ℝ
7 < f(-1) ⇨ 2 < f(6)
Assume that (7 < f(-1)).f: ℝ ⇨ ℝ
_H: 7 < f(-1)
2 < f(6)
By (f_increasing) it holds that (f(-1) ≤ f(6)).f: ℝ ⇨ ℝ
_H: 7 < f(-1)
_H0: f(-1) ≤ f(6)
2 < f(6)
We conclude that (2 < f(6)).
Qed.

Try it yourself

Lemma exercise_forwards :
  f(7) < 8 ⇒ f(3) ≤ 10.f: ℝ ⇨ ℝ
f(7) < 8 ⇨ f(3) ≤ 10
Proof.f: ℝ ⇨ ℝ
f(7) < 8 ⇨ f(3) ≤ 10

Admitted.

End monotone_function.

10. Use a for-all statement

Example

Lemma example_use_for_all :
  ∀ x ∈ ℝ,
    (∀ ε > 0, x < ε) ⇒
       x + 1/2 < 1.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ x + 1 / 2 < 1
Proof.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ x + 1 / 2 < 1
Take x ∈ ℝ.x: ℝ
_H: x ∈ ℝ
(∀ ε > 0, x < ε) ⇨ x + 1 / 2 < 1
Assume that (∀ ε > 0, x < ε) (i).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
x + 1 / 2 < 1
Use ε := (1/2) in (i).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
_H0: 1 / 2 > 0 ⇨ x < 1 / 2
Add the following line to the proof:

{ Indeed, (1 / 2 > 0). }

or write:

{ We need to verify that (1 / 2 > 0).

}

if intermediary proof steps are required.
x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
_H0: x < 1 / 2
_H1: 1 / 2 > 0
Add the following line to the proof:

It holds that (x < 1 / 2).
*x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
_H0: 1 / 2 > 0 ⇨ x < 1 / 2
Add the following line to the proof:

{ Indeed, (1 / 2 > 0). }

or write:

{ We need to verify that (1 / 2 > 0).

}

if intermediary proof steps are required. Indeed, (1 / 2 > 0).
*x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
_H0: x < 1 / 2
_H1: 1 / 2 > 0
Add the following line to the proof:

It holds that (x < 1 / 2). It holds that  (x < 1 / 2).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x < ε
_H1: 1 / 2 > 0
_H2: x < 1 / 2
x + 1 / 2 < 1
  We conclude that (x + 1/2 < 1).
Qed.

Try it yourself

Lemma exercise_use_for_all:
  ∀ x ∈ ℝ,
    (∀ ε > 0, x < ε) ⇒
       10 * x < 1.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ 10 * x < 1

Proof.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ 10 * x < 1

Admitted.

11. Use a there-exists statement

Example

Lemma example_use_there_exists :
  ∀ x ∈ ℝ,
    (∃ y > 10, y < x) ⇒
      10 < x.∀ x ∈ ℝ, (∃ y > 10, y < x) ⇨ 10 < x
Proof.∀ x ∈ ℝ, (∃ y > 10, y < x) ⇨ 10 < x
Take x ∈ ℝ.x: ℝ
_H: x ∈ ℝ
(∃ y > 10, y < x) ⇨ 10 < x
Assume that (∃ y > 10, y < x) (i).x: ℝ
_H: x ∈ ℝ
i: ∃ y > 10, y < x
10 < x
Obtain such a y.x: ℝ
_H: x ∈ ℝ
y: ℝ
_H1: y > 10
_H0: y < x
i: ∃ y > 10, y < x
10 < x
We conclude that (& 10 < y < x).
Qed.

Another example

Lemma example_use_there_exists_2 :
  ∀ x ∈ ℝ,
    (∃ y > 14, y < x) ⇒
      12 < x.∀ x ∈ ℝ, (∃ y > 14, y < x) ⇨ 12 < x
Proof.∀ x ∈ ℝ, (∃ y > 14, y < x) ⇨ 12 < x
Take x ∈ ℝ.x: ℝ
_H: x ∈ ℝ
(∃ y > 14, y < x) ⇨ 12 < x
Assume that (∃ y > 14, y < x) (i).x: ℝ
_H: x ∈ ℝ
i: ∃ y > 14, y < x
12 < x
Obtain y according to (i).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H1: y > 14
_H0: y < x
i: ∃ y > 14, y < x
12 < x
We conclude that (& 12 < y < x).
Qed.

Try it yourself

Lemma exercise_use_there_exists :
  ∀ z ∈ ℝ,
    (∃ x ≥ 5, x^2 < z) ⇒
      25 < z.∀ z ∈ ℝ, (∃ x ≥ 5, x ^ 2 < z) ⇨ 25 < z

Proof.∀ z ∈ ℝ, (∃ x ≥ 5, x ^ 2 < z) ⇨ 25 < z

Admitted.

12. Argue by contradiction

Example

Lemma example_contradicition :
  ∀ x ∈ ℝ,
    (∀ ε > 0, x > 1 - ε) ⇒
      x ≥ 1.∀ x ∈ ℝ, (∀ ε > 0, x > 1 - ε) ⇨ x ≥ 1
Proof.∀ x ∈ ℝ, (∀ ε > 0, x > 1 - ε) ⇨ x ≥ 1
Take x ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
(∀ ε > 0, x > 1 - ε) ⇨ x ≥ 1
Assume that (∀ ε > 0, x > 1 - ε) (i).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
x ≥ 1
We need to show that (x ≥ 1).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
x ≥ 1
We argue by contradiction.x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
Add the following line to the proof:

Assume that (¬ x ≥ 1).
Assume that (¬ (x ≥ 1)).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
_H0: ¬ x ≥ 1
Derive a contradiction.
It holds that ((1 - x) > 0).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
_H0: ¬ x ≥ 1
_H1: 1 - x > 0
Derive a contradiction.
By (i) it holds that (x > 1 - (1 - x)).x: ℝ
_H: x ∈ ℝ
i: ∀ ε > 0, x > 1 - ε
_H0: ¬ x ≥ 1
_H1: 1 - x > 0
_H2: x > 1 - (1 - x)
Derive a contradiction.
Contradiction.
Qed.

Try it yourself

Lemma exercise_contradiction :
  ∀ x ∈ ℝ,
    (∀ ε > 0, x < ε)
      ⇒ x ≤ 0.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ x ≤ 0
Proof.∀ x ∈ ℝ, (∀ ε > 0, x < ε) ⇨ x ≤ 0

Admitted.

13. Split into cases

Example

Lemma example_cases :
  ∀ x ∈ ℝ, ∀ y ∈ ℝ,
    max(x, y) = x ∨ max(x, y) = y.∀ x ∈ ℝ, ∀ y ∈ ℝ, max(x, y) = x ∨ max(x, y) = y
Proof.∀ x ∈ ℝ, ∀ y ∈ ℝ, max(x, y) = x ∨ max(x, y) = y

Take x ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
∀ y ∈ ℝ, max(x, y) = x ∨ max(x, y) = y
Take y ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
max(x, y) = x ∨ max(x, y) = y
Either (x < y) or (x ≥ y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x < y
Add the following line to the proof:

- Case (x < y).
x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x ≥ y
Add the following line to the proof:

- Case (x ≥ y).
-x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x < y
Add the following line to the proof:

- Case (x < y). Case (x < y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x < y
max(x, y) = x ∨ max(x, y) = y
  It suffices to show that (max(x, y) = y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x < y
max(x, y) = y
  We conclude that (max(x, y) = y).
-x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x ≥ y
Add the following line to the proof:

- Case (x ≥ y). Case (x ≥ y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x ≥ y
max(x, y) = x ∨ max(x, y) = y
  It suffices to show that (max(x, y) = x).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
H: x ≥ y
max(x, y) = x
  We conclude that (max(x, y) = x).
Qed.

Try it yourself

Lemma exercises_cases :
  ∀ x ∈ ℝ, ∀ y ∈ ℝ,
    min(x, y) = x ∨ min(x, y) = y.∀ x ∈ ℝ, ∀ y ∈ ℝ, min(x, y) = x ∨ min(x, y) = y
Proof.∀ x ∈ ℝ, ∀ y ∈ ℝ, min(x, y) = x ∨ min(x, y) = y

Admitted.

14. Prove two statements: A ∧ B

Example

Lemma example_both_statements :
  ∀ x ∈ ℝ, x^2 ≥ 0 ∧ | x | ≥ 0.∀ x ∈ ℝ, x ^ 2 ≥ 0 ∧ |x| ≥ 0
Proof.∀ x ∈ ℝ, x ^ 2 ≥ 0 ∧ |x| ≥ 0
Take x ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
x ^ 2 ≥ 0 ∧ |x| ≥ 0
We show both statements.x: ℝ
_H: x ∈ ℝ
Add the following line to the proof:

We need to show that (x ^ 2 ≥ 0).

or write:

We conclude that (x ^ 2 ≥ 0).

if no intermediary proof steps are required.
x: ℝ
_H: x ∈ ℝ
Add the following line to the proof:

We need to show that (|x| ≥ 0).

or write:

We conclude that (|x| ≥ 0).

if no intermediary proof steps are required.
*x: ℝ
_H: x ∈ ℝ
Add the following line to the proof:

We need to show that (x ^ 2 ≥ 0).

or write:

We conclude that (x ^ 2 ≥ 0).

if no intermediary proof steps are required. We need to show that (x^2 ≥ 0).x: ℝ
_H: x ∈ ℝ
x ^ 2 ≥ 0
  We conclude that (x^2 ≥ 0).
*x: ℝ
_H: x ∈ ℝ
Add the following line to the proof:

We need to show that (|x| ≥ 0).

or write:

We conclude that (|x| ≥ 0).

if no intermediary proof steps are required. We need to show that (| x | ≥ 0).x: ℝ
_H: x ∈ ℝ
|x| ≥ 0
  We conclude that (| x | ≥  0).
Qed.

Try it yourself

Lemma exercise_both_statements :
  ∀ x ∈ ℝ, 0 * x = 0 ∧ x + 1 > x.∀ x ∈ ℝ, 0 * x = 0 ∧ x + 1 > x
Proof.∀ x ∈ ℝ, 0 * x = 0 ∧ x + 1 > x

Admitted.

15. Show both directions

Example

Lemma example_both_directions :
  ∀ x ∈ ℝ, ∀ y ∈ ℝ,
    x < y ⇔ y > x.∀ x ∈ ℝ, ∀ y ∈ ℝ, x < y ⇔ y > x
Proof.∀ x ∈ ℝ, ∀ y ∈ ℝ, x < y ⇔ y > x
Take x ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
∀ y ∈ ℝ, x < y ⇔ y > x
Take y ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
x < y ⇔ y > x
We show both directions.x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
Add the following line to the proof:

We need to show that (x < y ⇨ y > x).

or write:

We conclude that (x < y ⇨ y > x).

if no intermediary proof steps are required.
x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
Add the following line to the proof:

We need to show that (y > x ⇨ x < y).

or write:

We conclude that (y > x ⇨ x < y).

if no intermediary proof steps are required.
++x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
Add the following line to the proof:

We need to show that (x < y ⇨ y > x).

or write:

We conclude that (x < y ⇨ y > x).

if no intermediary proof steps are required. We need to show that (x < y ⇒ y > x).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
x < y ⇨ y > x
   Assume that (x < y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
_H1: x < y
y > x
   We conclude that (y > x).
++x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
Add the following line to the proof:

We need to show that (y > x ⇨ x < y).

or write:

We conclude that (y > x ⇨ x < y).

if no intermediary proof steps are required. We need to show that (y > x ⇒ x < y).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
y > x ⇨ x < y
   Assume that (y > x).x: ℝ
_H: x ∈ ℝ
y: ℝ
_H0: y ∈ ℝ
_H1: y > x
x < y
   We conclude that (x < y).
Qed.

Try it yourself

Lemma exercise_both_directions :
  ∀ x ∈ ℝ, x > 1 ⇔ x - 1 > 0.∀ x ∈ ℝ, x > 1 ⇔ x - 1 > 0
Proof.∀ x ∈ ℝ, x > 1 ⇔ x - 1 > 0

Admitted.

16. Proof by induction

Example

Lemma example_induction :
  ∀ n : ℕ → ℕ, (∀ k ∈ ℕ, (n(k) < n(k+1))%nat) ⇒
    ∀ k ∈ ℕ, (k ≤ n(k))%nat.∀ n,
(∀ k ∈ ℕ, (n(k) < n(k + 1))%nat)
⇨ ∀ k ∈ ℕ, (k ≤ n(k))%nat
Proof.∀ n,
(∀ k ∈ ℕ, (n(k) < n(k + 1))%nat)
⇨ ∀ k ∈ ℕ, (k ≤ n(k))%nat
Take n : (ℕ → ℕ).n: ℕ ⇨ ℕ
(∀ k ∈ ℕ, (n(k) < n(k + 1))%nat)
⇨ ∀ k ∈ ℕ, (k ≤ n(k))%nat
Assume that (∀ k ∈ ℕ, n(k) < n(k+1))%nat.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
∀ k ∈ ℕ, (k ≤ n(k))%nat
We use induction on k.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
Add the following line to the proof:

- We first show the base case ((0 ≤ n(0))%nat).
n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
Add the following line to the proof:

- We now show the induction step.
+n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
Add the following line to the proof:

- We first show the base case ((0 ≤ n(0))%nat). We first show the base case ((0 ≤ n(0))%nat).n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
(0 ≤ n(0))%nat
  We conclude that (0 ≤ n(0))%nat.
+n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
Add the following line to the proof:

- We now show the induction step. We now show the induction step.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
∀ k ∈ ℕ, (k ≤ n(k))%nat ⇨ (k + 1 ≤ n(k + 1))%nat
  Take k ∈ ℕ.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
k: ℕ
_H0: k ∈ ℕ
(k ≤ n(k))%nat ⇨ (k + 1 ≤ n(k + 1))%nat
  Assume that (k ≤ n(k))%nat.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
k: ℕ
_H0: k ∈ ℕ
_H1: (k ≤ n(k))%nat
(k + 1 ≤ n(k + 1))%nat
  It holds that (n(k) < n(k+1))%nat.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
k: ℕ
_H0: k ∈ ℕ
_H1: (k ≤ n(k))%nat
_H2: (n(k) < n(k + 1))%nat
(k + 1 ≤ n(k + 1))%nat
  It holds that (n(k) + 1 ≤ n(k+1))%nat.n: ℕ ⇨ ℕ
_H: ∀ k ∈ ℕ, (n(k) < n(k + 1))%nat
k: ℕ
_H0: k ∈ ℕ
_H1: (k ≤ n(k))%nat
_H2: (n(k) < n(k + 1))%nat
_H3: (n(k) + 1 ≤ n(k + 1))%nat
(k + 1 ≤ n(k + 1))%nat
  We conclude that (& k + 1 ≤ n(k) + 1 ≤ n(k + 1))%nat.
Qed.

Try it yourself

Lemma exercise_induction :
  ∀ F : ℕ → ℕ, (∀ k ∈ ℕ, (F(k+1) = F(k))%nat) ⇒
    ∀ k ∈ ℕ, (F(k) = F(0))%nat.∀ F,
(∀ k ∈ ℕ, F((k + 1)%nat) = F(k))
⇨ ∀ k ∈ ℕ, F(k) = F(0%nat)
Proof.∀ F,
(∀ k ∈ ℕ, F((k + 1)%nat) = F(k))
⇨ ∀ k ∈ ℕ, F(k) = F(0%nat)

Admitted.

17. Expand definitions

By writing Expand the definition of square. you get suggestions on how to use the definition of square in your proof.

Example

Definition square (x : ℝ) := x^2.

Lemma example_expand :
  ∀ x ∈ ℝ, square x ≥ 0.∀ x ∈ ℝ, square(x) ≥ 0
Proof.∀ x ∈ ℝ, square(x) ≥ 0
Take x ∈ (ℝ).x: ℝ
_H: x ∈ ℝ
square(x) ≥ 0
Expand the definition of square.Expanded definition in statements where applicable.
Expanded definition in statements where applicable.
To include these statements, use (one of):
To include these statements, use (one of):
We need to show that (x ^ 2 ≥ 0).
We need to show that (x ^ 2 ≥ 0).
Remove this line in the final version of your proof.
x: ℝ
_H: x ∈ ℝ
square(x) ≥ 0
  (* Remove the above line in your own code! *)
We need to show that (x^2 ≥ 0).x: ℝ
_H: x ∈ ℝ
x ^ 2 ≥ 0
We conclude that (x^2 ≥ 0).
Qed.

Try it yourself

Lemma exercise_expand :
  ∀ x ∈ ℝ, - (square x) ≤ 0.∀ x ∈ ℝ, - square(x) ≤ 0
Proof.∀ x ∈ ℝ, - square(x) ≤ 0

Admitted.