We have seen…

*propositions*: factual claims- equality propositions (
`e1 = e2`

) - implications (
`P → Q`

) - quantified propositions (
`∀ x, P`

)

- equality propositions (
*proofs*: ways of presenting**evidence**for the truth of a proposition

`Prop`

type

1
2

Check 3 = 3. (* ===> Prop. A provable prop *)
Check 3 = 4. (* ===> Prop. A unprovable prop *)

`Prop`

is *first-class entity* we can

- name it
*parametrized*!

1
2
3
4

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

### Properties

In Coq,

functions that return propositionsare said to definepropertiesof their arguments.

1
2
3
4
5

Definition injective {A B} (f : A → B) :=
∀x y : A, f x = f y → x = y.
Lemma succ_inj : injective S. (* can be read off as "injectivity is a property of S" *)
Proof.
intros n m H. injection H as H1. apply H1. Qed.

The equality operator `=`

is also a function that returns a `Prop`

. (property: *equality*)

1

Check @eq. (* ===> forall A : Type, A -> A -> Prop *)

Theroems are types, and proofs are existentials.

## Slide Q&A - 1.

`Prop`

`Prop`

`Prop`

- Not typeable
`nat -> nat`

`nat -> Prop`

- (3)

think that Big Lambda (the type abstraction) works at type level, accepts type var, substitute and reture a type.
`forall`

in Coq is same (the concrete syntax) and only typecheck with `Type`

or its subtype `Set`

& `Prop`

.

1
2
3
4

Check (∀n:nat, S (pred n)). (* not typeable *)
Definition foo : (forall n:nat, bool) (* foo: nat -> bool *)
:= fun x => true.

## Logical Connectives

noticed that connectives symbols are “unicodize” in book and spacemacs.

### Conjuction (logical and)

`and`

is just binary `Prop -> Prop -> Prop`

and associative.

1
2
3

Print "/\".
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B
Check and. (* ===> and : Prop -> Prop -> Prop *)

#### and introduction

1
2
3
4
5
6

Lemma and_intro : forall A B : Prop, A -> B -> A /\ B.
Proof.
intros A B HA HB. split.
- apply HA.
- apply HB.
Qed.

To prove a conjunction,

- use the
`split`

tactic. It will generate two subgoals,- or use
`apply and_intro.`

, which match the conclusion and give its two premises as your subgoals.

#### and elimination

if we already have a proof of `and`

, `destruct`

can give us both.

1
2
3
4
5

Lemma and_example2' :
∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.
Proof.
intros n m [Hn Hm]. (* = intro H. destruct H. *)
rewrite Hn. rewrite Hm. reflexivity. Qed. (* you could use only one *)

Instead of packing into conjunction `∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.`

why not two separate premises? `∀n m : nat, n = 0 -> m = 0 → n + m = 0.`

Both are fine in this case but conjunction are useful as intermediate step etc.

Coq Intensive Q: why

`destruct`

can work on`and`

? is`and`

inductively defined? A: Yes.

### Disjunction (locial or)

#### or elimination

We need do case analysis (either `P`

or `Q`

should be able to prove the theroem separately!)

1
2
3
4
5
6
7
8

Lemma or_example :
forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
(* This pattern implicitly does case analysis on [n = 0 \/ m = 0] *)
intros n m [Hn | Hm]. (* = intro H. destruct H. *)
- (* Here, [n = 0] *) rewrite Hn. reflexivity.
- (* Here, [m = 0] *) rewrite Hm. rewrite <- mult_n_O. reflexivity.
Qed.

#### or introduction

When trying to establish (intro into conclusion) an `or`

, using `left`

or `right`

to pick one side to prove is sufficient.

1
2
3
4
5
6

Lemma or_intro : forall A B : Prop, A -> A \/ B.
Proof.
intros A B HA.
left. (* tactics *)
apply HA.
Qed.

### Falsehood and negation

#### False?

Recall the *princple of explosion*: it asserts that, if we assume a *contradiction*, then any other proposition can be derived.
we could define `¬ P`

(“not P”) as `∀ Q, P → Q.`

.

Coq actually makes a slightly different (but equivalent) choice, defining

`¬ P as P → False`

, where`False`

is a specificcontradictory propositiondefined in the standard library.

1
2

Definition not (P:Prop) := P → False.
Notation "¬x" := (not x) : type_scope.

Prove the *princple of explosion*:

1
2
3
4
5

Theorem ex_falso_quodlibet : forall (P:Prop),
False -> P.
Proof.
intros P contra.
destruct contra. Qed. (* 0 cases to prove since ⊥ is not provable. [inversion] also works *)

#### Inequality

1

Notation "x <> y" := (~(x = y)).

Same as SML and OCaml (for structural equality, OCaml uses `!=`

for physical equality.)

#### Proving of negation (or how to prove `¬P`

)

