Lecture 03

include some useful libraries
Require Import Bool.
Require Import List.
Require Import String.
Require Import Omega.

List provides the cons notation "::"
"x :: xs" is the same as "cons x xs"
Fixpoint my_length {A: Set} (l: list A) : nat :=
  match l with
  | nil => O
  | x :: xs => S (my_length xs)
  end.

List provides the append notation "++"
"xs ++ ys" is the same as "app xs ys"
Fixpoint my_rev {A: Set} (l: list A) : list A :=
  match l with
  | nil => nil
  | x :: xs => rev xs ++ x :: nil
  end.

some interesting types
Prop is like Set, but for propositions
Inductive myTrue : Prop :=
| I : myTrue.

Lemma foo:
  myTrue.
Proof.
  constructor.
exact I.
Qed.

Lemma foo´:
  Set.
Proof.
  exact (list nat).
exact bool.
Qed.

Inductive myFalse : Prop :=
.

Print False.

Lemma bogus:
  False -> 1 = 2.
Proof.
  intros.
inversion does case analysis on a hypothesis. For each way that hypothesis could have been proved, you need to complete the subgoal
  inversion H.
Qed.

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

Print eq.

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

Lemma yoyo:
  yo -> False.
Proof.
  intros.
  inversion H.
  inversion H0.
  inversion H1.
well, that didn't work
  induction H.
  assumption.
but that did!
Qed.

check out negation
Print not.

Expression Syntax

We can define parts of a language as an inductive datatype.
Inductive expr : Set :=
| Const : nat -> expr
| Var : string -> expr
| Add : expr -> expr -> expr
| Mul : expr -> expr -> expr
| Cmp : expr -> expr -> expr.

Check (Const 0).
Check (Var "x").
Check (Add (Const 0) (Var "x")).
Check (Mul (Add (Const 0) (Var "x"))
           (Add (Const 0) (Var "x"))).
Check (Cmp (Mul (Const 0) (Var "x"))
           (Mul (Var "y") (Const 0))).

On paper, this would be written as a "BNF grammar" as: 
    expr ::= N
          |  V
          |  expr <+> expr
          |  expr <*> expr
          |  expr <?> expr
Coq provides mechanism to define your own notation which we can use to get "concrete syntax"
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).

Check (C 0).
Check (V"x").
Check (C 0 <+> V"x").
Check (C 0 <+> V"x" <*> C 0 <+> V"x").
Check ((C 0 <+> V"x") <*> (C 0 <+> V"x")).
Check (C 0 <*> V"x" <?> V"y" <*> C 0).

try View ==> Display all basic low-level contents
parsing is classic CS topic, but won't say much more
we can write functions to analyze expressions
Fixpoint nconsts (e: expr) : nat :=
  match e with
  | Const _ => 1
same as S O
  | Var _ => 0
same as O
  | Add e1 e2 => nconsts e1 + nconsts e2
                 
same as plus (nconsts e1) (nconsts e2)
  | Mul e1 e2 => nconsts e1 + nconsts e2
  | Cmp e1 e2 => nconsts e1 + nconsts e2
  end.

Coq also provides existential quantifiers
Lemma expr_w_3_consts:
  exists e,
  nconsts e = 3.
Proof.
  exists (C 3 <+> C 2 <+> C 1).
  simpl. reflexivity.
Qed.

Fixpoint esize (e: expr) : nat :=
  match e with
  | Const _ => 1
same as S O
  | Var _ => 1
  | Add e1 e2 => esize e1 + esize e2
                 
same as plus (esize e1) (esize e2)
  | Mul e1 e2 => esize e1 + esize e2
  | Cmp e1 e2 => esize e1 + esize e2
  end.

and do proofs about programs
Lemma nconsts_le_size:
  forall e,
  nconsts e <= esize e.
Proof.
  intros.
  induction e.
  + simpl. auto.
auto will solve many simple goals
  + simpl. auto.
  + simpl. omega.
omega will solve many arithemetic goals
  + simpl. omega.
  + simpl. omega.
Qed.

