(**********************************************************) (* Definicje przez punkt staly *) Fixpoint plus [n:nat] : nat -> nat := [m:nat]Cases n of O => m | (S p) => (S (plus p m)) end. (* zdefiniuj mnozenie *) Fixpoint razy [n:nat] : nat -> nat := (* zdefiniowac recznie zasade indukcji: *) (* uzywajac (* nat_rec : (P:(nat->Set))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n) *) Fixpoint nat_rec [P:(nat->Set); o:(P O); s:((n:nat)(P n)->(P (S n))); n:nat] : (P n) := (* dowody przez indukcje *) Lemma plus_zero : (n:nat)(plus n O)=n. Lemma plus_S : (n,m:nat)(plus n (S m)) = (S (plus n m)). Lemma plus_przem : (n,m:nat)(plus n m) = (plus m n). (* Zdefiniuj plus' rekurencyjnie po drugim argumencie *) Fixpoint plus' .... Lemma plus_jak_plus : (n,m:nat)(plus n m)=(plus' n m). (* Funkcja Ackermanna ? *) (* Even Odd na dwa sposoby *) Inductive Even : nat -> Prop := evenO : (Even O) | evenSS : (n:nat)(Even n) -> (Even (S (S n))). Mutual Inductive Ev : nat -> Prop := | evO : (Ev O) | evS : (n:nat)(Odd n) -> (Ev (S n)) with Odd : nat -> Prop := | oddS : (n:nat)(Ev n) -> (Odd (S n)). Lemma Even_Ev : (n:nat) (Even n) -> (Ev n). (* w druga strone trudniejsze ... :( *) Lemma Ev_Even : (n:nat) (Even n) -> (Ev n). Inductive listn [A:Set] : nat -> Set := nnil : (listn A O) | ncons : A -> (n:nat) (listn A n) -> (listn A (S n)). (* zdefiniowac map na takich listach... *) Check mapn. mapn : (A,B:Set)(f:A->B)(n:nat)(listn A n) -> (listn B m) (* zdefiniowac append i udowodnic, ze map f (append l1 l2) = (append (map f l1) (map f l2)). *)