coq_intro.v

(****************************************)
(* datatypes and functional programming *)
(****************************************)

(* We can define (inductive) datatypes like in Haskell
   (where 'Set' corresponds to Haskell's '*')
*)
Inductive mynat : Set
  := zero : mynat | plus1 : mynat -> mynat.

(* 'Check' is like ':t' in ghci
*) 
Check mynat.

Check zero.
Check (plus1 (plus1 zero)).

Check plus1.

Check nat.
Print nat.
  (* Inductive nat : Set :=  O : nat | S : nat -> nat *)

Check O.
Check (S (S O)).
Check 2.

Print bool.
  (* Inductive bool : Set :=  true : bool | false : bool *)

Definition is_zero (n : nat) : bool
  := match n with
     | 0                 => true
     | _ (* otherwise *) => false 
     end.

Check is_zero.
Check is_zero 0.

Eval compute in is_zero 0.

(* to define recursive functions we use the
   'Fixpoint' keyword instead of 'Definition'
*)
Fixpoint is_even (n : nat) : bool
  := match n with
     | 0        => true
     | 1        => false
     | S (S n') => is_even n'
     end.

Eval compute in is_even 41.
Eval compute in is_even 42.

(* Note that this (seemingly equivalent) definition
   of "is_even" will NOT be accepted by coq due to the
   fact that coq isn't able to infer that "n-2" is
   structurally smaller than "n".
*)
(* Fixpoint is_even' (n : nat) : bool
  := match n with
     | 0  => true
     | 1  => false
     | _  => is_even' (n-2)
     end. 
*)
 

(* There are, however, ways to define "is_even'" with the
   additional help of the "Program ..." command(s):
*)

Require Import Coq.Program.Program.
 
Program Fixpoint is_even' (n : nat) {measure n} : bool
  := match n with
     | 0 => true
     | 1 => false
     | _ => is_even' (n-2)
     end. 
Next Obligation. (*
      1 subgoal
      n : nat
      H : 1 <> n
      H0 : 0 <> n
      ============================== (1/1)
      n - 2 < n
*)
Proof.
  destruct n as [| n'].
  - (* H0 : 0 <> 0
       ===========
       0 - 2 < 0  *)
    exfalso. (* Goal is "False" now. *)
    apply H0. (* this works because "0 <> 0" actually
                 is "0 = 0 -> False", i.e.
                 "not P" is implemented as "P -> False". *)
    reflexivity.
  - (* goal:  S n' - 2 < S n'  *)
    simpl.  (* ~>  n' - 1 < S n'  *)
    rewrite <- Minus.pred_of_minus.  (* ~>  pred n' < S n'  *)
    unfold lt (* < *).  (* ~>  S (pred n') <= S n'
                               because:  x < y  :=  S x <= y  *)
    apply Le.le_n_S. (* ~>  pred n' <= n'  *)
    apply Le.le_pred_n. (* done *)
    (* Alternatively, the last three steps could be
       replaced by
         "auto with arith."
       which instructs coq to do proof search using the lemmas
       in the hint database "arith" (containing the two results
       from the "Le"-module, we used above). *)
Defined.
(* Done. *)
 

Require Import List.

Print list.
  (* Inductive list (A : Type) : Type :=
       nil : list A | cons : A -> list A -> list A *)

Check (cons 42 nil).

Check 42 :: nil.

Import ListNotations.

Check [42; 0].

Eval compute in head [42; 0].
Check head. (* : forall A : Type, list A -> option A *)
Print option.
  (* Inductive option (A : Type) : Type :=
       Some : A -> option A | None : option A *)
    

Check fold_left.
  (* : forall A B : Type, (A -> B -> A) -> list B -> A -> A *)


(**********)
(* Proofs *)
(**********)

Example foo1 : is_zero 0 = true.
Proof.
  compute.
  reflexivity. (* solves "x = x"  ... *)
Qed.

Example foo2 : is_even 41 = false.
Proof.
  reflexivity. (* ... but also reduces both sides
                  first (i.e. prior "compute"/"simpl"
                  isn't necessary). *)
Qed.

Parameter n : nat.

Lemma foo3 : n = 0 -> is_zero n = true.
Proof.
  (* don't:
  compute. *)
  (* ok (but might do "nothing"): *)
  (* simpl. *)
  intro H. (* introduces "n = 0" as local hypothesis "H" *)
  rewrite -> H. (* rewrite with the equality "H : n = 0",
                   replacing "n"s with "0" in the goal.
                   ("rewrite <- H" would replace "0"s with "n".) *)
  exact foo1. (* the goal is now exactly (the conclusion of)
                 lemma "foo1" which we already proved above. *)
Qed.

(* Lemma foo4 : is_zero n -> is_even n. *)
    (* Error: The term "is_zero n" has type "bool"
       which should be Set, Prop or Type. *)

(* Q: So which terms are "logical building blocks" in coq? *)

Check (n = 0). (* : Prop *)
Check (1 = 0). (* : Prop *) 

(* A: The universe "Prop" includes all types that encode
      logical propositions.
   
   In fact: "x = y" is just a notation for "eq x y" where *)
Print eq.
  (* Inductive eq (A : Type) (x : A) : A -> Prop :=
       eq_refl : x = x *)
(* is also just a type with a single constructor ... *)

Check (n = 0 /\ n = 1). (* : Prop *)

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

Section Proofs.
  Variable P Q : Prop.
  
  Lemma and_com : P /\ Q -> Q /\ P.
  Proof.
    intro H.
    destruct H as [HP HQ]. (* "H : P /\ Q" must be built
                              using the "conj" constructor,
                              so we know that we must have
                              proofs "HP" of "P" and "HQ" of "Q". *)
    split. (* to solve the goal "Q /\ P"
              we have to provide proofs for "Q" and "P". *)
    - (* first case:  need a proof for "Q" *) exact HQ.
    - (* second case: need a proof for "P" *) exact HP.
  Qed.
  
  Print and_com.
    (* and_com =
       fun (H : P /\ Q) => match H with
                           | conj HP HQ => conj HQ HP
                           end
       : P /\ Q -> Q /\ P  *)
  
  (* So the proof (and_com) is just an inhabitant of the type
     "P /\ Q -> Q /\ P", i.e. a function that takes a proof
     of "P /\ Q" and yields a proof of "Q /\ P".
  
     This is an instance of the "Curry-Howard correspondence"
     which relates (in a bijective way) proofs and programs,
     i.e. (put simply) "proofs and programs are the same thing". *)

  (* This means that we can also provide the proof term
     for some "lemma" directly, as in the following "proof"
     of "or_com": *)
  
  Definition or_com : P \/ Q -> Q \/ P
    := fun H : P \/ Q =>
            match H with
            | or_introl HP => or_intror HP
            | or_intror HQ => or_introl HQ
            end.
  
  Print or.
    (* Inductive or (A B : Prop) : Prop :=
	 or_introl : A -> A \/ B | or_intror : B -> A \/ B  *)
End Proofs.

(* Dependent types make it possible to build "Prop"s
   like the following: *)

Lemma sum0 : forall r s : nat,
  (r + s = 0  ->  r = 0 /\ s = 0).
(* 
   This a "dependent product" (or "pi-type"),
   because "r" and "s" occure in the "body of the 'forall'".
   This is different from Haskell's polymorphism,
   because "r" and "s" don't range over types
   but over values of type "nat" (which are not types)!
*)
Proof.
  intros r s.
  destruct r as [|r'].
  - (* goal:  0 + s = 0 -> 0 = 0 /\ s = 0  *)
    intro H.
    simpl in H.  (*  H : 0 + s = 0  ~>  H : s = 0  *)
    rewrite H.  (* short for "rewrite -> H" *)
    (* The goal is now "0 = 0 /\ 0 = 0" which
       could be solved via "split; reflexivity." for example.
       But this goal is actually "tautologically enough" to
       be solved by the proof search tactic "tauto" (or "auto"). *)
    tauto.
  - (* goal:  S r' + s = 0 -> S r' = 0 /\ s = 0  *)
    intro H.
    exfalso.
    simpl in H.  (* r' s : nat
                    H : S (r' + s) = 0
                    ==================
                    False  *)
    discriminate H.  (* infers a contradiction from "H":
                        something built via the constructor "S"
                        can't equal the term "0" built with
                        via the constructor "O". *)
Qed.

(**)