VVbuys Blog

Review (only in slide)

1
2

Theorem review2: ∀b, (orb true b) = true.
Theorem review3: ∀b, (orb b true) = true.

Whether or not it can be just simpl. depending on the definition of orb.

In Proof Engineering, we probably won’t need to include review2 but need to include review3 in library.

Why we have simpl. but not refl. ?

Proving 0 is a “neutral element” for + (additive identity)

Proving 0 + n = n

1
2
3

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity. Qed.

This can be simply proved by simplication bcuz the definition of + is defined by pattern matching against 1st operand:

1
2
3
4
5

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O ⇒ m
    | S n' ⇒ S (plus n' m)
  end.

We can observe that if n is 0(O), no matter m is, it returns m as is.

Proving n + 0 = n

1st try: Simplication

1
2
3
4
5

Theorem plus_O_n_1 : forall n : nat,  n + 0 = n.
Proof.
  intros n.
  simpl. (* Does nothing! *)
Abort.

This cannot be proved by simplication bcuz n is unknown so unfold the definition + won’t be able to simplify anything.

2nd try: Case Analysis

1
2
3
4
5
6
7
8
9

Theorem plus_n_O_2 : ∀n:nat,
  n = n + 0.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    reflexivity. (* so far so good... *)
  - (* n = S n' *)
    simpl. (* ...but here we are stuck again *)
Abort.

Our 2nd try is to use case analysis (destruct), but the proof stucks in inductive case since n can be infinitely large (destructed)

Induction to the resucue

To prove interesting facts about numbers, lists, and other inductively defined sets, we usually need a more powerful reasoning principle: induction.

Princeple of induction over natural numbers (i.e. mathematical induction)

1

P(0); ∀n' P(n') → P(S n')  ====>  P(n)

In Coq, like destruct, induction break P(n) into 2 subgoals:

1
2
3
4
5

Theorem plus_n_O : ∀n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Proving n - n = 0

1
2
3
4
5
6
7
8
9

Theorem minus_diag : ∀n,
  minus n n = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite → IHn'. reflexivity. Qed

Noticed that the definition of minus:

1
2
3
4
5
6

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O   , _    => O
  | S _ , O    => n
  | S n', S m' => minus n' m'
  end.

rewrite

rewrite would do a (DFS) preorder traversal in the syntax tree.

Pair of Numbers

Q: Why name inductive?
A: Inductive means building things bottom-up, it doesn’t have to self-referencial (recursive)
(see below induction on lists as well.)

1
2
3
4

Inductive natprod : Type :=
  | pair (n1 n2 : nat).

Notation "( x , y )" := (pair x y).

Proof on pair cannot simply simpl.

1
2
3
4
5

Theorem surjective_pairing_stuck : ∀(p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything! *)
Abort.

We have to expose the structure:

1
2
3
4

Theorem surjective_pairing : ∀(p : natprod),
  p = (fst p, snd p).
Proof.
  intros p. destruct p as [n m**. simpl. reflexivity. Qed.

It only generate one subgoal, becasue

That’s because natprods can only be constructed in one way.

My take on destruct

destruct

• destruct bool to true and false
• destruct nat to O and S n' (inductively defined)
• destruct pair to (n, m)

The prove by case analysis (exhaustive) is just an application of the idea of destruction!

the idea simply destruct the data type into its data constructors (representing ways of constructing this data)

• Java class has only 1 way to construct (via its constructor)
• Scala case class then have multiple way to construct

Lists of Numbers

Generalizing the definition of pairs

1
2
3

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

The ability of quosiquotation using Notation is awesome:

1
2
3

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

It’s exactly like OCaml, even for ;, at level 60 means it’s tightly than + at level 50 .

1

Notation "x ++ y" := (app x y) (right associativity, at level 60).

Instead of SML/OCaml’s @, Coq chooses Haskell’s ++.

hd with default

Coq function (for some reason) has to be total, so hd require a default value as 1st argument:

1
2
3
4
5

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil ⇒ default
  | h :: t ⇒ h
  end.

Induction on Lists.

The definition of inductive defined set

Each Inductive declaration defines a set of data values that can be built up using the declared constructors:

• a boolean can be either true or false;
• a number can be either O or S applied to another number;
• a list can be either nil or cons applied to a number and a list.

The reverse: reasoning inductive defined sets

Moreover, applications of the declared constructors to one another are the
only possible shapes that elements of an inductively defined set can have,
and this fact directly gives rise to a way of reasoning about inductively defined sets:

• a number is either O or else it is S applied to some smaller number;
• a list is either nil or else it is cons applied to some number and some smaller list;

Reasoning lists

if we have in mind some proposition P that mentions a list l and we want to argue that P holds for all lists,
we can reason as follows

1. First, show that P is true of l when l is nil.
2. Then show that P is true of l when l is cons n l' for some number n and some smaller list l', assuming that P is true for l'.

Search

1

Search rev  (* list all theorems of [rev] *)

Coq Conditionals (if then else)

1
2
3
4
5
6

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
  match l with
  | nil ⇒ None
  | a :: l' ⇒ if n =? O then Some a
                        else nth_error' l' (pred n)
  end.

One small generalization: since the boolean type in Coq is not built-in. Coq actually supports conditional expr over any inductive defined typewith two constructors. First constructor is considered true and false for second.

Stuck in Proof

could be many cases

• wrong tactics
• wrong theroem!! (might derive to counterexample)
• wrong step (most hard to figure out)
  • induction on wrong things

The critical new ideas are
polymorphism (abstracting functions over the types of the data they manipulate) and
higher-order functions (treating functions as data).

Polymorphism

Until today, We were living in the monomorphic world of Coq.
So if we want a list, we have to define it for each type:

1
2
3

Inductive boollist : Type :=
  | bool_nil
  | bool_cons (b : bool) (l : boollist).

Polymorphic Type and Constructors

But of course Coq supports polymorphic type.
So we can abstract things over type

1
2
3
4
5
6

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

Check list.
(* ===> list : Type -> Type *)

Recall from PLT course, this is exacly Parametric Polymorphism
and it’s SystemFω. the list here is a type-level small lambda, or type operators

Another things I’d love to mention is the concrete syntax of list X,
it didn’t choose the SML/OCaml order but the Haskell order.

Q1. What’s the type of nil and cons?

Both having forall type

1
2
3
4

Check nil.
(* ===> nil : forall X : Type, list X *)
Check cons.
(* ===> nil : forall X : Type, X -> list X -> list X *)

Q2. What’s the type of list nat? Why not Type but weird Set?

1
2
3
4
5
6
7
8

Check nat.
(* ===> nat : Set *)
Check list nat.
(* ===> list nat : Set *)
Check Set.
(* ===> Set: Type *)
Check Type.
(* ===> Type: Type *)

1

Check (cons nat 2 (cons nat 1 (nil nat))).

Polymorphic Functions

we can make polymorphic versions of list-processing function:

Btw, Pierce follows the TAPL convention where type is written in capital letter but not greek letter,
less clear in first look but better for typing in real programming.

1
2
3
4
5

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 ⇒ nil X
  | S count' ⇒ cons X x (repeat X x count')
  end.

This is SystemF.

1
2

Check repeat.
(* ===> repeat : forall X : Type, X -> nat -> list X *)

Slide QA

1. ill-typed
2. forall X : Type, X -> nat -> list X
3. list nat

Type Argument Inference

X must be a Type since nil expects an Type as its first argument.

1
2
3
4
5
6
7
8

Fixpoint repeat' X x count : list X :=     (* return type [:list X] can be omitted as well *)
  match count with
  | 0 ⇒ nil X
  | S count' ⇒ cons X x (repeat' X x count')
  end.

Check repeat'.
(* ===> forall X : Type, X -> nat -> list X *)

Type Argument Synthesis

We can write _ (hole) in place of X and Coq will try to unify all local information.

1
2
3
4
5
6
7
8

Fixpoint repeat'' X x count : list X :=
  match count with
  | 0 ⇒ nil _
  | S count' ⇒ cons _ x (repeat'' _ x count')
  end.

