Skip to content

Logic & Propositions

  • Coq is a typed language → logical claims also have type
  • All syntactically well-formed propositions have type Prop (propositions)
  • Propositions can be used in many ways: in Theorem, Lemma, Example; can also be Definition
  • Proposition can be parameterized → functions that return propositions are said to define properties of their arguments
  • Use Check to print type of expression/what theorem identifier refers to

Logical-AND

Operator: /\

Prove with split tactic → replaces the goal with two subgoals A and B. We can apply and_intro to achieve the same effect as split.

1
2
3
4
5
6
Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
split. (* or:  apply and_intro. *)
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 * 2 = 4 *) reflexivity.
Qed.

Use destruct tactic to use a conjunctive hypothesis to help prove something else. Can destruct H right when it is introduced.

1
2
3
4
5
6
7
8
Lemma destruct_example :
  forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof. intros n m H.
destruct H as [Hn Hm].  (* or: intros n m [Hn Hm]. *)
rewrite Hn.
rewrite Hm.
reflexivity.
Qed.

If only A or B is needed, use an underscore pattern _ to indicate that the unneeded conjunct should just be thrown away.

1
2
3
4
5
6
Lemma proj1 : forall P Q : Prop, P /\ Q -> P.
Proof.
 intros P Q HPQ.
 destruct HPQ as [HP _].
 apply HP.
Qed.

Logical-OR

Operator: \/

To show that disjunction holds, only need to prove one side → use left and/or right tactic.

1
2
3
4
Lemma or_intro : forall A B : Prop, A -> A \/ B.
Proof. intros A B HA.
left. apply HA.
Qed.

Sometimes need both

1
2
3
4
5
6
Lemma zero_or_succ :
   forall n : nat, n = 0 \/ n = S (pred n).
Proof. intros [|n'].
- left. reflexivity.
- right. reflexivity.
Qed.

To use a disjunctive hypothesis, use case analysis i.e. destruct tactic.

1
2
3
4
5
6
7
Lemma eq_mult_0 :
  forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof. intros n m [Hn | Hm].
- rewrite Hn. reflexivity.
- rewrite Hm. rewrite <- mult_n_O.
reflexivity.
Qed.

Negation & False

Operator: not

Use destruct to prove negations

1
2
3
4
Theorem not_true : forall (P:Prop), False -> P.
Proof. intros P contra.
destruct contra.
Qed.

Use notation to set alternative operator

1
Notation "~ x" := (not x) : type_scope.

To define notation for "not equals", use:

1
Notation "x != y" := (~(x = y)).

If you are trying to prove a goal that is nonsensical, apply ex_falso_quodlibet to change the goal to False. Coq provides a built-in tactic exfalso for applying it.

1
2
3
4
5
6
7
8
Theorem not_true_is_false : forall b : bool,
  not (b = true) -> b = false.
Proof. intros [] H. (* implicit destruct *)
- unfold not in H.
  exfalso.
  apply H. reflexivity.
- reflexivity.
Qed.

If and only if

Define as a conjunction of two implications:

1
Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P).

Notation

1
2
Notation \"P <-> Q\" := (iff P Q) 
(at level 95, no associativity): type_scope.

rewrite and reflexivity can be used with iff statements after importing this support library: From Coq Require Import Setoids.Setoid.

A "setoid" is a set equipped with an equivalence relation, that is, a relation that is reflexive, symmetric, and transitive. When two elements of a set are equivalent according to the relation, rewrite can be used to replace one element with the other.

iff is reflexive, symmetric, and transitive → in P <-> Q can replace P with Q or Q with P.

Existential Quantifiers

  • \(\forall\): forall
  • \(\exists\): exists
1
2
3
4
5
6
Theorem exists_example : forall n,
(exists m, n = 4 + m) ->
(exists o, n = 2 + o).
Proof. intros n [m Hm]. (* implicit destruct *)
exists (2 + m).
apply Hm. Qed.

Propositions & Proofs

Example: "x occurs in a list"

  • cannot occur in an empty list
  • otherwise: may or may not occur
1
2
3
4
5
Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] => False
| x' :: l' => x' = x \/ In x l'
end.

1
2
3
4
Example ex_1 : In 4 [1, 2, 3, 4, 5].
Proof.
  simpl. right. right. right. left. reflexivity.
Qed.

1
2
3
4
5
6
Example ex_2 :
  forall n, In n [2, 4] -> exists n', n = 2 * n'.
Proof. simpl. intros n [H | [H | []]].
- exists 1. rewrite <- H. reflexivity.
- exists 2. rewrite <- H. reflexivity.
Qed.

Inductive Propositions

Example:

  • Rule ev_0: The number 0 is even.
  • Rule ev_SS: If n is even, then S (S n) is even.

Proof tree showing application of these rules to say 4 is even:

1
2
3
4
5
6
-------- (ev_0)
  ev 0
-------- (ev_SS)
  ev 2
-------- (ev_SS)
  ev 4

Inductively definition in Coq:

1
2
3
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Note:

  • Inductive definition from nat to Prop
  • Explicit type in each constructor
  • In an inductive definition:
    • argument to the type constructor on the left of the colon is a "parameter"
    • argument on the right is an "index" or "annotation
    • For example:
      • in inductive list (X : Type) := ... → X is a parameter
      • in inductive ev : nat -> Prop := ... → nat is an index
1
2
3
4
5
6
7
Theorem ev_inversion : forall (n : nat), ev n ->
(n = 0) \/ (exists n', n = S (S n') /\ ev n').
Proof. intros n E.
destruct E as [ | n' E'] eqn:EE.
- left. reflexivity.
- right. exists n'. split. reflexivity. apply E'.
Qed.

Proof using the inversion:

1
2
3
4
5
6
7
8
Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof.
 intros n H. apply ev_inversion in H.
 destruct H as [H0|H1].
 - discriminate H0.
 - destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
 rewrite Heq. apply Hev.
 Qed.

Inductive Relations

  • Two argument propositions can be thought of as a relation → define a set of pairs for which the proposition is provable
  • Relations can be defined inductively

example: less than or equal

1
2
3
4
5
Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

Notation \"n <= m\" := (le n m).
  • apply constructors to prove <= goals
  • use tactics like inversion to extract information from <= hypotheses