Types and functions

In this class, we'll use Rocq to write programs, and prove things about them! Rocq has three languages: one for commands (the “Vernacular”), one for terms (“Gallina”), and one for proof tactics (“Ltac”).

Let's start by defining a custom type in Gallina, an enumerated type. We define the type day, which has seven constructors: seven possible values for this type.

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

So far this is just an enumerated type, like you would write an enum in C. But we'll see later that we can define much more complex types.

Now, let's write our first function in Gallina, with some pattern-matching. Note that functions have to be total, I have to provide a result for all possible values of the argument.

Definition next_weekday (d: day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

One way to check the result of executing our function is to use the vernacular command Compute. Another way could be to extract our Rocq functions into OCaml or Haskell!

Compute (next_weekday friday).
= monday
: day

Another way is to prove that the execution of my function gives the expected result. Here we'll see our first interactive proof buffer, with an horizontal line. Above the line are our hypotheses (in this particular proof, there aren't any. Below the line is our proof goal.

Theorem next_wed:
  next_weekday wednesday = thursday.
next_weekday wednesday = thursday
Proof.
next_weekday wednesday = thursday
  simpl.
thursday = thursday
  reflexivity.
Qed.

The simpl tactic simplifies the aplication of a function by following its definition. And reflexivity conclude when our goal is an equality were both sides are exactly the same.

Now, I want to prove that our function never returns a day that is part of the weekend. Let us start by defining which days are part of the weekend. This function takes a day and returns a boolean. I could define my own boolean type, just like I did for day. But this is part of the standard library already. Let's look at its definition with Print.

Print bool.
Inductive bool : Set :=  true : bool | false : bool.

Now we can write our weekend definition, returning a boolean. Note that in many cases, Rocq can do some type inference and figure out some types by itself, I could remove all of the type annotations below and the definition would still be accepted.

Definition weekend (d: day) : bool :=
  match d with
  | saturday | sunday => true
  | _ => false
  end.

Gallina is strongly typed, every term has a type. We can check these types with Check. Of course, Rocq will reject ill-typed terms.

Check next_weekday.
next_weekday
     : day -> day
Check (next_weekday monday).
next_weekday monday
     : day
Check (next_weekday true).
The term "true" has type "bool"
while it is expected to have type "day".

We are now ready for our proof, using the universal quantifier forall to quantify over any possible input to the function. This theorem is proved by case analysis over the input d. To do so, we use the tactic destruct. We use - to focus on the current sub-goal and structure our proofs.

Theorem next_not_weekend:
  forall (d: day), weekend (next_weekday d) = false.
forall d : day, weekend (next_weekday d) = false
Proof.
forall d : day, weekend (next_weekday d) = false
  intros d.
d: day
weekend (next_weekday d) = false
  destruct d.
weekend (next_weekday monday) = false
weekend (next_weekday tuesday) = false
weekend (next_weekday wednesday) = false
weekend (next_weekday thursday) = false
weekend (next_weekday friday) = false
weekend (next_weekday saturday) = false
weekend (next_weekday sunday) = false
  -
weekend (next_weekday monday) = false
    simpl next_weekday.
weekend tuesday = false
    simpl weekend.
false = false
    reflexivity.
  -
weekend (next_weekday tuesday) = false simpl.
false = false reflexivity.
  -
weekend (next_weekday wednesday) = false simpl.
false = false reflexivity.
  -
weekend (next_weekday thursday) = false simpl.
false = false reflexivity.
  -
weekend (next_weekday friday) = false simpl.
false = false reflexivity.
  -
weekend (next_weekday saturday) = false simpl.
false = false reflexivity.
  -
weekend (next_weekday sunday) = false simpl.
false = false reflexivity.
Qed.

So far, we only defined a simple enumerated type. But we can define more complex abstract data types. let's define natural numbers and polymorphic lists. Natural numbers use an unary representation, where each number is either 0 or the successor of another natural.

Inductive mynat : Type :=
| O
| S (n:mynat).

Inductive mylist (X:Type) : Type :=
| nil: mylist X
| cons (x:X) (l:mylist X) : mylist X.

In fact, those definitions are already in the standard library. With Search, we can even search for definitions related to these types.

Print list.
Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.

Arguments list A%type_scope
Arguments Datatypes.nil {A}%type_scope
Arguments Datatypes.cons {A}%type_scope a l%list_scope
  (where some original arguments have been renamed)
Print nat.
Inductive nat : Set :=  O : nat | S : nat -> nat.

Arguments Datatypes.S _%nat_scope
Search list.
Datatypes.nil: forall {A : Type}, list A
length: forall [A : Type], list A -> nat
Datatypes.cons:
  forall {A : Type}, A -> list A -> list A
app: forall [A : Type], list A -> list A -> list A
list_ind:
  forall [A : Type] (P : list A -> Prop),
  P Datatypes.nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
  forall l : list A, P l
list_sind:
  forall [A : Type] (P : list A -> SProp),
  P Datatypes.nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
  forall l : list A, P l
list_rect:
  forall [A : Type] (P : list A -> Type),
  P Datatypes.nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
  forall l : list A, P l
list_rec:
  forall [A : Type] (P : list A -> Set),
  P Datatypes.nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
  forall l : list A, P l
Search nat. (* Quite a large list of results! *)
Nat.two: nat
Nat.one: nat
Nat.zero: nat
Datatypes.O: nat
IsSucc: nat -> Prop
Nat.log2: nat -> nat
Nat.succ: nat -> nat
Nat.div2: nat -> nat
Nat.double: nat -> nat
Nat.pred: nat -> nat
Nat.sqrt: nat -> nat
Nat.square: nat -> nat
Datatypes.S: nat -> nat
Nat.tail_mul: nat -> nat -> nat
le: nat -> nat -> Prop
Nat.lxor: nat -> nat -> nat
Nat.ldiff: nat -> nat -> nat
Nat.min: nat -> nat -> nat
ge: nat -> nat -> Prop
lt: nat -> nat -> Prop
Nat.div: nat -> nat -> nat
Nat.tail_add: nat -> nat -> nat
Nat.land: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
Nat.mul: nat -> nat -> nat
Nat.lor: nat -> nat -> nat
Nat.gcd: nat -> nat -> nat
Nat.sub: nat -> nat -> nat
Nat.pow: nat -> nat -> nat
gt: nat -> nat -> Prop
Nat.add: nat -> nat -> nat
Nat.max: nat -> nat -> nat
Nat.of_num_uint: Number.uint -> nat
Nat.of_hex_uint: Hexadecimal.uint -> nat
Nat.to_num_int: nat -> Number.signed_int
Nat.to_hex_int: nat -> Hexadecimal.signed_int
Nat.to_int: nat -> Decimal.signed_int
Nat.to_num_uint: nat -> Number.uint
Nat.to_hex_uint: nat -> Hexadecimal.uint
Nat.odd: nat -> bool
Nat.to_num_hex_uint: nat -> Number.uint
Nat.of_uint: Decimal.uint -> nat
Hexadecimal.nb_digits: Hexadecimal.uint -> nat
Decimal.nb_digits: Decimal.uint -> nat
Nat.to_uint: nat -> Decimal.uint
Nat.even: nat -> bool
Nat.tail_addmul: nat -> nat -> nat -> nat
Hexadecimal.del_tail:
  nat -> Hexadecimal.uint -> Hexadecimal.uint
Nat.ltb: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Decimal.del_tail_int:
  nat -> Decimal.signed_int -> Decimal.signed_int
Hexadecimal.del_tail_int:
  nat ->
  Hexadecimal.signed_int -> Hexadecimal.signed_int
Nat.to_little_uint:
  nat -> Decimal.uint -> Decimal.uint
Decimal.del_tail: nat -> Decimal.uint -> Decimal.uint
Hexadecimal.del_head:
  nat -> Hexadecimal.uint -> Hexadecimal.uint
Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
Nat.compare: nat -> nat -> comparison
Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.to_little_hex_uint:
  nat -> Hexadecimal.uint -> Hexadecimal.uint
Decimal.del_head: nat -> Decimal.uint -> Decimal.uint
Nat.eqb: nat -> nat -> bool
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
le_n: forall n : nat, n <= n
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
length: forall [A : Type], list A -> nat
Nat.iter: nat -> forall {A : Type}, (A -> A) -> A -> A
Decimal.del_head_int:
  nat -> Decimal.signed_int -> Decimal.uint
Nat.of_hex_int: Hexadecimal.signed_int -> option nat
Nat.of_num_int: Number.signed_int -> option nat
Hexadecimal.del_head_int:
  nat -> Hexadecimal.signed_int -> Hexadecimal.uint
Nat.of_int: Decimal.signed_int -> option nat
Decimal.nztail: Decimal.uint -> Decimal.uint * nat
Hexadecimal.nztail:
  Hexadecimal.uint -> Hexadecimal.uint * nat
Hexadecimal.nztail_int:
  Hexadecimal.signed_int ->
  Hexadecimal.signed_int * nat
le_0_n: forall n : nat, 0 <= n
Decimal.nztail_int:
  Decimal.signed_int -> Decimal.signed_int * nat
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
Nat.shiftr:
  (fun _ : nat => nat) 0 ->
  forall n : nat, (fun _ : nat => nat) n
Nat.bitwise:
  (bool -> bool -> bool) -> nat -> nat -> nat -> nat
Nat.shiftl:
  (fun _ : nat => nat) 0 ->
  forall n : nat, (fun _ : nat => nat) n
plus_n_O: forall n : nat, n = n + 0
plus_O_n: forall n : nat, 0 + n = n
mult_n_O: forall n : nat, 0 = n * 0
n_Sn: forall n : nat, n <> Datatypes.S n
pred_Sn: forall n : nat, n = Nat.pred (Datatypes.S n)
le_S: forall n m : nat, n <= m -> n <= Datatypes.S m
Acc_intro_generator:
  forall [A : Type] [R : A -> A -> Prop],
  nat -> well_founded R -> well_founded R
le_pred:
  forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
O_S: forall n : nat, 0 <> Datatypes.S n
le_S_n:
  forall n m : nat,
  Datatypes.S n <= Datatypes.S m -> n <= m
le_n_S:
  forall n m : nat,
  n <= m -> Datatypes.S n <= Datatypes.S m
eq_add_S:
  forall n m : nat,
  Datatypes.S n = Datatypes.S m -> n = m
eq_S:
  forall x y : nat,
  x = y -> Datatypes.S x = Datatypes.S y
f_equal_pred:
  forall x y : nat, x = y -> Nat.pred x = Nat.pred y
max_r: forall n m : nat, n <= m -> Nat.max n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
min_r: forall n m : nat, m <= n -> Nat.min n m = m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
nat_case:
  forall (n : nat) (P : nat -> Prop),
  P 0 -> (forall m : nat, P (Datatypes.S m)) -> P n
plus_Sn_m:
  forall n m : nat,
  Datatypes.S n + m = Datatypes.S (n + m)
plus_n_Sm:
  forall n m : nat,
  Datatypes.S (n + m) = n + Datatypes.S m
f_equal_nat:
  forall (B : Type) (f : nat -> B) (x y : nat),
  x = y -> f x = f y
nat_sind:
  forall P : nat -> SProp,
  P 0 ->
  (forall n : nat, P n -> P (Datatypes.S n)) ->
  forall n : nat, P n
nat_rec:
  forall P : nat -> Set,
  P 0 ->
  (forall n : nat, P n -> P (Datatypes.S n)) ->
  forall n : nat, P n
nat_rect:
  forall P : nat -> Type,
  P 0 ->
  (forall n : nat, P n -> P (Datatypes.S n)) ->
  forall n : nat, P n
nat_ind:
  forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (Datatypes.S n)) ->
  forall n : nat, P n
