(**********************************************************) Print nat_rect. Print nat_rec. Print nat_ind. (* dowody przez indukcje *) Locate "+". Print plus. Lemma plus_zero : forall n, n+0=n. Lemma plus_przem : forall n m, n+m = m+n. (* Zdefiniuj plus' rekurencyjnie po drugim argumencie *) Fixpoint plus' .... Lemma plus_jak_plus : forall n m, plus n m = plus' n m. * Funkcja Ackermanna ? *) (* ack O m = S m ack (S n) O = ack n (S O) ack (S n) (S m) = ack n (ack (S n) m) *) (* podpowiedź: co trzeba zrobic z ack n zeby dostac ack (S n) ? *) (* zdefiniować to przekształcenie *) (* 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 ... :) *) Lemma Ev_Even : forall n, Even n -> Ev n. Inductive listn (A:Set) : nat -> Set := nnil : listn A O | ncons : A -> forall n, listn A n -> listn A (S n). (* zdefiniowac map na takich listach... *) 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)). *)