Definition list123' :=
  cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Same underlying mechanisms:

1
2

repeat' X x count : list X :=
repeat' (X : _) (x : _) (count : _) : list X :=

Implicit Arguments

Using Arguments directives to tell if an argument need to be implicit (i.e. omitted and always to infer) or not.

Implicitly convert to _ (synthesis) by frontend.

1
2
3

Arguments nil {X}.
Arguments cons {X} _ _.       (* data constructor usually don't specify the name *)
Arguments repeat {X} x count. (* fun definition usually do *)

The even more convenient syntax is that we can declare them right in our function definition.
Just surrounding them with curly braces.

1
2
3
4
5

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0 ⇒ nil
  | S count' ⇒ cons x (repeat''' x count')
  end.

Implicit Arguments Pitfalls on Inductive

1
2
3

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

Doing this will make X implicit for even list', the type constructor itself…

Other Polymorphic List functions

No difference but add implicit type argument {X : Type}.

Supplying Type Arguments Explicitly

1
2
3
4
5
6

Fail Definition mynil := nil.

Definition mynil : list nat := nil.

Check @nil. (* ===> @nil : forall X : Type, list X *)
Definition mynil' := @nil nat.

First thought: Existential
Second thought: A wait to be unified Universal. (after being implicit and require inference)

1
2
3
4
5

Check nil.

nil : 
   list ?X
where ?X : [ |- Type]

List notation

1
2
3
4
5
6

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

Same with before thanks to the implicit argument

Slide Q&A 2

1. we use ; not ,!!
2. list nat
3. ill-typed
4. ill-typed
5. list (list nat)
6. list (list nat) (tricky in first look)
7. list bool
8. ill-typed
9. ill-typed

Poly Pair

1
2
3
4
5
6

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).
Arguments pair {X} {Y} _ _.  (* omit two type var **)

Notation "( x , y )" := (pair x y).
Notation "X * Y" := (prod X Y) : type_scope.  (* only be used when parsing type, avoids clashing with multiplication *)

Be careful of (X,Y) and X*Y. Coq pick the ML way, not haskell way.

Combine or Zip

1
2
3
4
5
6
7

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match lx, ly with
  | [], _ ⇒ []
  | _, [] ⇒ []
  | x :: tx, y :: ty ⇒ (x, y) :: (combine tx ty)
  end.

Guess type?

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

Check @combine.
@combine
     : forall X Y : Type,
       list X -> list Y -> list (X * Y)

(* A special form of `forall`? *)
Check combine.
combine
     : list ?X -> list ?Y -> list (?X * ?Y)
where
?X : [ |- Type]
?Y : [ |- Type]

Poly Option

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

Inductive option (X:Type) : Type :=
  | Some (x : X)
  | None.

Arguments Some {X} _.
Arguments None {X}.


(* find nth element if exist, None otherwise *)
Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
  match l with
  | [] ⇒ None
  | a :: l' ⇒ if n =? O then Some a else nth_error l' (pred n)
  end.

Function as data

Functions as first-class citizens

Higher-Order Functions

1
2
3
4
5

Definition doit3times {X:Type} (f:X→X) (n:X) : X :=
  f (f (f n)).

Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)

Filter (taking a predicate on X)

collection-oriented programming style - my first time seeing this, any comments?

1
2
3
4
5
6
7
8
9
10

Fixpoint filter {X:Type} (test: X→bool) (l:list X)
                : (list X) :=
  match l with
  | [] ⇒ []
  | h :: t ⇒ if test h then h :: (filter test t)
                        else filter test t
  end.

Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.

Anonymous Functions

It is arguably a little sad, in the example just above, to be forced to define the function length_is_1 and give it a name just to be able to pass it as an argument to filter

1
2
3

Example test_anon_fun':
  doit3times (fun n ⇒ n * n) 2 = 256.
Proof. reflexivity. Qed.

Syntax: hybrid of OCaml fun n -> n and SML fn n => n.
and support multi-arguments (curried)

1

Compute ((fun x y => x + y) 3 5).

Map

Should be familar.

1
2
3
4
5

Fixpoint map {X Y: Type} (f:X→Y) (l:list X) : (list Y) :=
  match l with
  | [] ⇒ []
  | h :: t ⇒ (f h) :: (map f t)
  end.

1
2
3

Check @map

@map : forall X Y : Type, (X -> Y) -> list X -> list Y

Slide Q&A 3

1. as above

option map

1
2
3
4
5

Definition option_map {X Y : Type} (f : X → Y) (xo : option X) : option Y :=
  match xo with
    | None ⇒ None
    | Some x ⇒ Some (f x)
  end.

Functor Map (fmap) !

Fold (Reduce)

1
2
3
4
5

Fixpoint fold {X Y: Type} (f: X→Y→Y) (l: list X) (b: Y) : Y :=
  match l with
  | nil ⇒ b
  | h :: t ⇒ f h (fold f t b)
  end.

Fold Right (foldr). Argument order same with OCaml, different with Haskell.

1
2
3
4
5

Check @fold

@fold
     : forall X Y : Type,
       (X -> Y -> Y) -> list X -> Y -> Y

Slide Q&A 4

1. as above (type can be simply readed out)
2. list nat -> nat -> nat
3. 10

Functions That Construct Functions

Should be familar.
Use of closure.

1
2
3
4
5
6
7

definition constfun {X: Type} (x: X) : nat→X :=
  fun (k:nat) ⇒ x.

Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.

Example constfun_example2 : (constfun 5) 99 = 5.

Curried and partial application

1
2
3
4
5

Check plus.
(* ==> nat -> nat -> nat *)

Check plus 3.
(* ==> nat -> nat *)

Universe Inconsistency

I encounter this problem when doing church numeral exercise.

1

Definition plus (n m : cnat) : cnat := n cnat succ m.

will result in universe inconsistency error.

1
2
3
4
5
6
7

Set Printing Universes. (* giving more error msg *)

In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{Top.168+1}" while it is expected to have type "Type@{Top.168}"
(universe inconsistency: Cannot enforce Top.168 < Top.168 because Top.168 = Top.168).

What’s happening?

Yes, you can define: Definition plus (n m : cnat) : cnat := n cnat succ m. in System F. However, in Coq’s richer logic, you need to be a little more careful about allowing types to be instantiated at their own types, else you run into issue of inconsistency. Essentially, there is a stratification of types (by “universes”) that says that one universe cannot contain a “bigger” universe. Often, things are polymorphic in their universe (i.e., work in all universes), you run into this where you cannot instantiate the “forall X, …” that is the definition of cnat by cnat itself.
– Prof. Fluet

https://stackoverflow.com/questions/32153710/what-does-error-universe-inconsistency-mean-in-coq

Check Type => Type is a bit of a lie, everytime it the Type is not that same, but a bigger one.

Formally, every Type has an index associated to it, called its universe level.

1
2
3
4
5
6
7

Set Printing Universes. (* giving more error msg *)

Check Type. 
Type@{Top.1} : Type@{Top.1+1} (* {Top.1} |=  *)

Check Type. 
Type@{Top.2} : Type@{Top.2+1} (* {Top.2} |=  *)

