X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FBase.ma;h=09d3ada50fc55570726e49ea2c6ce49688dd89cc;hb=ff31975b5e8899efaa9bd6daa236e12a8b62611f;hp=940eb118db20ceb60ee7067762c4861e2ea8dc93;hpb=96d82149c75cb82a8f4ceea9f1686cec36cebf76;p=helm.git diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma index 940eb118d..09d3ada50 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma @@ -16,157 +16,5 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base". -include "legacy/coq.ma". - -axiom insert_eq: \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: Prop).(((\forall (y: S).((P y) \to ((eq S y x) \to G)))) \to ((P x) \to G))))) . - -axiom unintro: \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x: A).(P x))) \to (P a)))) . - -axiom xinduction: \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x: A).((eq A t x) \to (P x)))) \to (P t)))) . - -axiom nat_dec: \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to (\forall (P: Prop).P)))) . - -axiom simpl_plus_r: \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) (plus p n)) \to (eq nat m p)))) . - -axiom minus_plus_r: \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m)) . - -axiom plus_permute_2_in_3: \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x y) z) (plus (plus x z) y)))) . - -axiom plus_permute_2_in_3_assoc: \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n h) k) (plus n (plus k h))))) . - -axiom plus_O: \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat x O) (eq nat y O)))) . - -axiom minus_Sx_SO: \forall (x: nat).(eq nat (minus (S x) (S O)) x) . - -axiom eq_nat_dec: \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j))) . - -axiom neq_eq_e: \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) \to P)) \to ((((eq nat i j) \to P)) \to P)))) . - -axiom le_false: \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P)))) . - -axiom le_Sx_x: \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P)) . - -axiom minus_le: \forall (x: nat).(\forall (y: nat).(le (minus x y) x)) . - -axiom le_plus_minus_sym: \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) n)))) . - -axiom le_minus_minus: \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) \to (le (minus y x) (minus z x)))))) . - -axiom le_minus_plus: \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat (minus (plus x y) z) (plus (minus x z) y))))) . - -axiom le_minus: \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to (le x (minus z y))))) . - -axiom le_trans_plus_r: \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to (le y z)))) . - -axiom le_gen_S: \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: nat).(eq nat x (S n))) (\lambda (n: nat).(le m n))))) . - -axiom lt_x_plus_x_Sy: \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y)))) . - -axiom simpl_lt_plus_r: \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m p)) \to (lt n m)))) . - -axiom minus_x_Sy: \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S (minus x (S y)))))) . - -axiom lt_plus_minus: \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus y (S x))))))) . - -axiom lt_plus_minus_r: \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y (S x)) x))))) . - -axiom minus_x_SO: \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O))))) . - -axiom le_x_pred_y: \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y)))) . - -axiom lt_le_minus: \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O))))) . - -axiom lt_le_e: \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) \to ((((le d n) \to P)) \to P)))) . - -axiom lt_eq_e: \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) \to ((((eq nat x y) \to P)) \to ((le x y) \to P))))) . - -axiom lt_eq_gt_e: \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P))))) . - -axiom lt_gen_xS: \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n)))))) . - -axiom le_lt_false: \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: Prop).P)))) . - -axiom lt_neq: \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y)))) . - -axiom arith0: \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2)))))) . - -axiom O_minus: \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O))) . - -axiom minus_minus: \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y)))))) . - -axiom plus_plus: \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1))))))))) . - -axiom ex2_sym: \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A (\lambda (x: A).(Q x)) (\lambda (x: A).(P x)))))) . - -inductive and3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def -| and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))). - -inductive or3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def -| or3_intro0: P0 \to (or3 P0 P1 P2) -| or3_intro1: P1 \to (or3 P0 P1 P2) -| or3_intro2: P2 \to (or3 P0 P1 P2). - -inductive or4 (P0:Prop) (P1:Prop) (P2:Prop) (P3:Prop): Prop \def -| or4_intro0: P0 \to (or4 P0 P1 P2 P3) -| or4_intro1: P1 \to (or4 P0 P1 P2 P3) -| or4_intro2: P2 \to (or4 P0 P1 P2 P3) -| or4_intro3: P3 \to (or4 P0 P1 P2 P3). - -inductive ex3 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop): Prop \def -| ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 P0 P1 P2)))). - -inductive ex4 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop) (P3:A0 \to Prop): Prop \def -| ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0) \to (ex4 A0 P0 P1 P2 P3))))). - -inductive ex_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)): Prop \def -| ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1 P0))). - -inductive ex2_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)): Prop \def -| ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to (ex2_2 A0 A1 P0 P1)))). - -inductive ex3_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)) (P2:A0 \to (A1 \to Prop)): Prop \def -| ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))). - -inductive ex4_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)) (P2:A0 \to (A1 \to Prop)) (P3:A0 \to (A1 \to Prop)): Prop \def -| ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))). - -inductive ex_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to (ex_3 A0 A1 A2 P0)))). - -inductive ex2_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))). - -inductive ex3_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1 P2)))))). - -inductive ex4_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))) (P3:A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 A1 A2 P0 P1 P2 P3))))))). - -inductive ex3_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def -| ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))). - -inductive ex4_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3:A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def -| ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))). - -inductive ex4_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def -| ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3))))))))). - -inductive ex5_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def -| ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))). - -inductive ex6_6 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))): Prop \def -| ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))). - -inductive ex6_7 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set) (A6:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))): Prop \def -| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5))))))))))))). - -definition blt: nat \to (nat \to bool) \def let rec blt (m: nat) (n: nat): bool \def (match n with [O \Rightarrow false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0) \Rightarrow (blt m0 n0)])]) in blt. - -axiom lt_blt: \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true))) . - -axiom le_bge: \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false))) . - -axiom blt_lt: \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x))) . - -axiom bge_le: \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y))) . +include "Base/theory.ma".