CPDT Exercise 4.6

gistfile1.txt

Section CPDT_Exercise_4_6.

(* problem 1 *)
Variable P Q R : Prop.

Goal (True \/ False) /\ (False \/ True).
Proof.
split; [ left | right ]; apply I.
Qed.

Goal P -> ~ ~ P.
Proof.
unfold not.
intros H H0.
apply H0.
assumption.
Qed.

Goal P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R).
Proof.
intro H.
destruct H as (H0, H1).
destruct H1 as [H2| H3];
 [left | right];
 split; assumption.
Qed.

(* problem 2 *)
Variable T : Set.
Variable x : T.
Variable p : T -> Prop.
Variable q : T -> T -> Prop.
Variable f : T -> T.

Goal p x ->
 (forall x, p x -> exists y, q x y) ->
  (forall x y, q x y -> q y (f y)) ->
   exists z, q z (f z).
Proof.
intros H H0 H1.
assert (exists y : T, q x y).
 apply H0.
 apply H.

 destruct H2.
 assert (q x0 (f x0));
  [apply (H1 x) | exists x0];
  assumption.
Qed.

(* problem 3 *)
Inductive mult6 : nat -> Prop :=
 | Mult6_0 : mult6 0
 | Mult6_S6 : forall n, mult6 n -> mult6 (6 + n).

Inductive mult10 : nat -> Prop :=
 | Mult10_0 : mult10 0
 | Mult10_S10 : forall n, mult10 n -> mult10 (10 + n).

Definition mult6or10 (n:nat) :=
 mult6 n \/ mult10 n.

Goal ~ mult6or10 13.
Proof.
unfold not.
inversion 1.
 inversion H;
  [ inversion H1 | inversion H0 ];
  inversion H3; inversion H5.

 inversion H0.
 inversion H2.
Qed.

Inductive odd : nat -> Prop :=
 | Odd1 : odd 1
 | OddSS : forall n, odd n -> odd (S (S n)).

Goal forall n, mult6or10 n -> ~ odd n.
Proof.
unfold mult6or10.
inversion 1; generalize H0; generalize n;
 [ refine (mult6_ind (fun n => ~ odd n) _ _)
 | refine (mult10_ind (fun n => ~ odd n) _ _) ];
 [ intro; inversion H1 | idtac | intro; inversion H1 | idtac ];
 intros; intro; inversion H3; inversion H5; inversion H7;
 [ idtac | inversion H9; inversion H11 ]; apply H2;
 assumption.
Qed.

End CPDT_Exercise_4_6.