(* Rownosc *)

Print eq.

(* x=x dla x:A to skrot od (eq A x x) *)

(* Dowodzenie rownosci . *)

Lemma re : forall (A:Set) (x:A), x=x.


Lemma true_albo_false : forall b:bool, b=true \/ b=false.


(* Uzywanie rownosci *)

Lemma Leibniz : forall (A:Set)(x y:A), x=y -> forall (P:A->Prop), (P x) -> (P y).


Lemma eq_trans: forall (A:Set) (x y z:A), x=y->y=z->x=z.


Lemma f_funkcja : forall (A B:Set)(f:A->B)(x y:A), x=y -> (f x)=(f y).


(*************nat******)
     
Print nat.

Check nat_rect.

Print nat_ind.

Print nat_rec.

Lemma zero_lub_nie_zero : forall n, n=O \/ n=(S (pred n)).

(**********************************************************)

(* Definicje przez punkt staly *)

Fixpoint plus (n m:nat) {struct n} : nat :=
   match n with
    | O   => m
    | S p => S (plus p m)
   end.


(* zdefiniuj mnozenie *)

Fixpoint razy 


(* zdefiniowac recznie zasade indukcji: *)
(* uzywajac Fixpoint i match *)
(*
nat_rec
     : forall P : nat->Prop, P O -> (forall n:nat, P n -> P (S n)) -> forall n:nat, P n 
*)
Fixpoint nat_rec 


(* dowody przez indukcje *)

Lemma plus_zero : forall (n:nat),(plus n O)=n.

Lemma plus_S:  forall (n m:nat), (plus n (S m)) = S (plus n m). 


Lemma plus_przem : forall (n m:nat), (plus n m) = (plus m n).


(* Zdefiniuj plus' rekurencyjnie po drugim argumencie *)

Fixpoint plus' 

Lemma plus_jak_plus : forall n m, plus n m = plus' n m.

(* Even Odd na dwa sposoby *)

Inductive Even : nat -> Prop :=
   evenO : Even O
 | evenSS : forall n:nat, Even n -> Even (S (S n)).

Inductive Ev : nat -> Prop :=
 | evO : Ev O
 | evS : forall n:nat, Odd n -> Ev (S n)
with Odd : nat -> Prop :=
 | oddS : forall n:nat, Ev n -> Odd (S n).

Lemma Even_Ev : forall n, Even n -> Ev n.


(* i w druga strone ... :) *)


Scheme Ev_i := Induction for Ev Sort Prop
    with Odd_i := Induction for Odd Sort Prop.

Check Ev_i. 

Lemma Ev_Even : forall n, Ev n -> Even n.

Lemma not_even_1: ~Even 1.


Inductive listn (A:Set) : nat -> Set :=
  nnil : listn A O
| ncons : A -> forall n, listn A n -> listn A (S n).


(*zdefiniuj dlugosc listy*) 
Fixpoint lenght 

 
Lemma dlugosc_sie_zgadza: forall (A: Set)(n:nat)(l:listn A n), lenght A n l = n.


(*dlugosc zero ma tylko nil

Lemma dlugosc_zero: forall (A: Set)(n:nat)(l:listn A n), lenght A n l = 0 -> l=(nnil A).
*)


(* zdefiniowac map na takich listach... *)

Fixpoint mapn 

Check mapn.

(* mapn : forall (A B:Set) (f:A->B) (n:nat), listn A n -> listn B n *)


(* zdefiniowac append i udowodnic, ze 
  map f (append l1 l2) = (append (map f l1) (map f l2)).

*)

Fixpoint append