(* Lambda termy - liczby naturalne Churcha *) Definition NAT := Definition zero : NAT := Definition one : NAT := Definition two : NAT := Definition three : NAT := Definition succ : NAT -> NAT := Definition plus : NAT -> NAT -> NAT := Definition plus' : NAT -> NAT -> NAT := Definition times : NAT -> NAT -> NAT := Definition times' : NAT -> NAT -> NAT := Definition ack : NAT -> NAT -> NAT := Eval Compute in (ack three three). (* Najprostsze dowody *) Parameters A B C:Prop. Lemma identycznosc : A -> A. Lemma przyklad : ((A->B)->C)->B->C. Lemma przyk2 : (A->B->C)->A->(A->B)->C. Lemma przyk3 : A -> (B->C) -> (A->B) -> C. (* kodowanie impredykatywne w polimorficznym rach. lambda *) Definition FALSE := Definition NOT := fun A:Prop => Lemma true : (NOT FALSE). Lemma FALSE_all : forall A:Prop, FALSE -> A. Definition AND := fun A B:Prop => ... Definition AND_intro : Lemma And_commute: forall A B:Prop, AND A B -> AND B A. Definition OR := fun A B:Prop => ... Definition OR_intro_l : Definition OR_intro_r : Lemma OR_commute : forall A B : Prop, OR A B -> OR B A. Lemma And_or : forall A B:Prop, AND A B -> OR A B. Lemma or_not_not_and : forall A B:Prop, OR (NOT A) (NOT B) -> NOT (AND A B). Lemma and_not_not_or : forall A B:Prop, AND (NOT A) (NOT B) -> NOT (OR A B). Lemma przyk4 : forall A B C:Prop, AND (A->C) (B->C)) -> ((AND A B) -> C). (* Zbiory *) Parameter U : Type. Definition SET := U -> Prop. Definition elt : U -> SET -> Prop := fun u S => S u. Definition included : SET -> SET -> Prop := Definition empty : SET -> Prop := Definition full : SET -> Prop := Definition union : SET -> SET -> SET := Definition inter : SET -> SET -> SET := Definition compl : SET -> SET := Definition disjoint : SET -> SET -> Prop := Definition equal : SET -> SET -> Prop := Lemma Empty_Included: forall E:SET, (empty E) -> forall A:SET, (included E A). Theorem Union_commutative : forall A B: SET, (equal (union A B) (union B A)). Theorem Union_associative : forall A B C: SET, (equal (union (union A B) C) (union A (union B C))). Theorem Union_idempotent : forall A: SET, (included (union A A) A). Lemma Union_absorbs : forall A B: SET, (included B A) -> (included (union A B) A). Theorem Distributivity : forall A B C: SET, (equal (inter A (union B C)) (union (inter A B) (inter A C))). (* Wiecej: *) (* Empty neutralny dla Union, *) (* A,B included in (union A B) *) (* A rozl z C, B rozl z C, to (union A B) i (inter A B) tez *) (* A rozl z B, to przeciecie dopelnien niepuste *)