Thus, the correct answer for that question is that Type_i has type Type_j, for any index j > i. This is needed to ensure the consistency of Coq’s theory: if there were only one Type, it would be possible to show a contradiction, similarly to how one gets a contradiction in set theory if you assume that there is a set of all sets.
Coq generates one new index variable every time you write Type, and keeps track of internal constraints

The error message you saw means that Coq’s constraint solver for universe levels says that there can’t be a solution to the constraint system you asked for.

The problem is that the forall in the definition of nat is quantified over Type_i, but Coq’s logic forces nat to be itself of type Type_j, with j > i. On the other hand, the application n nat requires that j <= i, resulting in a non-satisfiable set of index constraints.

From my understanding, the essences are:

1. reasons: Allowing self-application introduces logic contradiction (paradox).
2. understanding: The forall is quantified over types in the previous universe (the universe w/o itself).

From https://coq.inria.fr/refman/addendum/universe-polymorphism.html

1
2
3

Definition identity {A : Type} (a : A) := a.

Fail Definition selfid := identity (@identity).

1
2
3
4
5

The command has indeed failed with message:
The term "@identity" has type "forall A : Type, A -> A"
while it is expected to have type "?A"
(unable to find a well-typed instantiation for "?A": cannot ensure that
"Type@{Top.1+1}" is a subtype of "Type@{Top.1}").

The link also introduce some advanced/experimental way to do polymorphic universe

Polymorphic Church Numerals w/o self-applying itself

References: https://en.wikipedia.org/wiki/Church_encoding

Definition

Untyped doesn’t need to declare type…
STLC doesn’t have enough expressive power to represent church encoding
System F definition:

1

Definition cnat := forall X : Type, (X -> X) -> X -> X.

succ

1

succ = \n s z -> s (n s z) 

1
2

Definition succ (n : cnat) : cnat :=
  fun X s z => s (n X s z).

plus

1
2

plus = \m n -> m scc n
plus = \m n s z -> m s (n s z)

1
2
3

Definition plus (n m : cnat) : cnat :=
  n cnat succ m.                (* System F *)
  fun X s z => n X s (m X s z). (* Coq *)

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

plus = 
  lambda m:CNat.
  lambda n:CNat. ( 
    lambda X.
    lambda s:X->X.
    lambda z:X. 
      m [X] s (n [X] s z)
  ) as CNat;

plus = 
  lambda m:CNat.
  lambda n:CNat. 
    m [CNat] succ' n;

mult

1

mult = \m n -> m (plus n) n0 

1
2
3

Definition mult (n m : cnat) : cnat :=
  n cnat (plus m) zero.         (* SystemF *)
  fun X s z => (m X (n X s) z). (* Coq *)

1
2
3
4

mult = 
  lambda m:CNat.
  lambda n:CNat. 
    m [CNat] (plus n) c0;   /* partial app `plus` */

exp

1
2

pow = \m n -> m (mult n) n1
exp = \m n -> n m

1
2
3

Definition exp (n m : cnat) : cnat :=
  n cnat (mult m) one         (* SystemF *)
  fun X => m (X -> X) (n X).  (* Coq *)

apply

• exactly the same as some hypothesis
• can be used to finish a proof (shorter than rewrite then reflexivity)

It also works with conditional hypotheses:

1
2
3
4
5
6
7
8

n, m, o, p : nat
eq1 : n = m
eq2 : forall q r : nat, q = r -> [q; o] = [r; p]
============================
[n; o] = [m; p]

apply eq2.
n = m

It works by working backwards.
It will try to pattern match the universally quantified q r. (i.e. universal var)
We match the conclusion and generates the hypothesis as a subgoal.

1
2
3
4
5
6
7

Theorem trans_eq : forall (X:Type) (n m o : X), n = m -> m = o -> n = o.

Example trans_eq_example' : forall (a b c d e f : nat),
     [a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f].
Proof. 
  intros a b c d e f eq1 eq2.
  apply trans_eq. (* Error: Unable to find an instance for the variable m. *)

The unification algo won’t happy since:

• it can find instance for n = o from [a;b] = [e;f] (matching both conclusion)
• but what should be m? It could be anything as long as n = m and m = o holds.

So we need to tell Coq explicitly which value should be picked for m:

1

apply trans_eq with (m:=[c;d]).   (* <- supplying extra info, [m:=] can be ommited *)

Prof Mtf: As a PL person, you should feel this is a little bit awkward since now function argument name must be remembered. (but it’s just local and should be able to do any alpha-conversion).
named argument is more like a record.

In Coq Intensive 2 (2018), someone proposed the below which works:

1
2
3
4
5
6
7

Example trans_eq_example'' : forall (a b c d e f : nat),
  [a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f]. 
Proof.
  intros a b c d e f.
  apply trans_eq.          (* Coq was able to match three at all at this time...hmm *)
Qed.

injection and discrinimate

Side Note on Terminologys of Function

                     relation

function is defined as a special kind of binary relation.
it requires xRy1 ∧ xRy2 → y1 = y2 called “functional” or “univalent”, “right-unique”, or “deterministic”
and also ∀x ∈ X, ∃y ∈ Y s.t. xRy called “left-total”

                x       ↦      f(x)
              input     ↦     output
            argument    ↦     value

                X       ↦       Y
             domain 域  ↦  co-domain 陪域      
       what can go into ↦  what possibly come out

              A ⊆ X     ↦  f(A) = {f(x) | x ∈ A}
                        ↦     image
                        ↦  what actually come out

f⁻¹(B)={x ∈ X|f(x) ∈ B} ↦     B ⊆ Y
             preimage   ↦

            when A = X  ↦       Y
                        ↦     range  
                           image of domain

Besides subset, the notation of image and pre-image can be applied to element as well.
However, by definition:

• the image of an element x of domain ↦ always single element of codomain (singleton set)
• the preimage of an element y of codomain ↦ may be empty, or one, or many!
  • <= 1 ↦ 1 : injective (left-unique)
  • >= 1 ↦ 1 : surjective (right-total)
  • 1 ↦ 1 : bijective

Noted that the definition of “function” doesn’t require “right-total”ity) until we have surjective.

graph = [(x, f(x))], these points form a “curve”, 真的是图像

Total vs Partial

For math, we seldon use partial function since we can simply “define a perfect domain for that”.
But in Type Theory, Category Theory, we usually consider the domain X and the domain of definition X'.

Besides, f(x) can be undefined. (not “left-total”, might not have “right”)

Conclusion - the road from Relation to Function

            bi-relation 
                 | + right-unique 
          partial function
                 | + left-total   
          (total) function
 + left-unique /   \ + right-total
      injection     surjection
               \   /
             bijection

Original notes on Injective, surjective, Bijective

All talk about the propeties of preimage!

• Injective: <= 1 ↦ 1 or 0, 1 ↦ 1 (distinctness)
• Surjective: >= 1 ↦ 1 (at least 1 in the domain)
• Bijective: 1 ↦ 1 (intersection of Inj and Surj, so only 1 preimage, one-to-one correspondence)

injectivitiy and disjointness, or inversion.

Recall the definition of nat:

1
2
3

Inductive nat : Type :=
| O : nat
| S : nat → nat.

Besides there are two forms of nat (for destruct and induction), there are more facts:

1. The constructor S is injective (distinct), i.e S n = S m -> n = m.
2. The constructors O and S are disjoint, i.e. forall n, O != S n .

injection

• can be used to prove the preimages are the same.
• injection leave things in conclusion rather than hypo. with as would be in hypo.

disjoint

• principle of explosion (a logical principle)
  • asserts a contraditory hypothesis entails anything. (even false things)
  • vacously true
• false = true is contraditory because they are distinct constructors.

inversion

• the big hammer: inversion of the definition.
• combining injection and disjoint and even some more rewrite.
  • IMH, which one to use depends on semantics