mult_n_Sm:
  forall n m : nat, n * m + n = n * Datatypes.S m
not_eq_S:
  forall n m : nat,
  n <> m -> Datatypes.S n <> Datatypes.S m
f_equal2_plus:
  forall x1 y1 x2 y2 : nat,
  x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
  forall x1 y1 x2 y2 : nat,
  x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
f_equal2_nat:
  forall (B : Type) (f : nat -> nat -> B)
    (x1 y1 x2 y2 : nat),
  x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
le_sind:
  forall (n : nat) (P : nat -> SProp),
  P n ->
  (forall m : nat, n <= m -> P m -> P (Datatypes.S m)) ->
  forall n0 : nat, n <= n0 -> P n0
le_ind:
  forall (n : nat) (P : nat -> Prop),
  P n ->
  (forall m : nat, n <= m -> P m -> P (Datatypes.S m)) ->
  forall n0 : nat, n <= n0 -> P n0
nat_rect_succ_r:
  forall {A : Type} (f : A -> A) (x : A) (n : nat),
  nat_rect (fun _ : nat => A) x (fun _ : nat => f)
    (Datatypes.S n) =
  nat_rect (fun _ : nat => A) (f x) (fun _ : nat => f)
    n
nat_double_ind:
  forall R : nat -> nat -> Prop,
  (forall n : nat, R 0 n) ->
  (forall n : nat, R (Datatypes.S n) 0) ->
  (forall n m : nat,
   R n m -> R (Datatypes.S n) (Datatypes.S m)) ->
  forall n m : nat, R n m
