Library inductive_examples
Check bool.
Print bool.
Check bool_ind.
Definition neg (b : bool) : bool :=
match b with
true => false
| false => true
end.
Print neg.
Print bool.
Check bool_ind.
Definition neg (b : bool) : bool :=
match b with
true => false
| false => true
end.
Print neg.
There is some useful syntactic sugar for the type bool
Definition negg (b : bool) := if b then false else true.
Print negg.
Lemma bool1 : forall b : bool, neg (neg b) = b.
Proof.
intro b.
destruct b.
Print negg.
Lemma bool1 : forall b : bool, neg (neg b) = b.
Proof.
intro b.
destruct b.
or elim b or case b
- simpl. reflexivity.
- simpl. reflexivity.
- simpl. reflexivity.
or chain the last 5 lines into
destruct b; simpl; reflexivity.
Qed.
Distinct constructors of an inductive type are different:
true and false are different
There is a simple tactic congruence that proves -- among other things -- that distinct constructors of an inductive type are different:
There is a simple tactic congruence that proves -- among other things -- that distinct constructors of an inductive type are different:
Natural Numbers
Print nat.
Print plus.
Print plus.
To define plus, we would type the following
Fixpoint plus' (n m : nat) {struct n} : nat :=
match n with
| O => m
| S p => S (plus' p m)
end.
Print plus'.
Lemma nat1 : forall n : nat, plus n 0 = n.
Proof.
intro n.
induction n.
match n with
| O => m
| S p => S (plus' p m)
end.
Print plus'.
Lemma nat1 : forall n : nat, plus n 0 = n.
Proof.
intro n.
induction n.
Also try destruct n and notice it doesn't work:
destruct only does a case analysis, but doesn't give you an induction hypothesis
- simpl.
reflexivity.
- simpl.
rewrite IHn.
reflexivity.
Qed.
Print plus.
Lemma nat2 : forall n : nat, plus 0 n = n.
Proof.
simpl.
reflexivity.
- simpl.
rewrite IHn.
reflexivity.
Qed.
Print plus.
Lemma nat2 : forall n : nat, plus 0 n = n.
Proof.
simpl.
Note: this works because plus is defined by recursion
over the first argument:
plus 0 n = n
plus (S m) n = S(plus m n)
plus 0 n = n
plus (S m) n = S(plus m n)
auto.
Qed.
Qed.
Exercise 1:
(a) Define plus'' by recursion over the second argument
(b) Prove forall n : nat, plus'' n 0 = n by a simple script as in Lemma nat2
Example of a WRONG Fixpoint definition!
Try to feed this to Coq
Fixpoint f (n : nat) {struct n} : nat :=
match n with
0 => 0
| S p => f (f p)
end.
Logical connectives are also defined as inductive types
(a) Define plus'' by recursion over the second argument
(b) Prove forall n : nat, plus'' n 0 = n by a simple script as in Lemma nat2
contradiction.
destruct HF.
Qed.
Check False_ind.
Print and.
Check and_ind.
Print or.
Check or_ind.
Lemma triv1 :forall A B :Prop, A /\ B -> A\/B.
Proof.
intros A B.
intro H.
destruct H.
Qed.
Check False_ind.
Print and.
Check and_ind.
Print or.
Check or_ind.
Lemma triv1 :forall A B :Prop, A /\ B -> A\/B.
Proof.
intros A B.
intro H.
destruct H.
or induction H. or
case H. or
elim H.