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!