(* Lambda termy *) 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 *) Reset Initial. Definition FALSE := Definition NOT := [A:Prop] Lemma true : (NOT FALSE). Lemma FALSE_all : (A:Prop) FALSE -> A. Definition AND := [A,B:Prop] ... Definition AND_intro : Lemma And_commute: (A,B:Prop) (AND A B) -> (AND B A). Definition OR := [A,B:Prop] ... Definition OR_intro_l : Definition OR_intro_r : Lemma OR_commute : (A,B : Prop)(OR A B) -> (OR B A). Lemma And_or : (A,B:Prop)(AND A B) -> (OR A B). Lemma or_not_not_and : (A,B:Prop)(OR (NOT A) (NOT B)) -> (NOT (AND A B)). Lemma and_not_not_or : (A,B:Prop)(AND (NOT A) (NOT B)) -> (NOT (OR A B)). Lemma przyk4 : (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 := [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: (E:SET) (empty E) -> (A:SET) (included E A). Theorem Union_commutative : (A,B: SET) (equal (union A B) (union B A)). Theorem Union_associative : (A, B, C: SET) (equal (union (union A B) C) (union A (union B C))). Theorem Union_idempotent : (A: SET) (included (union A A) A). Lemma Union_absorbs : (A, B: SET) (included B A) -> (included (union A B) A). Theorem Distributivity : (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 *)