nat_rect_plus:
  forall (n m : nat) {A : Type} (f : A -> A) (x : A),
  nat_rect (fun _ : nat => A) x (fun _ : nat => f)
    (n + m) =
  nat_rect (fun _ : nat => A)
    (nat_rect (fun _ : nat => A) x (fun _ : nat => f)
       m) (fun _ : nat => f) n
dependent_choice:
  forall [X : Type] [R : X -> X -> Prop],
  (forall x : X, {y : X | R x y}) ->
  forall x0 : X,
  {f : nat -> X
  | f 0 = x0 /\
    (forall n : nat, R (f n) (f (Datatypes.S n)))}
Search (nat -> nat -> bool).
Nat.testbit: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
Search (nat -> nat -> nat).
Nat.lxor: nat -> nat -> nat
Nat.ldiff: nat -> nat -> nat
Nat.lor: nat -> nat -> nat
Nat.land: nat -> nat -> nat
Nat.gcd: nat -> nat -> nat
Nat.div: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
Nat.tail_add: nat -> nat -> nat
Nat.min: nat -> nat -> nat
Nat.pow: nat -> nat -> nat
Nat.tail_mul: nat -> nat -> nat
Nat.max: nat -> nat -> nat
Nat.sub: nat -> nat -> nat
Nat.mul: nat -> nat -> nat
Nat.add: nat -> nat -> nat
Nat.tail_addmul: nat -> nat -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
Nat.bitwise:
  (bool -> bool -> bool) -> nat -> nat -> nat -> nat

