(** After this set of lectures you should know and be able to use the
following proof tactics:
* intros - introduce a hypothesis from [forall] or [A -> B]
* simpl - simplification
* reflexivity - simplification followed by applying reflexive law
* destruct - proof by cases
* rewrite - if [A=B] is known, replace [A] by [B] or [B] by [A]
* symmetry - Flip [A=B] to [B=A]
* omega - linear arithmetic solver. [Require Import Omega.] *)
Require Import Omega.
Module Days.
Inductive day : Type :=
| Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday
| Zigaday.
Definition next_weekday(d:day) : day :=
match d with
| Monday => Tuesday
| Tuesday => Wednesday
| Wednesday => Thursday
| Thursday => Friday
| Friday => Monday
| Saturday => Monday
| Sunday => Monday
| Zigaday => Monday
end.
(* Proof by simplification using [simpl] and [reflexivity] *)
Example ex1: next_weekday(Monday) = Tuesday.
Proof.
simpl. reflexivity.
Qed.
Print ex1.
(* Note that [reflexivity] calls [simpl] but you don't see what's
happening *)
Example ex1': next_weekday(Monday) = Tuesday.
Proof.
reflexivity.
Qed.
(* Example from last class period. Cases cannot be solved with [reflexivity].
must deal with a negation that [reflexivity] won't work with. *)
Example ex2: forall d, next_weekday d <> Sunday.
Proof.
intros d.
destruct d.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
simpl. unfold not. intros. inversion H.
Qed.
Print ex2.
(* Where we're headed - How I would do the proof. *)
Example ex2': forall d, next_weekday d <> Sunday.
Proof.
intros d; destruct d; discriminate.
Qed.
End Days.
Module AE.
Inductive AE : Type :=
| Const : nat -> AE
| Plus : AE -> AE -> AE
| Times : AE -> AE -> AE.
Fixpoint run(t:AE):nat :=
match t with
| Const n => n
| Plus l r => run l + run r
| Times l r => run l * run r
end.
(* Proof by simplification using [simpl] and [reflexivity]. *)
Example ex1: run (Const 3) = 3.
Proof.
simpl. reflexivity.
Qed.
Example ex2: run (Plus (Const 3) (Const 4)) = 7.
Proof.
simpl. reflexivity.
Qed.
Example ex3: run (Plus (Const 3) (Const 4)) = run (Const 3) + run (Const 4).
Proof.
reflexivity.
Qed.
(* Dealing with universally quantified variables using [intros] *)
Theorem plus_t1: forall l r, run (Plus l r) = (run l) + (run r).
Proof.
intros l r. reflexivity.
Qed.
(* Proof by rewriting using [rewrite] and hypothesis introduction. You
can read [->] as [implies]. If [t = r] is an assumption, then we can
rewrite [t] with [r] or [r] with [t]. *)
Theorem eq_symmetric : forall m n : AE,
m = n -> n = m.
Proof.
intros m n.
intros H.
rewrite -> H.
reflexivity.
Restart.
intros m n.
intros H.
rewrite <- H.
reflexivity.
Qed.
Theorem eq_trans : forall m n o : AE,
m = n -> o = n -> m = o.
Proof.
intros m n o.
intros H1 H2.
rewrite H1.
rewrite H2.
reflexivity.
Restart.
intros.
subst.
reflexivity.
Qed.
Theorem AE_trans : forall n m o : AE,
n = m -> m = o -> run n + run m = run m + run o.
Proof.
intros n m o.
intros H1 H2.
rewrite H1.
rewrite H2.
reflexivity.
Qed.
(* More rewriting to prove things about [run] *)
Theorem run_AE_trans : forall n m o : AE,
run n = run m -> run m = run o -> run n + run m = run m + run o.
Proof.
intros m n o.
intros H1 H2.
rewrite H1.
rewrite H2.
reflexivity.
Qed.
Theorem run_silly_theorem : forall n m:AE,
n = m -> run n + run n = run m + run m.
Proof.
intros n m.
intros H1.
rewrite H1.
reflexivity.
Qed.
(* [omega] is a handy linear arithmetic solver. You can work without it,
but no need to. *)
(* If addition is commutative, then so is [run] over [Plus] *)
Theorem Plus_commutative: forall n m, run (Plus n m) = run (Plus m n).
Proof.
intros n m.
simpl.
omega.
Qed.
(* A first taste of induction *)
Theorem plus_0: forall n, n=n+0.
Proof.
intros n.
induction n.
reflexivity.
simpl.
rewrite <- IHn.
reflexivity.
Qed.
(* Destruct again to prove an optimization *)
Theorem Plus_0: forall t, run t = run (Plus t (Const 0)).
Proof.
intros t.
destruct t; simpl; omega.
Qed.
(* plus_n_O *)
Theorem Plus_eval_0: forall t z, run z = 0 -> run (Plus t z) = run t.
Proof.
intros t z.
destruct t.
intros H. simpl. rewrite H. symmetry. apply plus_n_O.
intros H. simpl. rewrite H. symmetry. apply plus_n_O.
intros H. simpl. rewrite H. symmetry. apply plus_n_O.
Restart.
intros t z.
intros H.
simpl. rewrite H. omega.
Qed.
End AE.