from Coq Intensive (not sure why it’s not the case in book version).

1
2
3
4
5
6
7
8
9
10

Theorem S_injective_inv : forall (n m : nat),
  S n = S m -> n = m.
Proof.
  intros n m H. inversion H. reflexivity. Qed. 


Theorem inversion_ex1 : forall (n m : nat),
  [n] = [m] -> n = m.
Proof.
  intros n m H. inversion H. reflexivity. Qed.

Side question: could Coq derive equality function for inductive type?
A: nope. Equality for some inductive types are undecidable.

Converse of injectivity

1
2
3
4
5

Theorem f_equal : ∀(A B : Type) (f: A → B) (x y: A),
  x = y → f x = f y.
Proof. 
  intros A B f x y eq. 
  rewrite eq. reflexivity. Qed.

Slide Q&A 1

1. The tactic fails because tho negb is injective but injection only workks on constructors.

Using Tactics in Hypotheses

Reasoning Backwards and Reasoning Forward (from Coq Intensive 2)

Style of reasoning

• Backwards: start with goal, applying tactics simpl/destruct/induction, generate subgoals, until proved.
  • iteratively reasons about what would imply the goal, until premises or previously proven theorems are reached.
• Forwards: start with hypo, applying tactics, iteratively draws conclusions, until the goal is reached.

Backwards reasoning is dominated stratgy of theroem prover (and execution of prolog). But not natural in informal proof.

True forward reasoning derives fact, but in Coq it’s like hypo deriving hypo, very imperative.

in

most tactics also have a variant that performs a similar operation on a statement in the context.

1
2
3
4
5

simpl in H.
simpl in *. (* in all hypo and goal *)

symmetry in H.
apply L in H.

applying in hypothesis and in conclusion

applying in hypo is very different with applying in conclusion.

it’s not we unify the ultimate conclusion and generate premises as new goal, but trying to find a hypothesis to match and left the residual conclusion as new hypothesis.

1
2
3
4
5
6
7
8

Theorem silly3'' : forall (n : nat),
  (true = (n =? 5) -> true = ((S (S n)) =? 7)) ->
  true = (n =? 5)  ->
  true = ((S (S n)) =? 7).
Proof.
  intros n eq H.
  apply eq in H.  (* or *)  apply eq. (* would be different *)
  apply H.  Qed.

Also if we add one more premises true = true ->,
the subgoal generated by apply would be in reversed order:

1
2
3
4
5

Theorem silly3'' : forall (n : nat),
  (true = true -> true = (n =? 5) -> true = ((S (S n)) =? 7)) ->
  true = (n =? 5)  ->
  true = ((S (S n)) =? 7).
Proof.

Again: “proof engineering”: proof can be done in so many different ways and in different orders.

Varying the Induction Hypothesis

Sometimes it’s important to control the exact form of the induction hypothesis!!

Considering:

1
2

Theorem double_injective: ∀n m,
        double n = double m → n = m.

if we begin with intros n m. induction n.
then we get stuck in the inductive case of n, where the induction hypothesis IHn' generated is:

1
2

IHn' : double n' = double m -> n' = m
IHn' : double n' = double (S m') -> n' = S m'  (* m = S m' *)

This is not what we want!!

To prove double_injective, we hope IHn' can give us double n' = double m' -> n' = m' (i.e. the P(n-1) case).

The problem is intros implies for these particular n and m. (not more forall but const). And when we intros n m. induction n, we are trying to prove a statement involving every n but just a single m…

How to keep m generic (universal)?

By either induction n before intros m or using generalize dependent m, we can have:

1

IHn' : forall m : nat, double n' = double m -> n' = m

where the m here is still universally quantified, so we can instaniate m with m' by applying it with double n' = double m' to yield n' = m' or vice versa. (recall conditional statements can be applyed in 2 ways.)

Notes on generalize dependent

Usually used when the argument order is conflict with instantiate (intros) order.

? reflection: turing a computational result into a propositional result

Unfolding Definitions.

tactics like simpl, reflexivity, and apply will often unfold the definitions of functions automatically.
However, this automatic unfolding is somewhat conservative.

simpl. only do unfolding when it can furthur simplify after unfolding. But sometimes you might want to explicitly unfold then do furthur works on that.

Using destruct on Compound Expressions

destruct the whole arbitrary expression.

destruct by default throw away the whole expression after it, which might leave you into a stuck state.
So explicitly saying eqn:Name would help with that!

Micro Sermon - Mindless proof-hacking

From Coq Intensive…

• a lot of fun
• …w/o thinking at all
• terrible temptation
• you shouldn’t always resist…

But after 5 mins…you should step back and try to think

A typical coq user

• sitting and does not have their brain engaged all the time…
• at some point…(get stuck)
  • oh I have to reengage brain..

what is this really saying…

One way: good old paper and pencil

5 mins is good time!

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

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 propositions are said to define properties of 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.

