Lecture 02

infer some type arguments automatically
Set Implicit Arguments.

Inductive list (A: Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.

Fixpoint length (A: Set) (l: list A) : nat :=
  match l with
  | nil => O
  | cons x xs => S (length xs)
  end.

so far, Coq will not infer the type argument for nil: 
Check (cons 1 nil).

Error: The term "nil" has type "forall A : Set, list A"
 while it is expected to have type "list nat".

Check (cons 1 (nil nat)).

we can tell Coq to always try though
Arguments nil {A}.

Check (cons 1 nil).
Eval cbv in (length (cons 1 nil)).
Eval cbv in (length (cons 2 (cons 1 nil))).
Eval cbv in (length nil).

Fixpoint countdown (n: nat) :=
  match n with
  | O => cons n nil
  | S m => cons n (countdown m)
  end.

Eval cbv in (countdown 0).
Eval cbv in (countdown 3).
Eval cbv in (countdown 10).

Fixpoint map (A B: Set) (f: A -> B) (l: list A) : list B :=
  match l with
  | nil => nil
  | cons x xs => cons (f x) (map f xs)
  end.

Eval cbv in (map (plus 1) (countdown 3)).
Eval cbv in (map (fun _ => true) (countdown 3)).

Definition is_zero (n: nat) : bool :=
  match n with
  | O => true
  | S m => false
  end.

Eval cbv in (map is_zero (countdown 3)).

Fixpoint is_even (n: nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S m) => is_even m
  end.

Eval cbv in (map is_even (countdown 3)).

Lemma map_length:
  forall (A B: Set) (f: A -> B) (l: list A),
  length (map f l) = length l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

discuss how does induction works

Definition compose (A B C: Set)
                   (f: B -> C)
                   (g: A -> B)
                   : A -> C :=
  fun x => f (g x).

Lemma map_map_compose:
  forall (A B C: Set)
         (g: A -> B) (f: B -> C) (l: list A),
  map f (map g l) = map (compose f g) l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  +
    simpl. rewrite IHl.
need to "unfold" compose to simpl
    unfold compose. reflexivity.
Qed.

Fixpoint foldr (A B: Set) (f: A -> B -> B)
               (l: list A) (b: B) : B :=
  match l with
  | nil => b
  | cons x xs => f x (foldr f xs b)
  end.

foldr f (cons 1 (cons 2 (cons 3 nil))) x > f 1 (f 2 (f 3 x))

Check plus.
Print plus.
Eval cbv in (foldr plus (countdown 10) 0).

Fixpoint fact (n: nat) : nat :=
  match n with
  | O => 1
  | S m => mult n (fact m)
  end.

Eval cbv in (fact 0).
Eval cbv in (fact 1).
Eval cbv in (fact 2).
Eval cbv in (fact 3).
Eval cbv in (fact 4).

Definition fact´ (n: nat) : nat :=
  match n with
  | O => 1
  | S m => foldr mult (map (plus 1) (countdown m)) 1
  end.

Eval cbv in (fact´ 0).
Eval cbv in (fact´ 1).
Eval cbv in (fact´ 2).
Eval cbv in (fact´ 3).
Eval cbv in (fact´ 4).

Lemma fact_fact´:
  forall n,
  fact n = fact´ n.
Proof.
challenge problem
Admitted.

we can also define map using fold
Definition map´ (A B: Set) (f: A -> B) (l: list A) : list B :=
  foldr (fun x acc => cons (f x) acc) l nil.

Lemma map_map´:
  forall (A B: Set) (f: A -> B) (l: list A),
  map f l = map´ f l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite IHl.
again, need to unfold so simpl can work
    unfold map´. simpl.
    reflexivity.
note: very sensitive to order of rewrite and unroll!
Qed.

another flavor of fold
Fixpoint foldl (A B: Set) (f: A -> B -> B)
               (l: list A) (b: B) : B :=
  match l with
  | nil => b
  | cons x xs => foldl f xs (f x b)
  end.

add one list to the end of another
Fixpoint app (A: Set) (l1: list A) (l2: list A) : list A :=
  match l1 with
  | nil => l2
  | cons x xs => cons x (app xs l2)
  end.

Eval cbv in (app (cons 1 (cons 2 nil)) (cons 3 nil)).

Theorem app_nil:
  forall A (l: list A),
  app l nil = l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

Theorem app_assoc:
  forall A (l1 l2 l3: list A),
  app (app l1 l2) l3 = app l1 (app l2 l3).
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

simple but inefficient way to reverse a list
Fixpoint rev (A: Set) (l: list A) : list A :=
  match l with
  | nil => nil
  | cons x xs => app (rev xs) (cons x nil)
  end.

tail recursion is faster, but more complicated
Fixpoint fast_rev_aux (A: Set) (l: list A) (acc: list A) : list A :=
  match l with
  | nil => acc
  | cons x xs => fast_rev_aux xs (cons x acc)
  end.

Definition fast_rev (A: Set) (l: list A) : list A :=
  fast_rev_aux l nil.

let's make sure we got that right
Theorem rev_ok:
  forall A (l: list A),
  fast_rev l = rev l.
Proof.
  intros.
  induction l.
  + simpl.
reduces rev, but does nothing to rev_fast
    unfold fast_rev.
unfold fast_rev to fast_rev_aux
    simpl.
now we can simplify the term
    reflexivity.
TIP: if simpl doesn't work, try unfolding!
  + unfold fast_rev in *.
this looks like it could be trouble...
    simpl. rewrite <- IHl.
STUCK! need to know about the rev_aux accumulator (acc) TIP: if your IH seems weak, try proving something more general
Abort.

Lemma fast_rev_aux_ok:
  forall A (l1 l2: list A),
  fast_rev_aux l1 l2 = app (rev l1) l2.
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl.
STUCK AGAIN! need to know for *any* l2 TIP: if your IH seems weak, only intro up to the induction variable
Abort.

Lemma fast_rev_aux_ok:
  forall A (l1 l2: list A),
  fast_rev_aux l1 l2 = app (rev l1) l2.
Proof.
  intros A l1.
  induction l1.
  + intros. simpl. reflexivity.
  + intros. simpl.
    rename l2 into foo.
    rewrite IHl1.
    rewrite app_assoc.
    simpl. reflexivity.
Qed.

now we can prove rev_ok as a special case of rev_aux_ok
Lemma fast_rev_ok:
  forall A (l: list A),
  fast_rev l = rev l.
Proof.
  intros.
  unfold fast_rev.
  rewrite fast_rev_aux_ok.
  rewrite app_nil.
  reflexivity.
Qed.



	                            ~-.
          ,,,;            ~-.~-.~-
         (.../           ~-.~-.~-.~-.~-.
         } o~`,         ~-.~-.~-.~-.~-.~-.
         (/    \      ~-.~-.~-.~-.~-.~-.~-.
          ;    \    ~-.~-.~-.~-.~-.~-.~-.
         ;     {_.~-.~-.~-.~-.~-.~-.~
        ;:  .-~`    ~-.~-.~-.~-.~-.
       ;.: :'    ._   ~-.~-.~-.~-.~-
        ;::`-.    '-._  ~-.~-.~-.~-
         ;::. `-.    '-,~-.~-.~-.
          ';::::.`''-.-'
            ';::;;:,:'
               '||"
               / |
             ~` ~"'
add an element to the end of a list
Fixpoint snoc (A: Set) (l: list A) (x: A) : list A :=
  match l with
  | nil => cons x nil
  | cons y ys => cons y (snoc ys x)
  end.

Theorem snoc_app_singleton:
  forall A (l: list A) (x: A),
  snoc l x = app l (cons x nil).
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

Theorem app_snoc_l:
  forall A (l1: list A) (l2: list A) (x: A),
  app (snoc l1 x) l2 = app l1 (cons x l2).
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

Theorem app_snoc_r:
  forall A (l1: list A) (l2: list A) (x: A),
  app l1 (snoc l2 x) = snoc (app l1 l2) x.
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

simple but inefficient way to reverse a list
Fixpoint rev_snoc (A: Set) (l: list A) : list A :=
  match l with
  | nil => nil
  | cons x xs => snoc (rev_snoc xs) x
  end.

Lemma fast_rev_aux_ok_snoc:
  forall A (l1 l2: list A),
  fast_rev_aux l1 l2 = app (rev_snoc l1) l2.
Proof.
  intros A l1.
  induction l1.
  + intros. simpl. reflexivity.
  + intros. simpl.
    rewrite IHl1.
    rewrite app_snoc_l.
    reflexivity.
Qed.

Lemma fast_rev_ok_snoc:
  forall A (l: list A),
  fast_rev l = rev_snoc l.
Proof.
  intros.
  unfold fast_rev.
  rewrite fast_rev_aux_ok_snoc.
  rewrite app_nil.
  reflexivity.
Qed.

Lemma length_app:
  forall A (l1 l2: list A),
  length (app l1 l2) = plus (length l1) (length l2).
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

Lemma plus_1_S:
  forall n,
  plus n 1 = S n.
Proof.
  intros.
  induction n.
  + simpl. reflexivity.
  + simpl. rewrite IHn. reflexivity.
Qed.

Lemma rev_length:
  forall A (l: list A),
  length (rev l) = length l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite length_app.
    simpl. rewrite plus_1_S.
    rewrite IHl. reflexivity.
Qed.

Lemma rev_app:
  forall A (l1 l2: list A),
  rev (app l1 l2) = app (rev l2) (rev l1).
Proof.
  intros.
  induction l1.
  + simpl. rewrite app_nil. reflexivity.
  + simpl. rewrite IHl1. rewrite app_assoc.
    reflexivity.
Qed.

Lemma rev_involutive:
  forall A (l: list A),
  rev (rev l) = l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite rev_app.
    simpl. rewrite IHl. reflexivity.
Qed.

END LECTURE 02

SYNTAX
We can define a programming language as an inductive datatype.
include string library for variable names
Require Import String.

E ::= N | V | E + E | E * E | E ? E
Inductive expr : Set :=
| Const : nat -> expr
| Var : string -> expr
| Add : expr -> expr -> expr
| Mul : expr -> expr -> expr
| Cmp : expr -> expr -> expr.

S ::= Skip | V <- E | S ;; S | IF E THEN S ELSE S | WHILE E S
Inductive stmt : Set :=
| Skip : stmt
| Asgn : string -> expr -> stmt
| Seq : stmt -> stmt -> stmt
| Cond : expr -> stmt -> stmt -> stmt
| While : expr -> stmt -> stmt.

Programs are just elements of type stmt.

Definition prog_skip : stmt :=
  Skip.

Definition prog_set_x : stmt :=
  Asgn "x" (Const 1).

Definition prog_incr_x_forever : stmt :=
  While (Const 1) (Asgn "x" (Const 1)).

Definition prog_xth_fib_in_y : stmt :=
  Seq (Asgn "y" (Const 0)) (
  Seq (Asgn "y0" (Const 1)) (
  Seq (Asgn "y1" (Const 0)) (
  Seq (Asgn "i" (Const 0)) (
      While (Cmp (Var "i") (Var "x")) (
            Seq (Asgn "y" (Add (Var "y0") (Var "y1"))) (
            Seq (Asgn "y0" (Var "y1")) (
            Seq (Asgn "y1" (Var "y")) (
                (Asgn "i" (Add (Var "i") (Const 1)))
            ))))
  )))).

but nobody wants to write programs like this, so Coq provides a "Notation" mechanism

Notation "´C´ X" := (Const X) (at level 80).
Notation "´V´ X" := (Var X) (at level 81).
Notation "X <+> Y" := (Add X Y) (at level 83, left associativity).
Notation "X <*> Y" := (Mul X Y) (at level 82, left associativity).
Notation "X <?> Y" := (Cmp X Y) (at level 84).

Notation "X <- Y" := (Asgn X Y) (at level 86).
Notation "X ;; Y" := (Seq X Y) (at level 87, left associativity).
Notation "´IF´ X ´THEN´ Y ´ELSE´ Z" := (Cond X Y Z) (at level 88).
Notation "´WHILE´ X {{ Y }}" := (While X Y) (at level 89).

Definition prog_fib : stmt :=
  "y" <- C 0;;
  "y0" <- C 1;;
  "y1" <- C 0;;
  "i" <- C 0;;
  WHILE (V"i" <?> V"x") {{
    "y" <- V"y0" <+> V"y1";;
    "y0" <- V"y1";;
    "y1" <- V"y";;
    "i" <- V"i" <+> C 1
  }}.

Notation provides us with "concrete" syntax which "desugars" to the underlying "abstract syntax tree".

Fixpoint nconsts (e: expr) : nat :=
  match e with
  | Const _ => 1
  | Var _ => 0
  | Add e1 e2 => plus (nconsts e1) (nconsts e2)
  | Mul e1 e2 => plus (nconsts e1) (nconsts e2)
  | Cmp e1 e2 => plus (nconsts e1) (nconsts e2)
  end.

Lemma has_3_consts:
  exists e, nconsts e = 3.
Proof.
  exists (Add (Const 1) (Add (Const 2) (Const 3))).
  simpl. reflexivity.
Qed.

Fixpoint expr_with_n_consts (n: nat) : expr :=
  match n with
  | O => Var "x"
  | S m => Add (Const 0) (expr_with_n_consts m)
  end.

Lemma has_n_consts:
  forall n,
  exists e, nconsts e = n.
Proof.
  intros.
  exists (expr_with_n_consts n).
  induction n.
  + simpl. reflexivity.
  + simpl. rewrite IHn. reflexivity.
Qed.

Definition orb (b1 b2: bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

Fixpoint has_const (e: expr) : bool :=
  match e with
  | Const _ => true
  | Var _ => false
  | Add e1 e2 => orb (has_const e1) (has_const e2)
  | Mul e1 e2 => orb (has_const e1) (has_const e2)
  | Cmp e1 e2 => orb (has_const e1) (has_const e2)
  end.

Fixpoint has_var (e: expr) : bool :=
  match e with
  | Const _ => false
  | Var _ => true
  | Add e1 e2 => orb (has_var e1) (has_var e2)
  | Mul e1 e2 => orb (has_var e1) (has_var e2)
  | Cmp e1 e2 => orb (has_var e1) (has_var e2)
  end.

Lemma expr_bottoms_out:
  forall e,
  orb (has_const e) (has_var e) = true.
Proof.
  intros.
  induction e.
  +
const
    simpl. reflexivity.
  +
var
    simpl. reflexivity.
  +
add
    simpl.
    destruct (has_const e1).
    -
e1 has a const
      simpl. reflexivity.
    -
e1 does not have a const
      destruct (has_const e2).
      *
e2 has a const
        simpl. reflexivity.
      *
e2 does not have a const
        simpl.
we also want to simplify in the hypotheses
        simpl in *.
and rewrite with the results
        rewrite IHe1. rewrite IHe2.
        simpl. reflexivity.
  +
mul
    simpl.
    destruct (has_const e1).
    -
e1 has a const
      simpl. reflexivity.
    -
e1 does not have a const
      destruct (has_const e2).
      *
e2 has a const
        simpl. reflexivity.
      *
e2 does not have a const
        simpl.
we also want to simplify in the hypotheses
        simpl in *.
and rewrite with the results
        rewrite IHe1. rewrite IHe2.
        simpl. reflexivity.
  +
cmp
    simpl.
    destruct (has_const e1).
    -
e1 has a const
      simpl. reflexivity.
    -
e1 does not have a const
      destruct (has_const e2).
      *
e2 has a const
        simpl. reflexivity.
      *
e2 does not have a const
        simpl.
we also want to simplify in the hypotheses
        simpl in *.
and rewrite with the results
        rewrite IHe1. rewrite IHe2.
        simpl. reflexivity.
Qed.

THE ABOVE PROOF IS VERY BAD. Make it better! Hint: think about how to rearrange the orbs.
Some interesting types

Inductive True : Prop :=
| I : True.

Inductive False : Prop :=
.

Lemma bogus:
  False -> 1 = 2.
Proof.
  intros.
  inversion H.
Qed.

Lemma also_bogus:
  1 = 2 -> False.
Proof.
  intros.
  discriminate.
Qed.

Inductive yo : Prop :=
| yolo : yo -> yo.

Lemma yoyo:
  yo -> False.
Proof.
  intros.
  inversion H.
well, that didn't work
  induction H.
  assumption.
but that did!
Qed.
This page has been generated by coqdoc