thinking about as `unfold not`

, i.e. `P -> False`

.
so you have an assumptions `P`

that could be `intros HP.`

and the residual goal would be simply `False`

.
which is usually proved by some kind of contradiction in hypotheses with tactics `discriminate.`

or `contradiction.`

1
2
3
4
5
6

Theorem contradiction_implies_anything : forall P Q : Prop,
(P /\ ~P) -> Q.
Proof.
intros P Q [HP HNA]. (* we could [contradiction.] to end the proof here`*)
unfold not in HNA. apply HNA in HP. (* HP : False, HNA : P -> False ⊢ HP: False *)
destruct HP. Qed. (* destruct False. *)

#### Tactic `exfalso.`

If you are trying to prove a goal that is nonsensical (e.g., the goal state is

`false = true`

), apply`ex_falso_quodlibet`

to change the goal to`False`

. This makes it easier to use assumptions of the form`¬P`

that may be available in the context — in particular, assumptions of the form`x≠y`

.

Since reasoning with

`ex_falso_quodlibet`

is quite common, Coq provides a built-in tactic,`exfalso`

, for applying it.

## Slide Q&A - 2

?

`unfold`

is implicit

- only
`destruct`

(if we consider`intros`

destruct is also`destruct`

.), ?`unfold`

- none (?
`unfold`

) `left.`

`destruct`

,`unfold`

,`left`

and`right`

`discrinminate`

(or`inversion`

)

### Truth

1
2

Lemma True_is_true : True.
Proof. apply I. Qed.

`I : True`

is a predefined Prop…

### Logical Equivalence

*if and only if* is just the conjunction of two implications. (so we need `split`

to get 2 subgoals)

1
2
3

Definition iff (P Q : Prop) := (P → Q) ∧ (Q → P).
Notation "P ↔ Q" := (iff P Q)
(at level 95, no associativity) : type_scope.

`rewrite`

and`reflexivity`

can be used with iff statements, not just equalities.

### Existential Quantification

To prove a statement of the form `∃x, P`

, we must show that `P`

holds for some specific choice of value for `x`

,
known as the **witness** of the existential.

So we explicitly tell Coq which witness `t`

we have in mind by invoking `exists t`

.
then all occurences of that “type variable” would be replaced.

#### Intro

1
2
3
4

Lemma four_is_even : exists n : nat, 4 = n + n.
Proof.
exists 2. reflexivity.
Qed.

#### Elim

Below is an interesting question…by intros and destruct we can have equation `n = 4 + m`

in hypotheses.

1
2
3
4
5
6
7

Theorem exists_example_2 : forall n,
(exists m, n = 4 + m) ->
(exists o, n = 2 + o).
Proof.
intros n [m Hm]. (* note implicit [destruct] here *)
exists (2 + m).
apply Hm. Qed.

## Programming with Propositions

Considering writing a common recursive `is_in`

for polymorphic lists.
(Though we dont have a polymorphic `=?`

(`eqb`

) defined yet)

1
2
3
4
5

Fixpoint is_in {A : Type} (x : A) (l : list A) : bool :=
match l with
| [] => false
| x' :: l' => if (x' =? x) then true else is_in x l'
end.

Similarly, we can write this function but with disjunction and return a `Prop`

!
*so we can write function to generate/create statements/propositions!* (thx for the idea Prop is first-class)

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.

The whole thing I understood as a *type operator* (function in type level) and it’s *recursive*!

Coq dare to do that becuz its *total*, which is guarded by its *termination checker*.
un-total PL, if having this, would make its type system *Turing Complete* (thus having *Halting Problem*).
(Recursive Type like ADT/GADT in ML/Haskell is a limited form of recursion allowing no arbitray recursion.)

### In_map

I took this one since it’s like a formal version of *Property-based Tests*!.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Lemma In_map :
forall (A B : Type) (f : A -> B) (l : list A) (x : A),
In x l ->
In (f x) (map f l).
Proof.
intros A B f l x.
induction l as [|x' l' IHl'].
- (* l = nil, contradiction *)
simpl. intros [].
- (* l = x' :: l' *)
simpl. intros [H | H]. (* evaluating [In] gives us 2 cases: *)
+ rewrite H. left. reflexivity. (* in head of l *)
+ right. apply IHl'. apply H. (* in tail of l*)
Qed.

Q & A:

`eq`

is just another inductively defined and doesn’t have any computational content. (satisfication)- Why use
`Prop`

instead of`bool`

? Seereflectionbelow.

### Drawbacks

In particular, it is subject to Coq’s usual restrictions regarding the definition of recursive functions, e.g., the requirement that they be “obviously terminating.”

In the next chapter, we will see how to define propositions

inductively, a different technique with its own set of strengths and limitations.

## Applying Theorems to Arguments.

`Check some_theorem`

print the statement!

1
2

Check plus_comm.
(* ===> forall n m : nat, n + m = m + n *)

Coq prints the

statementof the`plus_comm`

theorem in the same way that it prints thetypeof any term that we ask it to Check. Why?

Hmm…I just noticed that!!
But I should notice because **Propositions are Types! (and terms are proof)**

### Proof Object

proofsas first-class objects.

After `Qed.`

, Coq defined they as *Proof Object* and the *type of this obj* is the statement of the theorem.

Provable: some type is inhabited by some thing (having terms).

So I guess when we apply theorems, Coq implicitly use the type of the Proof Object. (it’s already type abstraction) …we will get to there later at ProofObject chapter.

### Apply theorem as function

`rewrite`

select variables greedily by default

1
2
3
4
5
6
7
8

Lemma plus_comm3_take3 :
∀x y z, x + (y + z) = (z + y) + x.
Proof.
intros x y z.
rewrite plus_comm.
rewrite (plus_comm y z). (* we can explicitly provide type var! *)
reflexivity.
Qed.

`x y z`

were some type var and *instantiated to values* by `intros`

, e.g. `x, y, z:nat`

but we can explicilty pass in to `plus_comm`

, which is a forall type abstraction! (`Δ n m. (eq (n + m) (m + n))`

)

there must be something there in Proof Object so we can apply

valuesto atype-level function

## Coq vs. Set Theory

Coq’s logical core, *the Calculus of Inductive Constructions*, is a *metalanguage for math*, but differs from other foundations of math e.g. ZFC Set Theory

### Functional Extensionality

1
2
3
4
5

(∀x, f x = g x) → f = g
∃f g, (∀x, f x = g x) → f = g
∃f g, (∀x, f x = g x) ∧ f != g (* negation, consistent but not interesting... *)

In common math practice, two functions

`f`

and`g`

are considered equal if they produce the same outputs. This is known as the principle offunctional extensionality.

Informally speaking, an “extensional property” is one that pertains to an object’s observable behavior. https://en.wikipedia.org/wiki/Extensionality https://en.wikipedia.org/wiki/Extensional_and_intensional_definitions?

This is not built-in Coq, but we can add them as Axioms. Why not add everything?

- One or multiple axioms combined might render
inconsistency.- Code extraction might be problematic

Fortunately, it is known that adding functional extensionality, in particular, is consistent. consistency: a consistent theory is one that does not contain a contradiction.

### Adding Axioms

1
2
3

Axiom functional_extensionality : forall {X Y: Type}
{f g : X -> Y},
(forall (x:X), f x = g x) -> f = g.

It’s like `Admitted.`

but alerts we’re not going to fill in later.

### Exercise - Proving Reverse with `app`

and with `cons`

are fn-exensionally equivalent.

1
2
3
4
5
6
7
8

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
match l1 with
| [] => l2
| x :: l1' => rev_append l1' (x :: l2)
end.
Definition tr_rev {X} (l : list X) : list X :=
rev_append l [].

BTW, this version is `tail recursive`

becuz the recursive call is the last operation needs to performed.
(In `rev`

i.e. `rev t ++ [h]`

, recursive call is a argument of function `++`

and we are CBV.)

1

Lemma tr_rev_correct : forall X, @tr_rev X = @rev X.

### Propositions and Booleans

We’ve seen two different ways of expressing logical claims in Coq:

- with booleans (of type
`bool`

), ; computational way- with propositions (of type
`Prop`

). ; logical way

There’re two ways to define 42 is even:

1
2

Example even_42_bool : evenb 42 = true.
Example even_42_prop : ∃k, 42 = double k.

We wanna show there are *interchangable*.

1
2

Theorem even_bool_prop : ∀n,
evenb n = true ↔ ∃k, n = double k.

In view of this theorem, we say that the boolean computation

`evenb n`

reflectsthe truth of the proposition`∃ k, n = double k`

.

We can futhur general this to any equations representing as `bool`

or `Prop`

:

1
2

Theorem eqb_eq : ∀n1 n2 : nat,
n1 =? n2 = true ↔ n1 = n2.

#### Notes on Computability.

However, even they are equivalent from a purely logical perspective, they may not be equivalent

`operationally`

.

1
2
3
4
5

Fail Definition is_even_prime n :=
if n = 2 then true
else false.
Error: The term "n = 2" has type "Prop" which is not a (co-)inductive type.

`=`

, or `eq`

, as any function in Coq, need to be computable and total. And we have no way to tell *whether any given proposition is true or false*. (…We can only naturally deduce things are inductively defined)

As a consequence, Prop in Coq does not have a universal case analysis operation telling whether any given proposition is true or false, since such an operation would allow us to write non-computable functions.

Although general non-computable properties cannot be phrased as boolean computations, it is worth noting that even many computable properties are easier to express using Prop than bool, since recursive function definitions are subject to significant restrictions in Coq.

E.g. Verifying Regular Expr in next chapter.

Doing the same with

`bool`

would amount to writing afull regular expression matcher(so we can execute the regex).

#### Proof by Reflection!

1
2
3
4
5
6
7
8
9
10
11

(* Logically *)
Example even_1000 : ∃k, 1000 = double k.
Proof. ∃500. reflexivity. Qed.
(* Computationally *)
Example even_1000' : evenb 1000 = true.
Proof. reflexivity. Qed.
(* Prove logical version by reflecting in computational version *)
Example even_1000'' : ∃k, 1000 = double k.
Proof. apply even_bool_prop. reflexivity. Qed.

As an extreme example, the Coq proof of the famous

4-color theoremuses reflection to reduce the analysis of hundreds of different cases to a boolean computation.

### Classical vs. Constructive Logic

…

## Future Schedule

Proof got messier! Lean on your past PLT experience

As discussion leader

- having many materials now
- selected troublesome and interesting ones