some improvements in the anticipator

- we anticipate the terms to be matched
- we do not anticipate inner fixpoints because we turn them into constants when we generate Grafite for the ng_kernel

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
index 0ebbb480abbb2c0cda16bb14fb67f4245468bcb8..ba88961f44ab57e7514f069b08a3cdf51ca9062d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
@@ -19,11 +19,11 @@ include "basic_1/tlist/defs.ma".
 include "basic_1/s/defs.ma".
 
 let rec lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match t with 
-[(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (let TMP_4 \def 
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)]) in 
-(TLRef TMP_4)) | (THead k u t0) \Rightarrow (let TMP_1 \def (lref_map f d u) 
-in (let TMP_2 \def (s k d) in (let TMP_3 \def (lref_map f TMP_2 t0) in (THead 
-k TMP_1 TMP_3))))].
+[(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (let TMP_4 \def (blt 
+i d) in (let TMP_5 \def (match TMP_4 with [true \Rightarrow i | false 
+\Rightarrow (f i)]) in (TLRef TMP_5))) | (THead k u t0) \Rightarrow (let 
+TMP_1 \def (lref_map f d u) in (let TMP_2 \def (s k d) in (let TMP_3 \def 
+(lref_map f TMP_2 t0) in (THead k TMP_1 TMP_3))))].
 
 definition lift:
  nat \to (nat \to (T \to T))

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/fwd.ma
index 11d21eb535737388ac6db694277714bdd8be122f..9c625c76c804efe35a7b7165b69c4962eee6675c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/fwd.ma
@@ -1232,7 +1232,7 @@ h d t) in (let TMP_6 \def (lifts h d t0) in (let TMP_7 \def (TCons TMP_5
 TMP_6) in (let H1 \def (eq_ind TList TNil TMP_4 I TMP_7 H0) in (let TMP_8 
 \def (TCons t t0) in (let TMP_9 \def (eq TList TNil TMP_8) in (False_ind 
 TMP_9 H1)))))))))))))) in (TList_ind TMP_2 TMP_3 TMP_10 ts))))) in (let 
-TMP_53 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (ts: 
+TMP_52 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (ts: 
 TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d t0) (lifts h 
 d ts)) \to (eq TList t0 ts))))))).(\lambda (ts: TList).(let TMP_13 \def 
 (\lambda (t1: TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h 
@@ -1244,29 +1244,28 @@ TMP_14 \def (lift h d t) in (let TMP_15 \def (lifts h d t0) in (let TMP_16
 with [TNil \Rightarrow False | (TCons _ _) \Rightarrow True])) in (let H1 
 \def (eq_ind TList TMP_16 TMP_17 I TNil H0) in (let TMP_18 \def (TCons t t0) 
 in (let TMP_19 \def (eq TList TMP_18 TNil) in (False_ind TMP_19 H1))))))))))) 
