Review (only in slide)
1 2 Theorem review2: ∀b, (orb true b) = true. Theorem review3: ∀b, (orb b true) = true.
Whether or not it can be just
simpl. depending on the definition of
In Proof Engineering, we probably won’t need to include
review2 but need to include
review3 in library.
Why we have
0 is a “neutral element” for
+ (additive identity)
0 + n = n
1 2 3 Theorem plus_O_n : forall n : nat, 0 + n = n. Proof. intros n. simpl. reflexivity. Qed.
This can be simply proved by simplication bcuz the definition of
+ is defined by pattern matching against 1st operand:
1 2 3 4 5 Fixpoint plus (n : nat) (m : nat) : nat := match n with | O ⇒ m | S n' ⇒ S (plus n' m) end.
We can observe that if
O), no matter
m is, it returns
m as is.
n + 0 = n
1st try: Simplication
1 2 3 4 5 Theorem plus_O_n_1 : forall n : nat, n + 0 = n. Proof. intros n. simpl. (* Does nothing! *) Abort.
This cannot be proved by simplication bcuz
n is unknown so unfold the definition
+ won’t be able to simplify anything.
2nd try: Case Analysis
1 2 3 4 5 6 7 8 9 Theorem plus_n_O_2 : ∀n:nat, n = n + 0. Proof. intros n. destruct n as [| n'] eqn:E. - (* n = 0 *) reflexivity. (* so far so good... *) - (* n = S n' *) simpl. (* ...but here we are stuck again *) Abort.
Our 2nd try is to use case analysis (
destruct), but the proof stucks in inductive case since
n can be infinitely large (destructed)
Induction to the resucue
To prove interesting facts about numbers, lists, and other inductively defined sets, we usually need a more powerful reasoning principle: induction.
Princeple of induction over natural numbers (i.e. mathematical induction)
1 P(0); ∀n' P(n') → P(S n') ====> P(n)
In Coq, like
P(n) into 2 subgoals:
1 2 3 4 5 Theorem plus_n_O : ∀n:nat, n = n + 0. Proof. intros n. induction n as [| n' IHn']. - (* n = 0 *) reflexivity. - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.
n - n = 0
1 2 3 4 5 6 7 8 9 Theorem minus_diag : ∀n, minus n n = 0. Proof. (* WORKED IN CLASS *) intros n. induction n as [| n' IHn']. - (* n = 0 *) simpl. reflexivity. - (* n = S n' *) simpl. rewrite → IHn'. reflexivity. Qed
Noticed that the definition of
1 2 3 4 5 6 Fixpoint minus (n m:nat) : nat := match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end.
rewrite would do a (DFS) preorder traversal in the syntax tree.