- Level-1: added some problems

- legacy: some now aliases

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
index e68fc505e0c26cba51bbb29f7740dd34346002fd..6142b4272a0cfe7be424ca03430a6399dd03bfef 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma
@@ -26,7 +26,7 @@ theorem xinduction: \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))
 
 axiom nat_dec: \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to (\forall (P: Prop).P)))) .
 
-theorem 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)))) \def \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat (plus m n) (plus p n))).(plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n p)) (plus m n) H) (plus n m) (plus_comm n m)))))).
+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)))) .
 
 theorem minus_plus_r: \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m)) \def \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_comm m n))).
 
@@ -34,15 +34,15 @@ theorem plus_permute_2_in_3: \forall (x: nat).(\forall (y: nat).(\forall (z: nat
 
 theorem 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))))) \def \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc n k h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
 
-theorem plus_O: \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (and (eq nat x O) (eq nat y O)))) \def \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to (and (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to (and (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (n0: nat).((eq nat n0 O) \to (and (eq nat (S n) O) (eq nat y O)))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (and (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
+axiom plus_O: \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat x O) (eq nat y O)))) .
 
-theorem minus_Sx_SO: \forall (x: nat).(eq nat (minus (S x) (S O)) x) \def \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal nat x) (minus x O) (minus_n_O x)).
+axiom minus_Sx_SO: \forall (x: nat).(eq nat (minus (S x) (S O)) x) .
 
-theorem eq_nat_dec: \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j))) \def \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) (\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or (not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda (H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H n0)))) j)))) i).
+axiom eq_nat_dec: \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j))) .
 
 theorem 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)))) \def \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
 
-theorem le_false: \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P)))) \def \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to P)) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to P) H3)) H1))]) in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to P)) with [le_n \Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m H2) \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m) \to P) H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
+axiom le_false: \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P)))) .
 
 theorem le_Sx_x: \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P)) \def \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def le_Sn_n in (False_ind P (H0 x H))))).
 
@@ -50,15 +50,15 @@ theorem minus_le: \forall (x: nat).(\forall (y: nat).(le (minus x y) x)) \def \l
 
 theorem le_plus_minus_sym: \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) n)))) \def \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) (plus (minus m n) n) (plus_comm (minus m n) n)))).
 
-theorem 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)))))) \def \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: nat).(\lambda (H0: (le y z)).(plus_le_reg_l x (minus y x) (minus z x) (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
+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)))))) .
 
-theorem 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))))) \def \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H return (\lambda (n: nat).((eq nat n x) \to (\forall (y: nat).(eq nat (minus (plus x y) O) (plus (minus x O) y))))) with [le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
+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))))) .
 
 theorem le_minus: \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to (le x (minus z y))))) \def \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x y))))).
 
 theorem le_trans_plus_r: \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to (le y z)))) \def \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
 
-theorem 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))))) \def \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def (match H return (\lambda (n: nat).((eq nat n x) \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m n0))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1 H0))]) in (H0 (refl_equal nat x))))).
+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))))) .
 
 theorem lt_x_plus_x_Sy: \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y)))) \def \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_comm x (S y)))).
 

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
index b396b4481bd4cd54af3c88e3f1cd5139f1cda3c3..80fcb3d4b945b7301cf1885486b6757c3b8aae93 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems".
 
 include "legacy/coq.ma".
 
-(* Problem 1: disambiguation/typechecking seems not to terminate *)
+(* Problem 1: disambiguation/typechecking very slow *)
 
 (*  - the "match" on "e" seems to be at the heart of the problem
  *  - all declararations are on "net" except the one of "e"
@@ -45,3 +45,59 @@ theorem nat_dec_real:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to (\forall (P: Prop).P))))
 \def  
  \lambda (n1: nat).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2: nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall (P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P: Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n) ((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match ee return Prop with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P: Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match (e:nat) return nat with [O \Rightarrow n | (S n) \Rightarrow n])) (S n) (S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n0: nat).((eq nat n n0) \to (\forall (P: Prop).P))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
+
+(* Problem 3: big problems with letins *)
+
+theorem 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))))
+\def
+ \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat (plus m n) (plus p n))).(plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n p)) (plus m n) H) (plus n m) (plus_comm n m)))))).
+
+(* Problem 4: very slow and big problems with letins *)
+
+theorem plus_O:
+ \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat x O) (eq nat y O))))
+\def
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus n y) O) \to ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) \to ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq nat (plus (S n) y) O)).(let H1 \def (match H0 return (\lambda (n0: nat).((eq nat n0 O) \to ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat (S n) O) (eq nat y O)))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((cic:/Coq/Init/Logic/and.ind#xpointer(1/1)) (eq nat (S n) O) (eq nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
+
+(* Problem 5: slow and problems with letins *)
+
+theorem minus_Sx_SO:
+ \forall (x: nat).(eq nat (minus (S x) (S O)) x)
+\def
+ \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal nat x) (minus x O) (minus_n_O x)).
+
+(* Problem 6: disambiguation problems *)
+
+theorem eq_nat_dec:
+ \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
+\def
+ \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) (\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or (not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda (H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H n0)))) j)))) i).
+
+(* Problem 7: very slow *)
+
+theorem le_false:
+ \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P))))
+\def
+ \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to P)) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to P) H3)) H1))]) in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to P)) with [le_n \Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m H2) \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m) \to P) H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
+
+(* Problem 8: disambiguation problems *)
+
+theorem 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))))))
+\def
+ \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: nat).(\lambda (H0: (le y z)).(plus_le_reg_l x (minus y x) (minus z x) (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
+
+(* Problem 9: very slow and disambiguation problems *)
+
+theorem 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)))))
+\def
+ \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H return (\lambda (n: nat).((eq nat n x) \to (\forall (y: nat).(eq nat (minus (plus x y) O) (plus (minus x O) y))))) with [le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def (match H0 return (\lambda (n: nat).((eq nat n O) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return Prop with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n H1) y))))) x)))) z).
+
+(* Problem 10: disambiguation problems *)
+
+theorem 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)))))
+\def
+ \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def (match H return (\lambda (n: nat).((eq nat n x) \to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m n0))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat (S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1 H0))]) in (H0 (refl_equal nat x))))).

diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma
index 0f5384697ae7d1498f78aaed191080abaad2f46c..092a11c6ae3e7e38c7c6c083e55dc7a5c554ac56 100644 (file)
--- a/helm/software/matita/library/legacy/coq.ma
+++ b/helm/software/matita/library/legacy/coq.ma
@@ -81,6 +81,10 @@ interpretation "Coq's natural 'not less or equal than'"
 alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
+alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
+alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
 
 (* theorems *)