「SF-LC」6 Logic - 黄玄的博客

We have seen…

propositions: factual claims
- equality propositions (e1 = e2)
- implications (P → Q)
- quantified propositions (∀ x, P)
proofs: ways of presenting evidence for the truth of a proposition

`Prop` type

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

Prop is first-class entity we can

name it
parametrized!

Definition is_three (n : nat) : Prop :=
  n = 3.

Check is_three. (* ===> nat -> Prop *)

Properties

In Coq, functions that return propositions are said to define properties of their arguments.

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)

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.

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.

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

and introduction

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.

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!)

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.

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 specific contradictory proposition defined in the standard library.

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

Prove the princple of explosion:

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

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.

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

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)

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

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.

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)

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)

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!.

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? See reflection below.

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!

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

Coq prints the statement of the plus_comm theorem in the same way that it prints the type of 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

proofs as 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

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 values to a type-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

(∀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 of functional 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

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.

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.)

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:

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

We wanna show there are interchangable.

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 reflects the truth of the proposition ∃ k, n = double k.

We can futhur general this to any equations representing as bool or Prop:

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.

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 a full regular expression matcher (so we can execute the regex).

Proof by Reflection!

(* 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 theorem uses 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

Prop type