1. Prop
2. Prop
3. Prop
4. Not typeable
5. nat -> nat
6. nat -> Prop
7. (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 specific contradictory proposition defined 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

1. only destruct (if we consider intros destruct is also destruct.), ?unfold
2. none (?unfold)
3. left.
4. destruct, unfold, left and right
5. 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:

1. eq is just another inductively defined and doesn’t have any computational content. (satisfication)
2. 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!

1
2

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

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

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 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?

1. One or multiple axioms combined might render inconsistency.
2. 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:

1. with booleans (of type bool), ; computational way
2. 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 reflects the 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 a full 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 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

Inductively Defined Propositions

The 3rd way to state Evenness…

Besides:

1
2
3

Theorem even_bool_prop : ∀n,
  evenb n = true ↔ ∃k, n = double k.
 (*bool*)                 (*prop*)

we can write an Inductive definition of the even property!

Inference rules

In CS, we often uses inference rules

                    ev n
---- ev_0       ------------ ev_SS
ev 0            ev (S (S n))

and proof tree (i.e. evidence), there could be multiple premieses to make it more tree-ish.

---- ev_0
ev 0
---- ev_SS
ev 2
---- ev_SS
ev 4

So we can literally translate them into a GADT:

Inductive Definition of Evenness

1
2
3
4
5
6

Inductive even : nat → Prop :=
  | ev_0  : even 0
  | ev_SS : ∀n, even n → even (S (S n)). 

Check even_SS.
(* ==> : forall n : nat, even n -> even (S (S n)) *)

There are two ways to understand the even here:

1. A Property of nat and two theorems (Intuitively)

the thing we are defining is not a Type, but rather a function nat -> Prop — i.e., a property of numbers.

we have two ways to provide an evidence to show the nat is even, either or:

1. it’s 0, we can immediately conclude it’s even.
2. for any n, if we can provide a evidence that n is even, then S (S n) is even as well.

We can think of the definition of even as defining a Coq property even : nat → Prop, together with primitive theorems ev_0 : even 0 and ev_SS : ∀ n, even n → even (S (S n)).

2. An “Indexed” GADT and two constructors (Technically)

In an Inductive definition, an argument to the type constructor on the left of the colon is called a “parameter”, whereas an argument on the right is called an “index”. – “Software Foundaton”

Considered a “parametrized” ADT such as the polymorphic list,

1
2
3
4
5

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

Check list. (* ===> list : Type -> Type *)

where we defined type con list : Type -> Type, by having a type var X in the left of the :.
the X is called a parameter and would be parametrized i.e. substituted, globally, in constructors.

Here, we write nat in the right of the : w/o giving it a name (to refer and to substitute),
which allows the nat taking different values in different constructors (as constraints).
it’s called an index and will form a family of type indexed by nat (to type check?)

From this perspective, there is an alternative way to write this GADT:

1
2
3

Inductive even : nat → Prop :=
| ev_0                         : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

we have two ways to construct the even type (Prop <: Type), either or:

1. ev_0 takes no argument, so simply instantiate even with nat 0
2. ev_SS takes a nat n and a H typed even n,

• the dependency between two arguments thus established!
• as long as the constraint on same n is fullfilled, we can build type even with S (S n)

The take way is that dependent type (Pi-type) allow us to constriant constructors with different values.

indexed way is more general. it formed a larger type, and is only used when extra power needed.
every parametrized one can be represented as indexed one (it’s just that index happended to be the same)

“Constructor Theorems”

Such “constructor theorems” have the same status as proven theorems. In particular, we can use Coq’s apply tactic with the rule names to prove even for particular numbers…

1
2

Theorem ev_4 : even 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Proof States Transition:

even 4
------ apply ev_SS.
even 2
------ apply ev_SS.
even 0
------ apply ev_0.
       Qed.

I believed what apply do is trying to backward reasoning, i.e. matching the goal and leave the “evidence” need to be proved (to conclude the goal).

we can write it as normal function application syntax w/o using tactics like other Dependent-typed PL as well

1
2

Theorem ev_4' : even 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

Using Evidence in Proofs

Besides constructing evidence that numbers are even, we can also reason about such evidence.

Introducing even with an Inductive declaration tells Coq that these two constructors are the only ways to build evidence that numbers are even.

In other words, if someone gives us evidence E for the assertion even n, then we know that E must have one of two shapes

This suggests that it should be possible to analyze a hypothesis of the form even n much as we do inductively defined data structures; in particular, it should be possible to argue by induction and case analysis on such evidence.

This starts to get familiar as what we did for many calculi, ranging from Logics to PLT.
This is called the Inversion property.

Inversion on Evidence

We can prove the inersion property by ourselves:

1
2
3
4
5
6
7
8
9

Theorem ev_inversion :
  ∀(n : nat), even n →
    (n = 0) ∨ (∃n', n = S (S n') ∧ even n').
Proof.
  intros n E.
  destruct E as [ | n' E'].
  - (* E = ev_0 : even 0 *)                  left. reflexivity.
  - (* E = ev_SS n', E' : even (S (S n')) *) right. ∃n'. split. reflexivity. apply E'.
Qed.

But Coq provide the inversion tactics that does more! (not always good tho, too automagical)

The inversion tactic does quite a bit of work. When applied to equalities, as a special case, it does the work of both discriminate and injection. In addition, it carries out the intros and rewrites

Here’s how inversion works in general. Suppose the name H refers to an assumption P in the current context, where P has been defined by an Inductive declaration. Then, for each of the constructors of P, inversion H generates a subgoal in which H has been replaced by the exact, specific conditions under which this constructor could have been used to prove P.
Some of these subgoals will be self-contradictory; inversion throws these away. The ones that are left represent the cases that must be proved to establish the original goal. For those, inversion adds all equations into the proof context that must hold of the arguments given to P (e.g., S (S n') = n in the proof of evSS_ev).
(9-proof-object.md has a better explaination on inversion)

inversion is a specific use upon destruct (both do case analysis on constructors), but many property need induction!.
By induction (even n), we have cases and subgoals splitted, and induction hypothesis as well.

Induction on Evidence

Similar to induction on inductively defined data such as list:

To prove a property of (for any X) list X holds, we can use induction on list X.
To prove a property of n holds for all numbers for which even n holds, we can use induction on even n.

Notes on induction

The principle of induction is to prove P(n-1) -> P(n) (多米诺) for some (well-founded partial order) set of n.

Here, we are induction over “the set of numbers fullfilling the property even“.
Noticed that we r proving things over this set, meaning we already have it (i.e. a proof, or a evidence) in premises, instead of proving the evenness of the set.

Proof by Mathematical Induction is Deductive Reasoning

“Proof by induction,” despite the name, is deductive. The reason is that proof by induction does not simply involve “going from many specific cases to the general case.” Instead, in order for proof by induction to work, we need a deductive proof that each specific case implies the next specific case. Mathematical induction is not philosophical induction.
https://math.stackexchange.com/a/1960895/528269

Mathematical induction is an inference rule used in formal proofs. Proofs by mathematical induction are, in fact, examples of deductive reasoning.
Equivalence with the well-ordering principle: The principle of mathematical induction is usually stated as an axiom of the natural numbers; see Peano axioms. However, it can be proved from the well-ordering principle. Indeed, suppose the following:
https://en.wikipedia.org/wiki/Mathematical_induction

Also, Structual Induction is one kind of Math. Induction

和标准的数学归纳法等价于良序原理一样，结构归纳法也等价于良序原理。

…A well-founded partial order is defined on the structures…
…Formally speaking, this then satisfies the premises of an axiom of well-founded induction…
https://en.wikipedia.org/wiki/Structural_induction

In terms of Well-ordering and Well-founded:

If the set of all structures of a certain kind admits a well-founded partial order,
then every nonempty subset must have a minimal element. (This is the definition of “well-founded”.)
如果某种整个结构的集容纳一个良基偏序， 那么每个非空子集一定都含有最小元素。（其实这也是良基的定义

Inductive Relations

Just as a single-argument proposition defines a property, 性质
a two-argument proposition defines a relation. 关系

1
2
3
4
5

Inductive le : nat → nat → Prop :=
  | le_n n                : le n n
  | le_S n m (H : le n m) : le n (S m).

Notation "n ≤ m" := (le n m).

It says that there are two ways to give evidence that one number is less than or equal to another:

1. either same number
2. or give evidence that n ≤ m then we can have n ≤ m + 1.

and we can use the same tactics as we did for properties.

Slide Q&A - 1

1. First destruct even n into 2 cases, then discriminate on each.

Another way…
rewriting n=1 on even n. It won’t compute Prop, but destruct can do some discriminate behind the scene.

Slide Q&A - 2

inversion and rewrite plus_comm (for n+2)

destruct vs. inversion vs. induction.

destruct, inversion, induction (on general thing)… similar/specialized version of each…

Trying to internalize this concept better: When to use which?

For any inductively defined proposition (<: Type) in hypothesis:
meaning from type perspective, it’s already a “proper type” (::*)

1

Inductive P = C1 : P1 | C2 : A2 -> P2 | ...

1. destruct case analysis on inductive type

• simply give you each cases, i.e. each constructors.
• we can destruct on a =? b since =? is inductively defined.

2. induction use induction principle

• proving P holds for all base cases
• proving P(n) holds w/ P(n-1) for all inductive cases
  (destruct stucks in this case because of no induction hypothesis gained from induction principle)

3. inversion invert the conclusion and give you all cases with premises of that case.

For GADT, i.e. “indexed” Prop (property/relation), P could have many shape
inversion give you Ax for shape P assuming built with Cx

inversion discards cases when shape P != Px.
(destruct stucks in this case because of no equation gained from inversion lemma)

Case Study: Regular Expressions

Definition

Definition of RegExp in formal language can be found in FCT/CC materials

1
2
3
4
5
6
7

Inductive reg_exp {T : Type} : Type :=
  | EmptySet                 (* ∅ *)
  | EmptyStr                 (* ε *)
  | Char (t : T)
  | App (r1 r2 : reg_exp)    (* r1r2 *)
  | Union (r1 r2 : reg_exp)  (* r1 | r2 *)
  | Star (r : reg_exp).      (* r*  *)

Note that this definition is polymorphic.
We depart slightly in that we do not require the type T to be finite. (difference not significant here)

reg_exp T describe strings with characters drawn from T — that is, lists of elements of T.

Matching

The matching is somewhat similar to Parser Combinator in Haskell…

e.g.
EmptyStr matches []
Char x matches [x]

we definied it into an Inductive relation (can be displayed as inference-rule).
somewhat type-level computing !

1
2
3
4
5
6
7
8
9
10

Inductive exp_match {T} : list T → reg_exp → Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar x : exp_match [x] (Char x)
| MApp s1 re1 s2 re2
            (H1 : exp_match s1 re1)
            (H2 : exp_match s2 re2) :
            exp_match (s1 ++ s2) (App re1 re2)
(** etc. **)

Notation "s =~ re" := (exp_match s re) (at level 80).  (* the Perl notation! *)

Slide Q&A - 3

The lack of rule for EmptySet (“negative rule”) give us what we want as PLT

Union and Star.

the informal rules for Union and Star correspond to two constructors each.

1
2
3
4
5
6
7
8
9
10
11

| MUnionL s1 re1 re2
              (H1 : exp_match s1 re1) :
              exp_match s1 (Union re1 re2)
| MUnionR re1 s2 re2
              (H2 : exp_match s2 re2) :
              exp_match s2 (Union re1 re2)
| MStar0 re : exp_match [] (Star re)
| MStarApp s1 s2 re
              (H1 : exp_match s1 re)
              (H2 : exp_match s2 (Star re)) :
              exp_match (s1 ++ s2) (Star re).

Thinking about their NFA: they both have non-deterministic branches!
The recursive occurrences of exp_match gives as direct argument (evidence) about which branches we goes.

we need some sanity check since Coq simply trust what we declared…
that’s why there is even Quick Check for Coq.

Direct Proof

In fact, MApp is also non-deterministic about how does re1 and re2 collaborate…
So we have to be explicit:

1
2
3
4

Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
  apply (MApp [1] _ [2]).
  ...

Inversion on Evidence

This, if we want to prove via destruct,
we have to write our own inversion lemma (like ev_inversion for even).
Otherwise we have no equation (which we should have) to say contradiction.

1
2
3
4

Example reg_exp_ex3 : ~ ([1; 2] =~ Char 1).
Proof.
  intros H. inversion H.
Qed.

Manual Manipulation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Lemma MStar1 :
  forall T s (re : @reg_exp T) ,
    s =~ re ->
    s =~ Star re.
Proof.
  intros T s re H.
  rewrite <- (app_nil_r _ s).  (* extra "massaging" to convert [s] => [s ++ []] *)
  apply (MStarApp s [] re).    (* to the shape [MStarApp] expected thus can pattern match on *)

      (* proving [MStarApp] requires [s1 s2 re H1 H2]. By giving [s [] re], we left two evidence *)
      | MStarApp s1 s2 re
          (H1 : exp_match s1 re)
          (H2 : exp_match s2 (Star re)) :
          exp_match (s1 ++ s2) (Star re).

  - apply H.                   (* evidence H1 *)
  - apply MStar0.              (* evidence H2 *)
Qed.                           (* the fun fact is that we can really think the _proof_
                                  as providing evidence by _partial application_. *)

Induction on Evidence

By the recursive nature of exp_match, proofs will often require induction.

1
2
3
4
5
6
7
8
9
10

(** Recursively collecting all characters that occur in a regex **)
Fixpoint re_chars {T} (re : reg_exp) : list T :=
  match re with
  | EmptySet ⇒ []
  | EmptyStr ⇒ []
  | Char x ⇒ [x]
  | App re1 re2 ⇒ re_chars re1 ++ re_chars re2
  | Union re1 re2 ⇒ re_chars re1 ++ re_chars re2
  | Star re ⇒ re_chars re
  end.

The proof of in_re_match went through by inversion on relation s =~ re. (which gives us all 7 cases.)
The interesting case is MStarApp, where the proof tree has two branches (of premises):

                  s1 =~ re    s2 =~ Star re
                 ---------------------------            (MStarApp)
                    s1 ++ s2 =~ Star re

So by induction on the relation (rule), we got two induction hypotheses!
That’s what we need for the proof.

The remember tactic (Induction on Evidence of A Specific Case)

One interesting/confusing features is that induction over a term that’s insuffciently general. e.g.

1
2
3
4
5
6

Lemma star_app: ∀T (s1 s2 : list T) (re : @reg_exp T),
  s1 =~ Star re →
  s2 =~ Star re →
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.

Here, we know the fact that both s1 and s2 are matching with the form Star re.
But by induction. it will give us all 7 cases to prove, but 5 of them are contradictory!

That’s where we need remember (Star re) as re' to get this bit of information back to discriminate.

Sidenotes: inversion vs. induction on evidence

We might attemp to use inversion,
which is best suitted for have a specific conclusion of some rule and inverts back to get its premises.

But for recursive cases (e.g. Star), we always need induction.

induction on a specific conclusion then remember + contradiction is similar with how inversion solves contradictionary cases. (They both destruct the inductively defined things for sure)

Exercise: 5 stars, advanced (pumping)

FCT/Wikipedia “proves” pumping lemma for regex in a non-constructive way.

Here we attempts to give a constructive proof.

Case Study: Improving Reflection (互映)

we often need to relate boolean computations to statements in Prop

1
2
3

Inductive reflect (P : Prop) : bool → Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ¬P) : reflect P false.

The only way to construct ReflectT/F is by showing (a proof) of P/¬P,
meaning invertion on reflect P bool can give us back the evidence.

iff_reflect give us eqbP.

1
2
3
4

Lemma eqbP : ∀n m, reflect (n = m) (n =? m).
Proof.
  intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

This gives us a small gain in convenience: we immediately give the Prop from bool, no need to rewrite.

Proof Engineering Hacks…

SSReflect - small-scale reflection

a Coq library
used to prove 4-color theorem…!
simplify small proof steps with boolean computations. (somewhat automation with decision procedures)

Extended Exercise: A Verified Regular-Expression Matcher

we have defined a match relation that can prove a regex matches a string.
but it does not give us a program that can run to determine a match automatically…

we hope to translate inductive rules (for constructing evidence) to recursive fn.
however, since reg_exp is recursive, Coq won’t accept it always terminates

theoritically, the regex = DFA so it is decidable and halt.
technically, it only halts on finite strings but not infinite strings.
(and infinite strings are probably beyond the scope of halting problem?)

Heavily-optimized regex matcher = translating into state machine e.g. NFA/DFA.
Here we took a derivative approach which operates purely on string.

1
2

Require Export Coq.Strings.Ascii.
Definition string := list ascii.

Coq 标准库中的 ASCII 字符串也是归纳定义的，不过我们这里为了之前定义的 match relation 用 list ascii.

to define regex matcher over list X i.e. polymorphic lists.
we need to be able to test equality for each X etc.

Rules & Derivatives.

Check paper Regular-expression derivatives reexamined - JFP 09 as well.

app and star are the hardest ones.

Let’s take app as an example

1. 等价 helper

1
2

Lemma app_exists : ∀(s : string) re0 re1,
    s =~ App re0 re1 ↔ ∃s0 s1, s = s0 ++ s1 ∧ s0 =~ re0 ∧ s1 =~ re1.

this helper rules is written for the sake of convenience:

• the <- is the definition of MApp.
• the -> is the inversion s =~ App re0 re1.

2. App 对于 a :: s 的匹配性质

1
2
3
4

Lemma app_ne : ∀(a : ascii) s re0 re1,
    a :: s =~ (App re0 re1) ↔
    ([ ] =~ re0 ∧ a :: s =~ re1) ∨
    ∃s0 s1, s = s0 ++ s1 ∧ a :: s0 =~ re0 ∧ s1 =~ re1.

the second rule is more interesting. It states the property of app:

App re0 re1 匹配 a::s 当且仅当 (re0 匹配空字符串 且 a::s 匹配 re1) 或 (s=s0++s1，其中 a::s0 匹配 re0 且 s1 匹配 re1)。

这两条对后来的证明很有帮助，app_exists 反演出来的 existential 刚好用在 app_ne 中.

https://github.com/jiangsy/SoftwareFoundation/blob/47543ce8b004cd25d0e1769f7444d57f0e26594d/IndProp.v

3. 定义 derivative 关系

the relation re' is a derivative of re on a is defind as follows:

1
2

Definition is_der re (a : ascii) re' :=
  ∀s, a :: s =~ re ↔ s =~ re'.

4. 实现 derive

Now we can impl derive by follwing 2, the property.
In paper we have:

∂ₐ(r · s) = ∂ₐr · s + ν(r) · ∂ₐs       -- subscriprt "a" meaning "respective to a" 

where 
  ν(r) = nullable(r) ? ε : ∅ 

In our Coq implementation, nullable(r) == match_eps(r),

Since we know that
∀r, ∅ · r = ∅,
∀r, ε · r = r,
we can be more straightforward by expanding out v(r):

1
2
3
4
5

Fixpoint derive (a : ascii) (re : @reg_exp ascii) : @reg_exp ascii :=
...
 | App r1 r2 => if match_eps r1                            (** nullable(r) ? **)
      then Union (App (derive a r1) r2) (derive a r2)      (**  ∂ₐr · s + ∂ₐs **)
      else App (derive a r1) r2                            (**  ∂ₐr · s       **)

useful as env

Map == Dictionary

• building data structure.
• use of reflection to streamline proofs.

Two flavors of maps:

1. total maps, return default when lookup fails
2. partial maps, return option to indicate success/failure, using None as the default.

The Coq Standard Lib

From now on, importing from std lib. (but should not notice much difference)

1
2
3
4
5
6

From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.

TODO: what’s the differences above?
Answered in Coq Intensive:

• Require give access but need to use qualified name
• Import no need to use qualified name
• Export module importing me no need to use qualified name as well

String in Coq is list of Char and Char is record of 8 Bool…

Identifiers

we need a type for the keys that we use to index into our maps.

In Lists.v (Partial Maps):

1
2

Inductive id : Type := 
  | Id (n : nat).

From now on we will use the string from Coq’s std lib:

1
2
3
4
5

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

Check string_dec: (* ===> *)
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

The equality check fn for string from stdlib is string_des, which returns a sumbool type, i.e. {x=y} + {x≠y}.

which can be thought of as an “evidence-carrying boolean”.
Formally, an element of sumbool is either or

• a proof that two things are equal
• a proof that they are unequal,
  together with a tag indicating which.

Some properties:

1
2
3
4
5
6

(* reflexive relation *)
Theorem eqb_string_refl : ∀s : string, true = eqb_string s s.

(* functional extensionality *)
Theorem eqb_string_true_iff : ∀x y : string, eqb_string x y = true ↔ x = y.
Theorem eqb_string_false_iff : ∀x y : string, eqb_string x y = false ↔ x ≠ y.

Total Maps

use functions, rather than lists of key-value pairs, to build maps.
The advantage of this representation is that it offers a more extensional view of maps. 外延性

(where two maps that respond to queries in the same way will be represented as literally the same thing rather than just “equivalent” data structures. This, in turn, simplifies proofs that use maps.)

1
2
3
4
5
6
7
8
9
10

Definition total_map (A : Type) := string -> A.

(* empty take a default value *)
Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

(* update take a key value pair *)
Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) (* : total_map A *) :=
  fun x' => if eqb_string x x' then v else m x'.

Where is the data stored? Closure!

My Reviews on API style of ML

1
2
3

Definition examplemap :=
  t_update (t_update (t_empty false) "foo" true)
           "bar" true.

since t_update is defined as so called “t-first” style.
Reason/BuckleScript and OCaml stdlib uses this style as well:

1
2
3
4

let examplemap = 
  t_empty(false)
  |. t_update("foo", true)         /* fast pipe */
  |. t_update("bar", true) 

1
2
3
4
5

val add : key -> 'a -> 'a t -> 'a t
let examplemap = 
  Map.empty 
  |> Map.add "foo" true
  |> Map.add "bar" true

Or, In Jane Street “named-argument” style
e.g. Real World OCaml

1
2
3
4

let examplemap = 
  Map.empty
  |> Map.add ~key:"foo" ~data:true
  |> Map.add ~key:"bar" ~data:true

Lightweight Meta-Programming in Coq - Notation

In Coq, we can leverage some meta programming:

1
2
3
4
5
6
7
8
9
10
11

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).

Notation "x '!->' v ';' m" := (t_update m x v)
  (at level 100, v at next level, right associativity).

Definition examplemap' :=
  ( "bar" !-> true;
    "foo" !-> true;
    _     !-> false
  ).

Noticed that the “Map building” is in a reversed order…

Note that we don’t need to define a find operation because it is just function application!

1
2
3

Example update_example2 : examplemap' "foo" = true.
Example update_example4 : examplemap' "bar" = true.
Example update_example1 : examplemap' "baz" = false. (* default *)

Partial Maps

we define partial maps on top of total maps.
A partial map with elements of type A is simply a total map with elements of type option A and default element None.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

Definition partial_map (A : Type) := total_map (option A).

Definition empty {A : Type} : partial_map A :=
  t_empty None.

Definition update {A : Type} (m : partial_map A)
           (x : string) (v : A) :=
  (x !-> Some v ; m).
  
Notation "x '⊢>' v ';' m" := (update m x v)
  (at level 100, v at next level, right associativity).

(** hide the empty case. Since it's always [None] **)
Notation "x '⊢>' v" := (update empty x v)
  (at level 100).
  
(** so nice **)
Example examplepmap :=
  ("Church" ⊢> true ; 
   "Turing" ⊢> false).

we use the “standard” map operator ↦ for partial map since maps in CS are usually partial.

Maps are functions

In many branches of mathematics, the term map is used to mean a function.
partial map = partial function,
total map = total function.

In category theory, “map” is often used as a synonym for morphism or arrow.

In formal logic, “map” is sometimes used for a functional symbol.

“Algorithms are the computational content of proofs.” —Robert Harper

So the book material is designed to be gradually reveal the facts that

Programming and proving in Coq are two sides of the same coin.

e.g.

• Inductive is useds for both data types and propositions.
• -> is used for both type of functions and logical implication.

The fundamental idea of Coq is that:

provability in Coq is represented by concrete evidence. When we construct the proof of a basic proposition, we are actually building a tree of evidence, which can be thought of as a data structure.

e.g.

• implication like A → B, its proof will be an evidence transformer: a recipe for converting evidence for A into evidence for B.

Proving manipulates evidence, much as programs manipuate data.

Curry-Howard Correspondence

deep connection between the world of logic and the world of computation:

propositions             ~  types
proofs / evidence        ~  terms / data values 

ev_0 : even 0

• ev_0 has type even 0
• ev_0 is a proof of / is evidence for even 0

ev_SS : ∀n, even n -> even (S (S n))

• takes a nat n and evidence for even n and yields evidence for even (S (S n)).

This is Props as Types.

Proof Objects

Proofs are data! We can see the proof object that results from this proof script.

1
2
3
4
5
6

Print ev_4.
(* ===> ev_4 = ev_SS 2 (ev_SS 0 ev_0) 
             : even 4  *)

Check (ev_SS 2 (ev_SS 0 ev_0)).     (* concrete derivation tree, we r explicitly say the number tho *)
(* ===> even 4 *)

These two ways are the same in principle!

Proof Scripts

Show Proof. will show the partially constructed proof terms / objects.
?Goal is the unification variable. (the hold we need to fill in to complete the proof)

more complicated in branching cases
one hole more subgoal

1
2
3
4
5
6
7
8
9
10

Theorem ev_4'' : even 4.   (*  match? (even 4) *)
Proof.
  Show Proof.              (*  ?Goal  *)
  apply ev_SS.
  Show Proof.              (*  (ev_SS 2 ?Goal)  *)
  apply ev_SS.
  Show Proof.              (*  (ev_SS 2 (ev_SS 0 ?Goal))  *)
  apply ev_0. 
  Show Proof.              (*  ?Goal (ev_SS 2 (ev_SS 0 ev_0))  *)
Qed.

Tactic proofs are useful and convenient, but they are not essential:
in principle, we can always construct the required evidence by hand

Agda doesn’t have tactics built-in. (but also Interactive)

Quantifiers, Implications, Functions

In Coq’s computational universe (where data structures and programs live), to give ->:

• constructors (introduced by Indutive)
• functions

in Coq’s logical universe (where we carry out proofs), to give implication:

• constructors
• functions!

So instead of writing proof scripts e.g._

1
2
3
4
5
6
7

Theorem ev_plus4 : ∀n, even n → even (4 + n).
Proof.
  intros n H. simpl.
  apply ev_SS.
  apply ev_SS.
  apply H.
Qed.

we can give proof object, which is a function here, directly!

1
2
3
4
5
6
7
8
9

Definition ev_plus4' : ∀n, even n → even (4 + n) :=    (* ∀ is syntax for Pi? *)
  fun (n : nat)    ⇒ 
  fun (H : even n) ⇒
    ev_SS (S (S n)) (ev_SS n H).


Definition ev_plus4'' (n : nat) (H : even n)           (* tricky: implicitly `Pi` when `n` get mentioned?  *)
                    : even (4 + n) :=
  ev_SS (S (S n)) (ev_SS n H).

two interesting facts:

1. intros x corresponds to λx. (or Pi x.??)
2. apply corresponds to…not quite function application… but more like filling the hole.
3. even n mentions the value of 1st argument n. i.e. dependent type!

Recall Ari’s question in “applying theorem as function” e.g. plus_comm
why we can apply value in type-level fun.
becuz of dependent type.

Now we call them dependent type function

→ is degenerated ∀ (Pi)

Notice that both implication (→) and quantification (∀) correspond to functions on evidence.
In fact, they are really the same thing: → is just a shorthand for a degenerate use of ∀ where there is no dependency, i.e., no need to give a name to the type on the left-hand side of the arrow:

1
2
3
4
5
6
7

  ∀(x:nat), nat 
= ∀(_:nat), nat 
= nat → nat

  ∀n, ∀(E : even n), even (n + 2).
= ∀n, ∀(_ : even n), even (n + 2).
= ∀n, even n → even (n + 2).

In general, P → Q is just syntactic sugar for ∀ (_:P), Q.

TaPL also mention this fact for Pi.

Q&A - Slide 15

1. ∀ n, even n → even (4 + n). (2 + n = S (S n))

Programming with Tactics.

If we can build proofs by giving explicit terms rather than executing tactic scripts,
you may be wondering whether we can build programs using tactics? Yes!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

Definition add1 : nat → nat.
  intro n.
  Show Proof.      
(** 
the goal (proof state):
    
    n : nat
    =======
    nat
    
the response:

    (fun n : nat => ?Goal) 
    
What is really interesting here, is that the premies [n:nat] is actually the arguments!
again, the process of applying tactics is _partial application_
**)

  apply S.
  Show Proof.      
(** 
    (fun n : nat => S ?Goal) 
**)
  apply n. 
Defined.

Print add1.
(* ==> add1 = fun n : nat => S n
            : nat -> nat *)

Notice that we terminate the Definition with a . rather than with := followed by a term.
This tells Coq to enter proof scripting mode (w/o Proof., which did nothing)

Also, we terminate the proof with Defined rather than Qed; this makes the definition transparent so that it can be used in computation like a normally-defined function
(Qed-defined objects are opaque during computation.).

Qed make things unfoldable,
thus add 1 ends with Qed is not computable…
(becuz of not even unfoldable thus computation engine won’t deal with it)

Prof.Mtf: meaning “we don’t care about the details of Proof”

see as well Smart Constructor

This feature is mainly useful for writing functions with dependent types

In Coq - you do as much as ML/Haskell when you can…?
Unlike Agda - you program intensively in dependent type…?

When Extracting to OCaml…Coq did a lot of Object.magic for coercion to bypass OCaml type system. (Coq has maken sure the type safety.)

Logical Connectives as Inductive Types

Inductive definitions are powerful enough to express most of the connectives we have seen so far.
Indeed, only universal quantification (with implication as a special case) is built into Coq;
all the others are defined inductively.
Wow…

CoqI: What’s Coq logic? Forall + Inductive type (+ coinduction), that’s it.

Conjunctions

1
2
3
4
5
6
7

Inductive and (P Q : Prop) : Prop :=
| conj : P → Q → and P Q.

Print prod.
(* ===>
   Inductive prod (X Y : Type) : Type :=
   | pair : X -> Y -> X * Y. *)

similar to prod (product) type… more connections happening here.

This similarity should clarify why destruct and intros patterns can be used on a conjunctive hypothesis.

Similarly, the split tactic actually works for any inductively defined proposition with exactly one constructor
(so here, apply conj, which will match the conclusion and generate two subgoal from assumptions )

A very direct proof:

1
2
3
4

Definition and_comm'_aux P Q (H : P ∧ Q) : Q ∧ P :=
  match H with
  | conj HP HQ ⇒ conj HQ HP
  end.

Disjunction

1
2
3

Inductive or (P Q : Prop) : Prop :=
| or_introl : P → or P Q
| or_intror : Q → or P Q.

this explains why destruct works but split not..

Q&A - Slide 22 + 24

Both Question asked about what’s the type of some expression

1
2
3
4
5
6
7
8
9
10

fun P Q R (H1: and P Q) (H2: and Q R) ⇒
    match (H1,H2) with
    | (conj _ _ HP _, conj _ _ _ HR) ⇒ conj P R HP HR
    end.

fun P Q H ⇒
    match H with
    | or_introl HP ⇒ or_intror Q P HP
    | or_intror HQ ⇒ or_introl Q P HQ
    end.

But if you simply Check on them, you will get errors saying:
Error: The constructor conj (in type and) expects 2 arguments. or
Error: The constructor or_introl (in type or) expects 2 arguments..

Coq Magics, “Implicit” Implicit and Overloading??

So what’s the problem?
Well, Coq did some magics…

1
2
3
4

Print and.
(* ===> *)
Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B
For conj: Arguments A, B are implicit

constructor conj has implicit type arg w/o using {} in and …

1
2
3
4
5
6
7
8
9
10
11

Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B

For or_introl, when applied to no more than 1 argument:
  Arguments A, B are implicit
For or_introl, when applied to 2 arguments:
  Argument A is implicit
For or_intror, when applied to no more than 1 argument:
  Arguments A, B are implicit
For or_intror, when applied to 2 arguments:
  Argument B is implicit

this is even more bizarre…
constructor or_introl (and or_intror) are overloaded!! (WTF)

And the questions’re still given as if they’re inside the modules we defined our plain version of and & or (w/o any magics), thus we need _ in the positions we instantiate and & or so Coq will infer.

Existential Quantification

To give evidence for an existential quantifier, we package a witness x together with a proof that x satisfies the property P: