(* In Coq, propositions are of type Prop, which means they are types. *)
(* Data-types are of type Type or Set, which means they are also types *)
(* The differences between Prop, Set and Type will be made clear later *)
(* ex 1 *)
Definition easy : forall P : Prop, P -> P := ...
Print easy.
(* In Coq, -> is just a particular case of forall *)
Check forall n : nat, True.
(* Minimal logic *)
Parameter A B C : Prop.
(* Prove *)
A -> A
(A -> B) -> (B -> C) -> A -> C
A -> B -> A
(A -> B -> C) -> (A -> B) -> A -> C
(* Negation : remember ~A is an abrevation for A -> False *)
(* Prove the following, possibly using False_ind *)
A -> ~~A
(A -> B) -> (~B -> ~A)
~~(~~A -> A).
(* forall quantification *)
(forall x, P x -> Q x) -> (forall x, P x) -> (forall x, Q x).
(forall x, P x -> Q x) -> (forall x, Q x -> R x) -> (forall x, P x -> R x)
(forall x , P x -> P (f x)) -> (forall x, P x -> P (f(f x)))
(forall x, P x -> Q x) -> ~Q c -> ~(forall x, P x)
(* existantial quantification *)
Check ex_intro.
Definition al_ex : forall A : Type, forall P : A -> Prop,
A -> (forall x, P x) -> (exists x, P x) := ...
Definition ex_al : forall A : Type, forall P : A -> Prop,
~(exists x, P x) -> forall x, ~(P x) := ...
(* Induction / recursion *)
Definition half x y := x=y+y \/ x = S (y+y).
Definition d (x:nat) := exists y,half x y.
(* advanced : do the following without tactics ! *)
(* for now, just use it *)
Lemma dS : forall x, d x -> d(S x).
Proof.
intros x dx.
destruct dx as [y [ey|ey]].
exists y; right.
rewrite ey; trivial.
exists (S y); left.
rewrite <- plus_n_Sm, ey.
simpl; trivial.
Defined.
Definition d0 : (d 0) :=
(* Use nat_ind for the following *)
Definition div2 (x:nat) : (d x) :=
Eval compute in (div2 3).
Check I.
(* Try to understand the following *)
Definition divide (x:nat) : exists y:nat, True :=
(@ex_ind nat (half x) (exists y:nat, True)
(fun x p => (ex_intro _ x I)) (div2 x)).
Eval compute in (divide 251).