(* G54DTP Dependently Typed Programming.
Inductive predicates and relations.
Venanzio Capretta, February 2011. *)
Require Import Arith.
(* Check the definitions and theorems in the standard library Arith. *)
(* Predicate stating that a number is even. *)
Inductive Even : nat -> Prop :=
evenO : Even O
| evenSS : forall n:nat, Even n -> Even (S (S n)).
Lemma even12: Even 12.
Proof.
apply evenSS.
apply evenSS.
apply evenSS.
apply evenSS.
apply evenSS.
apply evenSS.
exact evenO.
Qed.
(* We can avoid repeating the same tactic many times
by using the tactical "repeat".
*)
Lemma even12' : Even 12.
Proof.
repeat (apply evenSS).
exact evenO.
Qed.
Lemma twoTimesEven: forall n:nat, Even (n+n).
Proof.
intro n.
(* Elimination of a natural number: proof by induction. *)
elim n.
(* Base case. *)
exact evenO.
(* Inductive step. *)
intros n' IH.
rewrite <- plus_Snm_nSm.
(* The lemma plus_Snm_nSm states an equality,
the arrow <- specifies that we want to rewrite it from right to left.
*)
simpl.
apply evenSS.
exact IH.
Qed.
(* Predicate stating that a number is odd. *)
Inductive Odd: nat -> Prop :=
odd1 : Odd 1
| oddSS : forall n, Odd n -> Odd (S (S n)).
Lemma oddSeven: forall m, Odd m -> Even (S m).
Proof.
intros m H.
(* We do induction of the proof of (Odd m). *)
elim H.
(* Base case: the proof was odd1, so m=1. *)
apply evenSS; apply evenO. (* Semicolon: do the tactis in succession. *)
(* Inductive step: the proof was (oddSS m' Hm') for some m' and some
proof Hm': Odd m'; so m=(S (S m')).
*)
intros m' Hm' IH.
apply evenSS.
exact IH.
Qed.
Lemma evenSodd: forall m, Even m -> Odd (S m).
intros m h; elim h.
exact odd1.
intros m' h' IH; apply oddSS; exact IH.
Qed.
Lemma oddPlusOddEven: forall n, Odd n -> forall m, Odd m -> Even (n+m).
Proof.
intros n Hn.
(* We do induction on the proof of (Odd n). *)
elim Hn.
(* Base case: odd1, so n=1. *)
apply oddSeven.
(* Inductive step: oddSS n' Hn', so n=(S (S n')). *)
intros n' Hn' IH.
intros m Hm; simpl.
apply evenSS.
apply IH.
exact Hm.
Qed.
(* Even and odd numbers are already predefined
in the standard library using a mutual inductive definition.
*)
Require Import Even.
Print even.
(* Our definitions are equivalent to those in the library. *)
Lemma Even_even: forall n, Even n -> even n.
Proof.
intros n h; elim h.
exact even_O.
intros n' h' IH.
apply even_S.
apply odd_S.
exact IH.
Qed.
Lemma Odd_odd: forall n, Odd n -> odd n.
Proof.
intros n h; elim h.
apply odd_S; exact even_O.
intros n' h' IH; apply odd_S; apply even_S; exact IH.
Qed.
(* For the implication in the other direction we must do
mutual induction on even and odd.
This can't be done in an ordinary proof
but it can be done in a mutual fixpoint.
*)
Fixpoint even_Even (n:nat)(h: even n): Even n :=
match h in even n return Even n with
even_O => evenO
| even_S n' h' => oddSeven n' (odd_Odd n' h')
end
with odd_Odd (n:nat)(h:odd n): Odd n :=
match h with
odd_S n' h' => evenSodd n' (even_Even n' h')
end.