(* ------------------------------------------------------------- *)
Section EX.

Variables (A:Set) (P : A->Prop).
Variable Q:Prop.

Lemma trivial : forall x:A, P x -> P x.
Proof.
intros.
assumption.
Qed.

Print trivial.

Lemma example : forall x:A, (Q -> Q -> P x) -> Q -> P x.
Proof.
intros x H H0.
apply H.
assumption.
assumption.
Qed.

Print example.

End EX.

Print trivial.
Print example.

(* ------------------------------------------------------------- *)

Print nat.
Print nat_rect.
Check nat_ind.
Check nat_rec.


(* RECURSIVE FUNCTIONS ON NAT *)

(* The double of a number *)
Definition double : nat -> nat := 
  nat_rec (fun _=>nat) 0 (fun x y => S (S y)). 

(* performs evaluation of an expression
   strategy: lazy evaluation;  reductions: delta, beta and iota *)
Eval lazy delta beta iota in (double 7).


(* "Eval compute" is equivalent to "Eval cbv delta beta iota zeta" *)
Eval compute in (double (S (S (S 0)))).
Eval compute in (double 8).


(* USING Fixpoint and case analysis*)
Fixpoint double' (n :nat) : nat := 
  match n with 
  | O => 0 
  | S x => S (S (double' x))
  end. 


(* Using predefined operations on nat *)
Definition double'' (x:nat) : nat := 2 * x.

(*performs evaluation of an expression
  strategy: call-by-value;  reductions: delta*)
Eval cbv delta [double''] in (double'' 22).

Eval compute in (double'' 22).

(* ------------------------------------------------------------- *)


(* INDUCTIVE PREDICATES *)


(* A property (predicate) on natural numbers *)
Inductive Even : nat -> Prop :=
| Even_base : Even 0
| Even_step : forall n, Even n -> Even (S (S n)).



Lemma de : forall n:nat, Even (double n).
Proof.
induction n.
simpl.
apply Even_base.
simpl.
apply Even_step.
assumption.
Qed.