From 24b593925bae7964bdc61e28408d389e5a74bd7a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 6 Feb 2015 19:40:26 +0000 Subject: [PATCH] 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 --- .../contribs/lambdadelta/basic_1/lift/defs.ma | 10 ++--- .../contribs/lambdadelta/basic_1/lift/fwd.ma | 43 +++++++++---------- .../lambdadelta/basic_1/lift/props.ma | 43 +++++++++---------- .../contribs/lambdadelta/basic_1/lift/tlt.ma | 2 +- .../lambdadelta/legacy_1/coq/props.ma | 4 +- 5 files changed, 50 insertions(+), 52 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma index 0ebbb480a..ba88961f4 100644 --- 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 11d21eb53..9c625c76c 100644 --- 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 97cd58e0e..6adeada0c 100644 --- 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 77e5025dd..adade462b 100644 --- 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 83e2b707e..a9223f1b1 100644 --- 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 -- 2.39.2