Now let's introduce some more proof tactics. Here, we use rewrite to use an equality in our hypotheses. Note that using rewrite <- would rewrite the equality in the other direction.

Theorem plus_same :
  forall n m:nat,
    n = m ->
    n + n = m + m.
forall n m : nat, n = m -> n + n = m + m
Proof.
forall n m : nat, n = m -> n + n = m + m
  intros n m.
n, m: nat
n = m -> n + n = m + m
  intros H.
n, m: nat
H: n = m
n + n = m + m
  rewrite H.
n, m: nat
H: n = m
m + m = m + m
  reflexivity.
Qed.

In this proof, we use the keyword as to name the new terms introduce by case analysis. In that case, we need to name the natural of which n is a successor of.

Theorem plus_1_neq_0 : forall n : nat,
  Nat.eqb (n + 1) 0 = false.
forall n : nat, Nat.eqb (n + 1) 0 = false
Proof.
forall n : nat, Nat.eqb (n + 1) 0 = false
  intros n.
n: nat
Nat.eqb (n + 1) 0 = false destruct n as [| n'] eqn:E.
n: nat
E: n = 0
Nat.eqb (0 + 1) 0 = false
n, n': nat
E: n = Datatypes.S n'
Nat.eqb (Datatypes.S n' + 1) 0 = false
  -
n: nat
E: n = 0
Nat.eqb (0 + 1) 0 = false simpl.
n: nat
E: n = 0
false = false reflexivity.
  -
n, n': nat
E: n = Datatypes.S n'
Nat.eqb (Datatypes.S n' + 1) 0 = false simpl.
n, n': nat
E: n = Datatypes.S n'
false = false reflexivity.
Qed.

Note that destruct typically forgets entirely about what we did case analysis on. We can remember that term and what it's equal to with the keyword eqn:.

Theorem andb_commutative : forall b c, andb b c = andb c b.
forall b c : bool, (b && c)%bool = (c && b)%bool
Proof.
forall b c : bool, (b && c)%bool = (c && b)%bool
  intros b c.
b, c: bool
(b && c)%bool = (c && b)%bool destruct b eqn:Eb.
b, c: bool
Eb: b = true
(true && c)%bool = (c && true)%bool
b, c: bool
Eb: b = false
(false && c)%bool = (c && false)%bool
  -
b, c: bool
Eb: b = true
(true && c)%bool = (c && true)%bool destruct c eqn:Ec.
b, c: bool
Eb: b = true
Ec: c = true
(true && true)%bool = (true && true)%bool
b, c: bool
Eb: b = true
Ec: c = false
(true && false)%bool = (false && true)%bool
    +
b, c: bool
Eb: b = true
Ec: c = true
(true && true)%bool = (true && true)%bool reflexivity.
    +
b, c: bool
Eb: b = true
Ec: c = false
(true && false)%bool = (false && true)%bool reflexivity.
  -
b, c: bool
Eb: b = false
(false && c)%bool = (c && false)%bool destruct c eqn:Ec.
b, c: bool
Eb: b = false
Ec: c = true
(false && true)%bool = (true && false)%bool
b, c: bool
Eb: b = false
Ec: c = false
(false && false)%bool = (false && false)%bool
    +
b, c: bool
Eb: b = false
Ec: c = true
(false && true)%bool = (true && false)%bool reflexivity.
    +
b, c: bool
Eb: b = false
Ec: c = false
(false && false)%bool = (false && false)%bool reflexivity.
Qed.

Propositions and Propositional Logic

We said that every term has a type, what is the type of the statements we've been proving?

Check (next_weekday wednesday = thursday).
next_weekday wednesday = thursday
     : Prop

Rocq has a special kind of type, named Prop to represent propositions, that we might try to prove. Note that not all propositions are true, they are just statements for which we may provide a proof. Propositions are a first-class entity in Rocq that can be defined, manipulated almost like any other type.

Definition false_prop: Prop :=
  3 = 2.

Theorem false_proof:
  3 = 2.
3 = 2
Proof.
3 = 2
  simpl.
3 = 2 reflexivity.
Unable to unify "2" with "3".
Abort.

Definition plus_claim : Prop := 2 + 2 = 4.
Check plus_claim.
plus_claim
     : Prop

We often define functions that create propositions. This defines properties of the arguments.

Definition is_three (n : nat) : Prop :=
  n = 3.
Check is_three.
is_three
     : nat -> Prop

Definition injective {A B:Type} (f : A ->  B) : Prop :=
  forall x y : A, f x = f y -> x = y.

Now that we have propositions, we can do propositional logic. Let's see how we manipulate conjunctions, disjunctions and implications.

Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.
3 + 4 = 7 /\ 2 * 2 = 4
Proof.
3 + 4 = 7 /\ 2 * 2 = 4
  split.
3 + 4 = 7
2 * 2 = 4
  -
3 + 4 = 7 reflexivity.
  -
2 * 2 = 4 reflexivity.
Qed.

Example or_example: 1 = 2 \/ 3 + 9 = 12.
1 = 2 \/ 3 + 9 = 12
Proof.
1 = 2 \/ 3 + 9 = 12
  right.
3 + 9 = 12
  reflexivity.
Qed.

Theorem and_elim_left:
  forall A B, A /\ B -> A.
forall A B : Prop, A /\ B -> A
Proof.
forall A B : Prop, A /\ B -> A
  intros A B H.
A, B: Prop
H: A /\ B
A
  destruct H as [HA HB].
A, B: Prop
HA: A
HB: B
A
  exact HA.
Qed.

Theorem or_commut:
  forall A B, A \/ B -> B \/ A.
forall A B : Prop, A \/ B -> B \/ A
Proof.
forall A B : Prop, A \/ B -> B \/ A
  intros A B H.
A, B: Prop
H: A \/ B
B \/ A
  destruct H as [HA | HB].
A, B: Prop
HA: A
B \/ A
A, B: Prop
HB: B
B \/ A
  -
A, B: Prop
HA: A
B \/ A right.
A, B: Prop
HA: A
A exact HA.
  -
A, B: Prop
HB: B
B \/ A left.
A, B: Prop
HB: B
B exact HB.
Qed.

We can also have equivalences, which is in practice a conjunction of two implications.

Theorem and_commut:
  forall A B, A /\ B <-> B /\ A.
forall A B : Prop, A /\ B <-> B /\ A
Proof.
forall A B : Prop, A /\ B <-> B /\ A
  intros A B.
A, B: Prop
A /\ B <-> B /\ A split.
A, B: Prop
A /\ B -> B /\ A
A, B: Prop
B /\ A -> A /\ B
  -
A, B: Prop
A /\ B -> B /\ A intros H.
A, B: Prop
H: A /\ B
B /\ A
    destruct H as [HA HB].
A, B: Prop
HA: A
HB: B
B /\ A
    split.
A, B: Prop
HA: A
HB: B
B
A, B: Prop
HA: A
HB: B
A
    +
A, B: Prop
HA: A
HB: B
B exact HB.
    +
A, B: Prop
HA: A
HB: B
A exact HA.
  -
A, B: Prop
B /\ A -> A /\ B intros H.
A, B: Prop
H: B /\ A
A /\ B
    destruct H as [HB HA].
A, B: Prop
HB: B
HA: A
A /\ B
    split.
A, B: Prop
HB: B
HA: A
A
A, B: Prop
HB: B
HA: A
B
    +
A, B: Prop
HB: B
HA: A
A exact HA.
    +
A, B: Prop
HB: B
HA: A
B exact HB.
Qed.

To use an implication, the tactic apply allows us to match the conclusion of an hypothesis with the goal, and replace the goal with the premise of that implication. Note that we could also have made progress in the hypotheses instead of the goal using apply ... in .... In fact, a lot of tactics can work on either the goal or the hypotheses. We can do both forward and backward reasoning, and often even meet in the middle.

Theorem modus_ponens:
  forall A B, (A -> B) -> A -> B.
forall A B : Type, (A -> B) -> A -> B
Proof.
forall A B : Type, (A -> B) -> A -> B
  intros A B Himpl HA.
A, B: Type
Himpl: A -> B
HA: A
B
  apply Himpl.
A, B: Type
Himpl: A -> B
HA: A
A
  (* apply Himpl in HA. *)
  apply HA.
Qed.

Finally, negation is defined as implying False. The False proposition is a proposition with no constructors, so we cannot construct a proof of it.

Print not.
not = fun A : Prop => A -> False
     : Prop -> Prop

Arguments not A%type_scope
Print True.
Inductive True : Prop :=  I : True.
Print False.
Inductive False : Prop :=  .

Lemma exfalso_quodlibet:
  forall P, False -> P.
forall P : Type, False -> P
Proof.
forall P : Type, False -> P
  intros P H.
P: Type
H: False
P
  contradiction.
Qed.

Lemma using_not:
  forall P, ~ P -> P -> False.
forall P : Prop, ~ P -> P -> False
Proof.
forall P : Prop, ~ P -> P -> False
  intros P Hnot HP.
P: Prop
Hnot: ~ P
HP: P
False
  unfold not in Hnot.
P: Prop
Hnot: P -> False
HP: P
False
  apply Hnot.
P: Prop
Hnot: P -> False
HP: P
P apply HP.
Qed.

Theorem zero_not_one : 0 <> 1.
0 <> 1
Proof.
0 <> 1
  unfold not.
0 = 1 -> False intros.
H: 0 = 1
False inversion H.
Qed.

Theorem double_neg:
  forall P, P -> ~~P.
forall P : Prop, P -> ~ ~ P
Proof.
forall P : Prop, P -> ~ ~ P
  unfold not.
forall P : Prop, P -> (P -> False) -> False intros.
P: Prop
H: P
H0: P -> False
False apply H0.
P: Prop
H: P
H0: P -> False
P apply H.
Qed.

Theorem contrapositive:
  forall P Q,
    (P -> Q) ->
    (~Q -> ~P).
forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P
Proof.
forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P
  unfold not.
forall P Q : Prop,
(P -> Q) -> (Q -> False) -> P -> False intros P Q H H0 H1.
P, Q: Prop
H: P -> Q
H0: Q -> False
H1: P
False apply H0.
P, Q: Prop
H: P -> Q
H0: Q -> False
H1: P
Q apply H.
P, Q: Prop
H: P -> Q
H0: Q -> False
H1: P
P apply H1.
Qed.

Finally, let's see how we can work with quantifiers, universal and existential. We've seen that intros is useful when our goal is a forall. When we have a forall as an hypothesis, we can use apply ... with to use it, or specialize it.

Theorem forall_elim:
  forall A (f:A -> A),
  (forall x, f x = f (f x)) ->
  forall y, f (f y) = f (f (f y)).
forall (A : Type) (f : A -> A),
(forall x : A, f x = f (f x)) ->
forall y : A, f (f y) = f (f (f y))
Proof.
forall (A : Type) (f : A -> A),
(forall x : A, f x = f (f x)) ->
forall y : A, f (f y) = f (f (f y))
  intros A f Hinvol y.
A: Type
f: A -> A
Hinvol: forall x : A, f x = f (f x)
y: A
f (f y) = f (f (f y))
  (* specialize (Hinvol (f y)). exact Hinvol.  *)
  apply Hinvol with (x:= f y).
Qed.

For existential quantifiers, we can use the exists tactic to provide a witness. And we can destruct an existential hypothesis to exhibit the witness.

Theorem exists_intro:
  forall (x: nat), exists y, y = x.
forall x : nat, exists y : nat, y = x
Proof.
forall x : nat, exists y : nat, y = x
  intros x.
x: nat
exists y : nat, y = x exists x.
x: nat
x = x reflexivity.
Qed.

Theorem exists_elim:
  (exists x, x + 2 = 5) ->
  exists y, 3 * (y + 2) = 15.
(exists x : nat, x + 2 = 5) ->
exists y : nat, 3 * (y + 2) = 15
Proof.
(exists x : nat, x + 2 = 5) ->
exists y : nat, 3 * (y + 2) = 15
  intros H.
H: exists x : nat, x + 2 = 5
exists y : nat, 3 * (y + 2) = 15 destruct H as [x Hx].
x: nat
Hx: x + 2 = 5
exists y : nat, 3 * (y + 2) = 15
  exists x.
x: nat
Hx: x + 2 = 5
3 * (x + 2) = 15 rewrite Hx.
x: nat
Hx: x + 2 = 5
3 * 5 = 15 reflexivity.
Qed.