Check bool.
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.
(* elim b case b elim b *)
destruct b.
- 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 *)
Definition F(b:bool) :Prop :=
match b with
true => True
|false => False
end.
Lemma dist : ~ true = false.
Proof.
intro H.
change (F false).
rewrite <- H.
simpl.
auto.
Qed.
(* There is a simple tactic "congruence" that proves -- among other things -- that
distinct constructors of an inductive type are different: *)
Lemma dist' : ~ true = false.
Proof.
congruence.
Qed.
Print nat.
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.
(* 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.
(* 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)
*)
auto.
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.
*)
(* Illustrating that logical connectives are also defined as inductive types *)
Print True.
Print False.
Lemma False1 : forall A:Prop, False -> A.
Proof.
intros A HF.
(* 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.
(* OR: induction H.
case H.
elim H.*)
left.
exact H.
Qed.
Lemma triv2 :forall A B C :Prop, (A->C) \/ (B->C) -> A/\B -> C.
Proof.
intros A B C H1 H2.
destruct H1.
- destruct H2.
apply H; auto.
- apply H.
destruct H2.
auto.
Qed.