Coq takes on many identities, with two in particular that you need to be comfortable with.

On the one hand, Coq is a dependently typed programming language. In other words, we use it to reason about functions that consume things and produce data types.

On the other hand, Coq is a proof scripting language. In other words, we use it to compute terms of particular types.

Of course the only sensible way to proceed is by example

Natural numbers are a type

Print nat.
    

     

      

       Inductive nat : Set :=  O : nat | S : nat -> nat.

Arguments S _%nat_scope
      
     
    
   
   

  
  Check nat_ind. (* recall induction *)
  

   

    

     nat_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n
    
   
  
 

Ordered collections tagged with their fixed length are a dependent type.

From Coq Require Import Vector.
Check t.


 

  t
     : Type -> nat -> Type
 

The point here is that the type t is a function that lands in Type. It's not a type yet until it is applied to some type (the elements) and some nat (the length)

We also reason about vectors t A n (for type A and nat n) with induction

Check t_ind.



t_ind
     : forall (A : Type)
         (P : forall n : nat, t A n -> Prop),
       P 0 (nil A) ->
       (forall (h : A) (n : nat) (t : t A n),
        P n t -> P (S n) (cons A h n t)) ->
       forall (n : nat) (t : t A n), P n t

The general story of which natural number induction is a special case is called structural induction. We can do structural induction every time an _ind is generated, which is anytime we use the Inductive keyword.

Inductive tree (A : Type) : Type := Leaf (x : A) | Node (t1 : tree A) (t2 : tree A).

So if we want to prove that a function from A to B can turn a tree A into a tree B,

Theorem fmap_tree {A B : Type} (f : A -> B) (x : tree A) : tree B.




A, B: Type
f: A -> B
x: tree A






tree B








Proof.




A, B: Type
f: A -> B
x: tree A






tree B








  (* we apply the induction principle *)
  induction x. (* the *tactic* induction invokes the term `tree_ind` under the hood *)




A, B: Type
f: A -> B
x: A






tree B






A, B: Type
f: A -> B
x1, x2: tree A
IHx1, IHx2: tree B






tree B









  -




A, B: Type
f: A -> B
x: A






tree B





 

apply (Leaf _ (f x)). (* construct the exact term for the base case*)
  -




A, B: Type
f: A -> B
x1, x2: tree A
IHx1, IHx2: tree B






tree B





 

apply (Node _ IHx1 IHx2). (* construct the exact term for the recursive step. *)
Defined.

This is the proof script version of implementing fmap_tree.

equivalently, we can provide a direct definition

Fixpoint fmap_tree' {A B : Type} (f : A -> B) (x : tree A) : tree B
  := match x with
     | Leaf _ x => Leaf _ (f x)
     | Node _ t1 t2 => Node _ (fmap_tree' f t1) (fmap_tree' f t2)
     end.

Bool and Prop

NOTE: I WROTE THIS BEFORE I DECIDED TO USE MATHCOMP, SO IT'LL BE DELETED

We will leverage the property of decidability, which some propositions have.

Coq takes place in constructive logic, meaning law of excluded middle (LEM) is omitted.

In many elementary logic courses, bool - the values of boolean algebra - and prop - the set of propositions - are strictly equivalent. One of the reasons they're able to do this is LEM

Module LEM_test.
  Axiom LEM : forall (P : Prop), P \/ ~ P.
End LEM_test.

The "middle" in the name is the idea of indeterminacy, we don't know if the proposition is true or false. With this axiom, we exclude the middle, we exclude the ability for propositions to be indeterminate

In constructivism, with it's primary logic called intuitionism, we do not have such an axiom. For many propositions, we simply don't know if they're true or false. One thing we like to do even in intuitionism is distinguish a class of propositions for which we can recover the equivalence between bool and prop The functional account of this lives in the standard library

From Coq.Logic Require Import Decidable.
Check decidable.



decidable
     : Prop -> Prop







Print decidable.



decidable =
fun P : Prop => P \/ ~ P
     : Prop -> Prop

Arguments decidable P%type_scope

We may, toward the middle or the end of the book, rely on the typeclass account of this, but idk yet.

From Coq Require Import Lia.



[Loading ML file ring_plugin.cmxs (using legacy method) ... done]


[Loading ML file zify_plugin.cmxs (using legacy method) ... done]


[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]







From Coq.Arith Require Import PeanoNat.
Check Nat.Even.



Nat.Even
     : nat -> Prop







Print Nat.Even.



Nat.Even =
fun n : nat => exists m : nat, n = 2 * m
     : nat -> Prop

Arguments Nat.Even n%nat_scope








Lemma L1 : forall n, ~ (Nat.Even n /\ Nat.Even (S n)).







forall n : nat, ~ (Nat.Even n /\ Nat.Even (S n))








Proof.







forall n : nat, ~ (Nat.Even n /\ Nat.Even (S n))








  intros n contra.




n: nat
contra: Nat.Even n /\ Nat.Even (S n)






False








  destruct contra.




n: nat
H: Nat.Even n
H0: Nat.Even (S n)






False








  induction n as [| n' IHn'].




H: Nat.Even 0
H0: Nat.Even 1






False






n': nat
H: Nat.Even (S n')
H0: Nat.Even (S (S n'))
IHn': Nat.Even n' -> Nat.Even (S n') -> False






False









  -




H: Nat.Even 0
H0: Nat.Even 1






False





 

unfold Nat.Even in H0.




H: Nat.Even 0
H0: exists m : nat, 1 = 2 * m






False








    destruct H0 as [m H0].




H: Nat.Even 0
m: nat
H0: 1 = 2 * m






False








    lia.
  -




n': nat
H: Nat.Even (S n')
H0: Nat.Even (S (S n'))
IHn': Nat.Even n' -> Nat.Even (S n') -> False






False





 

inversion H.




n': nat
H: Nat.Even (S n')
H0: Nat.Even (S (S n'))
IHn': Nat.Even n' -> Nat.Even (S n') -> False
x: nat
H1: S n' = 2 * x






False








    unfold Nat.Even in H, H0.




n': nat
H: exists m : nat, S n' = 2 * m
H0: exists m : nat, S (S n') = 2 * m
IHn': Nat.Even n' -> Nat.Even (S n') -> False
x: nat
H1: S n' = 2 * x






False








    destruct H as [m H].




n', m: nat
H: S n' = 2 * m
H0: exists m : nat, S (S n') = 2 * m
IHn': Nat.Even n' -> Nat.Even (S n') -> False
x: nat
H1: S n' = 2 * x






False








    destruct H0 as [m0 H0].




n', m: nat
H: S n' = 2 * m
m0: nat
H0: S (S n') = 2 * m0
IHn': Nat.Even n' -> Nat.Even (S n') -> False
x: nat
H1: S n' = 2 * x






False








    rewrite H in H1.




n', m: nat
H: S n' = 2 * m
m0: nat
H0: S (S n') = 2 * m0
IHn': Nat.Even n' -> Nat.Even (S n') -> False
x: nat
H1: 2 * m = 2 * x






False








    lia.
Qed.