-in (let TMP_52 \def (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_: 
+in (let TMP_51 \def (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_: 
 ((\forall (h: nat).(\forall (d: nat).((eq TList (TCons (lift h d t) (lifts h 
 d t0)) (lifts h d t2)) \to (eq TList (TCons t t0) t2)))))).(\lambda (h: 
 nat).(\lambda (d: nat).(\lambda (H1: (eq TList (TCons (lift h d t) (lifts h d 
 t0)) (TCons (lift h d t1) (lifts h d t2)))).(let TMP_27 \def (\lambda (e: 
-TList).(match e with [TNil \Rightarrow (let TMP_25 \def lref_map in (let 
-TMP_26 \def (\lambda (x: nat).(plus x h)) in (TMP_25 TMP_26 d t))) | (TCons 
-t3 _) \Rightarrow t3])) in (let TMP_28 \def (lift h d t) in (let TMP_29 \def 
-(lifts h d t0) in (let TMP_30 \def (TCons TMP_28 TMP_29) in (let TMP_31 \def 
-(lift h d t1) in (let TMP_32 \def (lifts h d t2) in (let TMP_33 \def (TCons 
-TMP_31 TMP_32) in (let H2 \def (f_equal TList T TMP_27 TMP_30 TMP_33 H1) in 
-(let TMP_37 \def (\lambda (e: TList).(match e with [TNil \Rightarrow (let 
-TMP_36 \def lifts in (TMP_36 h d t0)) | (TCons _ t3) \Rightarrow t3])) in 
-(let TMP_38 \def (lift h d t) in (let TMP_39 \def (lifts h d t0) in (let 
-TMP_40 \def (TCons TMP_38 TMP_39) in (let TMP_41 \def (lift h d t1) in (let 
-TMP_42 \def (lifts h d t2) in (let TMP_43 \def (TCons TMP_41 TMP_42) in (let 
-H3 \def (f_equal TList TList TMP_37 TMP_40 TMP_43 H1) in (let TMP_51 \def 
-(\lambda (H4: (eq T (lift h d t) (lift h d t1))).(let TMP_46 \def (\lambda 
-(t3: T).(let TMP_44 \def (TCons t t0) in (let TMP_45 \def (TCons t3 t2) in 
-(eq TList TMP_44 TMP_45)))) in (let TMP_47 \def (refl_equal T t) in (let 
-TMP_48 \def (H t2 h d H3) in (let TMP_49 \def (f_equal2 T TList TList TCons t 
-t t0 t2 TMP_47 TMP_48) in (let TMP_50 \def (lift_inj t t1 h d H4) in (eq_ind 
-T t TMP_46 TMP_49 t1 TMP_50))))))) in (TMP_51 H2)))))))))))))))))))))))) in 
-(TList_ind TMP_13 TMP_20 TMP_52 ts)))))))) in (TList_ind TMP_1 TMP_11 TMP_53 
-xs)))).
+TList).(match e with [TNil \Rightarrow (let TMP_26 \def (\lambda (x: 
+nat).(plus x h)) in (lref_map TMP_26 d t)) | (TCons t3 _) \Rightarrow t3])) 
+in (let TMP_28 \def (lift h d t) in (let TMP_29 \def (lifts h d t0) in (let 
+TMP_30 \def (TCons TMP_28 TMP_29) in (let TMP_31 \def (lift h d t1) in (let 
+TMP_32 \def (lifts h d t2) in (let TMP_33 \def (TCons TMP_31 TMP_32) in (let 
+H2 \def (f_equal TList T TMP_27 TMP_30 TMP_33 H1) in (let TMP_36 \def 
+(\lambda (e: TList).(match e with [TNil \Rightarrow (lifts h d t0) | (TCons _ 
+t3) \Rightarrow t3])) in (let TMP_37 \def (lift h d t) in (let TMP_38 \def 
+(lifts h d t0) in (let TMP_39 \def (TCons TMP_37 TMP_38) in (let TMP_40 \def 
+(lift h d t1) in (let TMP_41 \def (lifts h d t2) in (let TMP_42 \def (TCons 
+TMP_40 TMP_41) in (let H3 \def (f_equal TList TList TMP_36 TMP_39 TMP_42 H1) 
+in (let TMP_50 \def (\lambda (H4: (eq T (lift h d t) (lift h d t1))).(let 
+TMP_45 \def (\lambda (t3: T).(let TMP_43 \def (TCons t t0) in (let TMP_44 
+\def (TCons t3 t2) in (eq TList TMP_43 TMP_44)))) in (let TMP_46 \def 
+(refl_equal T t) in (let TMP_47 \def (H t2 h d H3) in (let TMP_48 \def 
+(f_equal2 T TList TList TCons t t t0 t2 TMP_46 TMP_47) in (let TMP_49 \def 
+(lift_inj t t1 h d H4) in (eq_ind T t TMP_45 TMP_48 t1 TMP_49))))))) in 
+(TMP_50 H2)))))))))))))))))))))))) in (TList_ind TMP_13 TMP_20 TMP_51 
+ts)))))))) in (TList_ind TMP_1 TMP_11 TMP_52 xs)))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/props.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/props.ma
index 97cd58e0ea385afc7221109be6e59778430e2899..6adeada0c74be488605997e746239fb183f0fe37 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/props.ma
@@ -121,28 +121,27 @@ t1))).(\lambda (P: Prop).(let TMP_14 \def (\lambda (e: T).(match e with
 \def (THead k0 t0 t1) in (let TMP_21 \def (lift h d TMP_20) in (let TMP_22 
 \def (THead k v TMP_21) in (let TMP_23 \def (THead k0 t0 t1) in (let H3 \def 
 (f_equal T T TMP_19 TMP_22 TMP_23 H1) in (let TMP_54 \def (\lambda (e: 
-T).(match e with [(TSort _) \Rightarrow (let TMP_43 \def lref_map in (let 
-TMP_44 \def (\lambda (x: nat).(plus x h)) in (let TMP_45 \def (TMP_43 TMP_44 
-d t0) in (let TMP_50 \def lref_map in (let TMP_51 \def (\lambda (x: 
-nat).(plus x h)) in (let TMP_52 \def (s k0 d) in (let TMP_53 \def (TMP_50 
-TMP_51 TMP_52 t1) in (THead k0 TMP_45 TMP_53)))))))) | (TLRef _) \Rightarrow 
-(let TMP_28 \def lref_map in (let TMP_29 \def (\lambda (x: nat).(plus x h)) 
-in (let TMP_30 \def (TMP_28 TMP_29 d t0) in (let TMP_35 \def lref_map in (let 
-TMP_36 \def (\lambda (x: nat).(plus x h)) in (let TMP_37 \def (s k0 d) in 
-(let TMP_38 \def (TMP_35 TMP_36 TMP_37 t1) in (THead k0 TMP_30 TMP_38)))))))) 
-| (THead _ _ t2) \Rightarrow t2])) in (let TMP_55 \def (THead k0 t0 t1) in 
-(let TMP_56 \def (lift h d TMP_55) in (let TMP_57 \def (THead k v TMP_56) in 
-(let TMP_58 \def (THead k0 t0 t1) in (let H4 \def (f_equal T T TMP_54 TMP_57 
-TMP_58 H1) in (let TMP_70 \def (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K 
-k k0)).(let TMP_59 \def (\lambda (k1: K).(\forall (v0: T).(\forall (h0: 
-nat).(\forall (d0: nat).((eq T (THead k1 v0 (lift h0 d0 t1)) t1) \to (\forall 
-(P0: Prop).P0)))))) in (let H7 \def (eq_ind K k TMP_59 H0 k0 H6) in (let 
-TMP_60 \def (THead k0 t0 t1) in (let TMP_61 \def (lift h d TMP_60) in (let 
-TMP_62 \def (\lambda (t2: T).(eq T t2 t1)) in (let TMP_63 \def (lift h d t0) 
-in (let TMP_64 \def (s k0 d) in (let TMP_65 \def (lift h TMP_64 t1) in (let 
-TMP_66 \def (THead k0 TMP_63 TMP_65) in (let TMP_67 \def (lift_head k0 t0 t1 
-h d) in (let H8 \def (eq_ind T TMP_61 TMP_62 H4 TMP_66 TMP_67) in (let TMP_68 
-\def (lift h d t0) in (let TMP_69 \def (s k0 d) in (H7 TMP_68 h TMP_69 H8 
+T).(match e with [(TSort _) \Rightarrow (let TMP_44 \def (\lambda (x: 
+nat).(plus x h)) in (let TMP_45 \def (lref_map TMP_44 d t0) in (let TMP_51 
+\def (\lambda (x: nat).(plus x h)) in (let TMP_52 \def (s k0 d) in (let 
+TMP_53 \def (lref_map TMP_51 TMP_52 t1) in (THead k0 TMP_45 TMP_53)))))) | 
+(TLRef _) \Rightarrow (let TMP_29 \def (\lambda (x: nat).(plus x h)) in (let 
+TMP_30 \def (lref_map TMP_29 d t0) in (let TMP_36 \def (\lambda (x: 
+nat).(plus x h)) in (let TMP_37 \def (s k0 d) in (let TMP_38 \def (lref_map 
+TMP_36 TMP_37 t1) in (THead k0 TMP_30 TMP_38)))))) | (THead _ _ t2) 
+\Rightarrow t2])) in (let TMP_55 \def (THead k0 t0 t1) in (let TMP_56 \def 
+(lift h d TMP_55) in (let TMP_57 \def (THead k v TMP_56) in (let TMP_58 \def 
+(THead k0 t0 t1) in (let H4 \def (f_equal T T TMP_54 TMP_57 TMP_58 H1) in 
+(let TMP_70 \def (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let 
+TMP_59 \def (\lambda (k1: K).(\forall (v0: T).(\forall (h0: nat).(\forall 
+(d0: nat).((eq T (THead k1 v0 (lift h0 d0 t1)) t1) \to (\forall (P0: 
+Prop).P0)))))) in (let H7 \def (eq_ind K k TMP_59 H0 k0 H6) in (let TMP_60 
+\def (THead k0 t0 t1) in (let TMP_61 \def (lift h d TMP_60) in (let TMP_62 
+\def (\lambda (t2: T).(eq T t2 t1)) in (let TMP_63 \def (lift h d t0) in (let 
+TMP_64 \def (s k0 d) in (let TMP_65 \def (lift h TMP_64 t1) in (let TMP_66 
+\def (THead k0 TMP_63 TMP_65) in (let TMP_67 \def (lift_head k0 t0 t1 h d) in 
+(let H8 \def (eq_ind T TMP_61 TMP_62 H4 TMP_66 TMP_67) in (let TMP_68 \def 
+(lift h d t0) in (let TMP_69 \def (s k0 d) in (H7 TMP_68 h TMP_69 H8 
 P)))))))))))))))) in (let TMP_71 \def (TMP_70 H3) in (TMP_71 
 H2))))))))))))))))))))))))))))))) in (T_ind TMP_1 TMP_7 TMP_13 TMP_72 t)))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
index 77e5025dd1cd88f8d38e554dfb6d40c459105cf6..adade462b7a18f289fd32c92408449a91c3e93c0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "basic_1/lift/fwd.ma".
+include "basic_1/lift/props.ma".
 
 include "basic_1/tlt/props.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
index 83e2b707e840a53fc175f6cc1b813a5185382897..a9223f1b14f63fea039caaf1cfbf3f9d7ec2a245 100644 (file)
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
@@ -77,8 +77,8 @@ theorem eq_ind_r:
 (\forall (y: A).((eq A y x) \to (P y))))))
 \def
  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda 
-(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) 
-with [refl_equal \Rightarrow H])))))).
+(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(let TMP_1 \def (sym_eq 
+A y x H0) in (match TMP_1 with [refl_equal \Rightarrow H]))))))).
 
 theorem trans_eq:
  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A