that proof had a lot of copy-past :(
Lemma nconsts_le_size´:
  forall e,
  nconsts e <= esize e.
Proof.
  intros.
do induction, then on every resulting subgoal do simpl, then on every resulting subgoal do auto, then on every resulting subgoal do omega
  induction e; simpl; auto; omega.
note that after the auto, only the Add, Mul, and Cmp subgoals remain, but it's hard to tell since the proof does not "pause"
Qed.

Locate "<=".

take a second to consider <=
Print le.

it's a relation defined as an inductive predicate
we give rules for when the relation holds
we can define our own relations to encode properties of expressions

Inductive has_const : expr -> Prop :=
| hc_const :
    forall n, has_const (Const n)
| hc_add_l :
    forall e1 e2,
    has_const e1 ->
    has_const (Add e1 e2)
| hc_add_r :
    forall e1 e2,
    has_const e2 ->
    has_const (Add e1 e2)
| hc_mul_l :
    forall e1 e2,
    has_const e1 ->
    has_const (Mul e1 e2)
| hc_mul_r :
    forall e1 e2,
    has_const e2 ->
    has_const (Mul e1 e2)
| hc_cmp_l :
    forall e1 e2,
    has_const e1 ->
    has_const (Cmp e1 e2)
| hc_cmp_r :
    forall e1 e2,
    has_const e2 ->
    has_const (Cmp e1 e2).

Lemma add_mul_comm:
  (forall e1 e2, Add e1 e2 = Add e2 e1) ->
  False.
Proof.
  intros.
  specialize (H (Const 0) (Const 1)).
  inversion H.
Qed.

Inductive has_var : expr -> Prop :=
| hv_var :
    forall s, has_var (Var s)
| hv_add_l :
    forall e1 e2,
    has_var e1 ->
    has_var (Add e1 e2)
| hv_add_r :
    forall e1 e2,
    has_var e2 ->
    has_var (Add e1 e2)
| hv_mul_l :
    forall e1 e2,
    has_var e1 ->
    has_var (Mul e1 e2)
| hv_mul_r :
    forall e1 e2,
    has_var e2 ->
    has_var (Mul e1 e2)
| hv_cmp_l :
    forall e1 e2,
    has_var e1 ->
    has_var (Cmp e1 e2)
| hv_cmp_r :
    forall e1 e2,
    has_var e2 ->
    has_var (Cmp e1 e2).

we could also write boolean functions to check the same properties

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

the Bool library provides "||" as a notation for orb
Fixpoint hasVar (e: expr) : bool :=
  match e with
  | Const _ => false
  | Var _ => true
  | Add e1 e2 => hasVar e1 || hasVar e2
  | Mul e1 e2 => hasVar e1 || hasVar e2
  | Cmp e1 e2 => hasVar e1 || hasVar e2
  end.

That looks way easier! However, as the quarter progresses, we'll see that sometime defining a property as an inductive relation is more convenient
We can prove that our relational and functional versions agree
Lemma has_const_hasConst:
  forall e,
  has_const e ->
  hasConst e = true.
Proof.
  intros.
  induction e.
  + simpl. reflexivity.
  + simpl.
uh oh, trying to prove something false! it's OK though because we have a bogus hyp!
    inversion H.
inversion lets us do case analysis on how a hypothesis of an inductive type may have been built. In this case, there is no way to build a value of type "has_const (Var s)", so we complete the proof of this subgoal for all zero ways of building such a value
  +
here we use inversion to consider how a value of type "has_const (Add e1 e2)" could have been built
    inversion H.
    -
built with hc_add_l
      subst.
subst rewrites all equalities it can
      apply IHe1 in H1.
      simpl.
remember notation "||" is same as orb
      rewrite H1. simpl. reflexivity.
    -
built with hc_add_r
      subst. apply IHe2 in H1.
      simpl. rewrite H1.
use fact that orb is commutative
      simpl. rewrite orb_comm.
you can find this by turning on auto completion or using a search query
SearchAbout orb.
      simpl. reflexivity.
  +
Mul case is similar
    inversion H; simpl; subst.
    - apply IHe1 in H1; rewrite H1; auto.
    - apply IHe2 in H1; rewrite H1;
      rewrite orb_comm; auto.
  +
Cmp case is similar
    inversion H; simpl; subst.
    - apply IHe1 in H1; rewrite H1; auto.
    - apply IHe2 in H1; rewrite H1;
      rewrite orb_comm; auto.
Qed.

now the other direction
Lemma hasConst_has_const:
  forall e,
  hasConst e = true ->
  has_const e.
Proof.
  intros.
  induction e.
  +
    
we can prove this case with a constructor constructor.
    apply hc_const.
exact (hc_const n). this uses hc_const
  +
Uh oh, no constructor for has_const can possibly produce a value of our goal type! It's OK though because we have a bogus hypothesis.
    simpl in H.
    discriminate.
  +
now do Add case
    simpl in H.
either e1 or e2 had a Const
    apply orb_true_iff in H.
consider cases for H
    destruct H.
    -
e1 had a Const
      apply hc_add_l.
      apply IHe1.
      assumption.
    -
e2 had a Const
      apply hc_add_r.
      apply IHe2.
      assumption.
   +
Mul case is similar
     simpl in H; apply orb_true_iff in H; destruct H.
     -
constructor will just use hc_mul_l
       constructor. apply IHe1. assumption.
     -
constructor will screw up and try hc_mul_l again!
       constructor.
OOPS!
       Undo.
       apply hc_mul_r. apply IHe2. assumption.
   +
Cmp case is similar
     simpl in H; apply orb_true_iff in H; destruct H.
     - constructor; auto.
     - apply hc_cmp_r; auto.
Qed.

all that was only for the true cases! can also use not and do the false cases

Lemma not_has_const_hasConst:
  forall e,
  ~ has_const e ->
  hasConst e = false.
Proof.
  unfold not. intros.
  induction e.
  + simpl.
uh oh, trying to prove something bogus better exploit a bogus hypothesis
    exfalso.
proof by contradiction
    apply H. constructor.
  + simpl. reflexivity.
  + simpl. apply orb_false_iff.
prove conjunction by proving left and right
    split.
    - apply IHe1. intro.
      apply H. apply hc_add_l. assumption.
    - apply IHe2. intro.
      apply H. apply hc_add_r. assumption.
  +
Mul case is similar
    simpl; apply orb_false_iff.
    split.
    - apply IHe1; intro.
      apply H. apply hc_mul_l. assumption.
    - apply IHe2; intro.
      apply H. apply hc_mul_r. assumption.
  +
Cmp case is similar
    simpl; apply orb_false_iff.
    split.
    - apply IHe1; intro.
      apply H. apply hc_cmp_l. assumption.
    - apply IHe2; intro.
      apply H. apply hc_cmp_r. assumption.
Qed.

Lemma false_hasConst_hasConst:
  forall e,
  hasConst e = false ->
  ~ has_const e.
Proof.
  unfold not. intros.
  induction e;
    
crunch down everything in subgoals
    simpl in *.
  + discriminate.
  + inversion H0.
  + apply orb_false_iff in H.
get both proofs out of a conjunction by destructing it
    destruct H.
case analysis on H0 DISCUSS: how do we know to do this?
    inversion H0.
    - subst. auto.
auto will chain things for us
    - subst. auto.
  +
Mul case similar
    apply orb_false_iff in H; destruct H.
    inversion H0; subst; auto.
  +
Cmp case similar
    apply orb_false_iff in H; destruct H.
    inversion H0; subst; auto.
Qed.

we can stitch all these together

Lemma has_const_iff_hasConst:
  forall e,
  has_const e <-> hasConst e = true.
Proof.
  intros. split.
  +
  • >
    apply has_const_hasConst.
  +
<-
    apply hasConst_has_const.
Qed.

We can also do all the same sorts of proofs for has_var and hasVar

Lemma has_var_hasVar:
  forall e,
  has_var e ->
  hasVar e = true.
Proof.
TODO: try this without copying from above
Admitted.

Lemma hasVar_has_var:
  forall e,
  hasVar e = true ->
  has_var e.
Proof.
TODO: try this without copying from above
Admitted.

Lemma has_var_iff_hasVar:
  forall e,
  has_var e <-> hasVar e = true.
Proof.
TODO: try this without copying from above
Admitted.

we can also prove things about expressions
Lemma expr_bottoms_out:
  forall e,
  has_const e \/ has_var e.
Proof.
  intros. induction e.
  +
prove left side of disjunction
    left.
    constructor.
  +
prove right side of disjunction
    right.
    constructor.
  +
case analysis on IHe1
    destruct IHe1.
    - left. constructor. assumption.
    - right. constructor. assumption.
  +
Mul case similar
    destruct IHe1.
    - left. constructor. assumption.
    - right. constructor. assumption.
  +
Cmp case similar
    destruct IHe1.
    - left. constructor. assumption.
    - right. constructor. assumption.
Qed.

we could have gotten some of the has_const lemmas by being a little clever! (but then we wouldn't have learned as many tactics ;) )

Lemma has_const_hasConst´:
  forall e,
  has_const e ->
  hasConst e = true.
Proof.
  intros.
  induction H.
  + simpl. reflexivity.
  + simpl. rewrite orb_true_iff.
    left. assumption.
Admitted.
simpl; auto. + rewrite orb_true_iff. auto. + rewrite orb_true_iff. auto. + rewrite orb_true_iff. auto. + rewrite orb_true_iff. auto. + rewrite orb_true_iff. auto. + rewrite orb_true_iff. auto. Qed.
or even better
Lemma has_const_hasConst´´:
  forall e,
  has_const e ->
  hasConst e = true.
Proof.
  intros.
  induction H; simpl; auto;
    rewrite orb_true_iff; auto.
Qed.

Lemma not_has_const_hasConst´:
  forall e,
  ~ has_const e ->
  hasConst e = false.
Proof.
  unfold not; intros.
  destruct (hasConst e) eqn:?.
  - exfalso. apply H.
    apply hasConst_has_const; auto.
  - reflexivity.
Qed.

Lemma false_hasConst_hasConst´:
  forall e,
  hasConst e = false ->
  ~ has_const e.
Proof.
  unfold not; intros.
  destruct (hasConst e) eqn:?.
  - discriminate.
  - rewrite has_const_hasConst in Heqb.
NOTE: we got another subgoal!
    * discriminate.
    * assumption.
Qed.

In general:
  • relational defns are nice when you want to use inversion
  • functional defns are nice when you want to use simpl
This page has been generated by coqdoc