(* Prop is *p en Set is *s. Type is the box in Lambda C *)
Check Prop.
Check Set.

(* nat is the set of the natural numbers *)
Check nat.

Check 3.

Check plus.

Check (nat->(nat->nat)).

Check (plus 3).

(*
 Coq Notation:
   Lambda abstraction: fun x:A => M,
   Pi abstraction:     forall x:A, B   
*)

Check fun n:nat=>(plus n (S O)).

Check fun P:nat->Prop => forall x:nat, (P x) -> (P x).

(* implicit type assignments: *)

Check (fun x => plus x x).

Check (fun x=> x=3).

(* product types: the polymorphic identity *)

Check (fun (A:Set)(x:A)=>x).

(* Searching known results:*)

Check lt.

SearchAbout lt.

(* Useful first step: load collections of known facts and functions. *)

Require Import Arith. 

SearchAbout lt.

(* Warning: "SearchAbout <." does not work.  *)

SearchPattern (lt _ _).

SearchPattern (_ < _).

Check lt_S.

Print lt_S.

Check (lt_S 3).

Check (lt_S 3 1).

(* Declaration *)
Variable n: nat.

Hypothesis Pos_n: n>0.

(* Definition *)

Definition double:= fun x:nat => (plus x x).

Check double.

Print double.

(* Propositional logic: Prove A -> B -> A  *)

Goal forall A B:Prop, A->B->A.
intros A B H0 H1.
assumption.

Save ABA.

Print ABA.

(* Second-order definition of conjunction *)

Lemma Stupid: forall (A B:Prop), A -> B.
Proof.
Admitted.

Definition two := S (S 0).

Check two.

Lemma TwoIsTwo: two = S (S 0).
Proof.
unfold two.
reflexivity.
(* or, more generally: trivial. *)
Qed.

Lemma Example1: forall A B C:Prop, (A->B)->(B->C)->(A->C).
intros A B C.
intro.
intro.
intro.
apply H0.
apply H.
assumption.
Save.

Lemma Example2: 
 forall A:Set, 
 forall P:A->Prop,
 forall Q:A->Prop,
 forall c:forall x:A,(P x)->(Q x),
 forall d:forall x:A,(P x),
 forall (z:A), (Q z).
intros.
apply c.
apply d.
Save.

Print Example2.

Print and.

(* /\ is the infix notation for the predefined "and" *)
(* note the implicit `forall': *)

Lemma Example3 (A B:Prop): (A/\B) -> A.
Proof.
intros.
elim H.
apply ABA.
Qed.


Section InductiveDefinition.

Inductive List:Set:=
 nil:List |
 cons: nat->List ->List.


Fixpoint append(L:List):List->List:=
fun X:List =>
 match L with
  nil => X |
  (cons n M) => (cons n (append M X))
 end.

Lemma AppNil: forall L:List, (append L nil)=L.
induction L.
simpl.
trivial.
simpl.
rewrite IHL.
trivial.
Save.

Lemma App_Assoc: forall (L1 L2 L3:List), (append L1 (append L2 L3))=(append (append L1 L2) L3).
induction L1.
simpl.
trivial.

intros.
simpl.
rewrite IHL1.
trivial.
Save.


End InductiveDefinition.

Section CaseDistinctions.

(* Definitions using case distinctions *)

Check eq_nat_dec.

Definition CaseDist1: nat -> nat := 
fun n =>
( if (eq_nat_dec n two) then 0 else 1).

(* Another way of doing the same: *)

Definition CaseDist2: nat -> nat := 
fun n =>
match (eq_nat_dec n two) with
| left _ => 0
| right _ => 1
end.

Lemma Test: (CaseDist2 1) = 1.
unfold CaseDist2.
simpl.
reflexivity.
Save.

(* More complicated case distinction: *)

Check lt_eq_lt_dec.

(* this is a nested construction:

inleft _ : ( {n<m} + {n=m} )
inleft (left _ ): {n<m}
inleft (right _): {n=m}
inright _: {m<n}

This should clarify what the following definition does: *)

Definition CaseDist3: nat -> nat :=
fun n =>
match (lt_eq_lt_dec n 3) with
| inleft (left _) => 1
| inleft (right _) => 3
| inright _ => 5
end.

(* If we now Print the definition, we see an alternative way 
of doing the same, using "if-then": *)

Print CaseDist3.

Definition CaseDist3a: nat -> nat :=
fun n =>
match (lt_eq_lt_dec n 3)  with
|inleft s => (if  s then 1 else 3)
|inright _ => 5
end. 


End CaseDistinctions.