From: Ferruccio Guidi Date: Fri, 29 Feb 2008 18:13:10 +0000 (+0000) Subject: we added the classic substitution function X-Git-Tag: make_still_working~5571 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e44ebf8a8c659b408fa765d30faf1b8c8ff2adb0;p=helm.git we added the classic substitution function --- diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma index e89081ac9..559add969 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma @@ -26,6 +26,8 @@ include "LambdaDelta-1/cnt/defs.ma". include "LambdaDelta-1/cimp/defs.ma". +include "LambdaDelta-1/subst/defs.ma". + include "LambdaDelta-1/subst1/defs.ma". include "LambdaDelta-1/csubst1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma index e493455eb..b94953a5b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma @@ -25,6 +25,7 @@ alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con". alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con". alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con". alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". +alias id "lt_le_weak" = "cic:/Coq/Arith/Lt/lt_le_weak.con". alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con". alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con". alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". @@ -37,4 +38,5 @@ alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con". alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con". alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con". +alias id "pred_Sn" = "cic:/Coq/Init/Peano/pred_Sn.con". alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/defs.ma new file mode 100644 index 000000000..fbeebb984 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/defs.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "LambdaDelta-1/lift/defs.ma". + +definition subst: + nat \to (T \to (T \to T)) +\def + let rec subst (d: nat) (v: T) (t: T) on t: T \def (match t with [(TSort n) +\Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true +\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true +\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) | (THead k +u t0) \Rightarrow (THead k (subst d v u) (subst (s k d) v t0))]) in subst. + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/fwd.ma new file mode 100644 index 000000000..5fec959ab --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/fwd.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "LambdaDelta-1/subst/defs.ma". + +theorem subst_sort: + \forall (v: T).(\forall (d: nat).(\forall (k: nat).(eq T (subst d v (TSort +k)) (TSort k)))) +\def + \lambda (_: T).(\lambda (_: nat).(\lambda (k: nat).(refl_equal T (TSort +k)))). + +theorem subst_lref_lt: + \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt i d) \to (eq T +(subst d v (TLRef i)) (TLRef i))))) +\def + \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt i +d)).(eq_ind_r bool true (\lambda (b: bool).(eq T (match b with [true +\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true +\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) (TLRef i))) +(refl_equal T (TLRef i)) (blt i d) (lt_blt d i H))))). + +theorem subst_lref_eq: + \forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v))) +\def + \lambda (v: T).(\lambda (i: nat).(eq_ind_r bool false (\lambda (b: bool).(eq +T (match b with [true \Rightarrow (TLRef i) | false \Rightarrow (match b with +[true \Rightarrow (TLRef (pred i)) | false \Rightarrow (lift i O v)])]) (lift +i O v))) (refl_equal T (lift i O v)) (blt i i) (le_bge i i (le_n i)))). + +theorem subst_lref_gt: + \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt d i) \to (eq T +(subst d v (TLRef i)) (TLRef (pred i)))))) +\def + \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt d +i)).(eq_ind_r bool false (\lambda (b: bool).(eq T (match b with [true +\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true +\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) (TLRef +(pred i)))) (eq_ind_r bool true (\lambda (b: bool).(eq T (match b with [true +\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)]) (TLRef (pred +i)))) (refl_equal T (TLRef (pred i))) (blt d i) (lt_blt i d H)) (blt i d) +(le_bge d i (lt_le_weak d i H)))))). + +theorem subst_head: + \forall (k: K).(\forall (w: T).(\forall (u: T).(\forall (t: T).(\forall (d: +nat).(eq T (subst d w (THead k u t)) (THead k (subst d w u) (subst (s k d) w +t))))))) +\def + \lambda (k: K).(\lambda (w: T).(\lambda (u: T).(\lambda (t: T).(\lambda (d: +nat).(refl_equal T (THead k (subst d w u) (subst (s k d) w t))))))). + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/props.ma new file mode 100644 index 000000000..3797559a2 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/props.ma @@ -0,0 +1,110 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "LambdaDelta-1/subst/fwd.ma". + +include "LambdaDelta-1/subst0/defs.ma". + +include "LambdaDelta-1/lift/props.ma". + +theorem subst_lift_SO: + \forall (v: T).(\forall (t: T).(\forall (d: nat).(eq T (subst d v (lift (S +O) d t)) t))) +\def + \lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(eq +T (subst d v (lift (S O) d t0)) t0))) (\lambda (n: nat).(\lambda (d: +nat).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (subst d v t0) (TSort n))) +(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 (TSort n))) (refl_equal T +(TSort n)) (subst d v (TSort n)) (subst_sort v d n)) (lift (S O) d (TSort n)) +(lift_sort n (S O) d)))) (\lambda (n: nat).(\lambda (d: nat).(lt_le_e n d (eq +T (subst d v (lift (S O) d (TLRef n))) (TLRef n)) (\lambda (H: (lt n +d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (subst d v t0) (TLRef n))) +(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (TLRef n))) (refl_equal T +(TLRef n)) (subst d v (TLRef n)) (subst_lref_lt v d n H)) (lift (S O) d +(TLRef n)) (lift_lref_lt n (S O) d H))) (\lambda (H: (le d n)).(eq_ind_r T +(TLRef (plus n (S O))) (\lambda (t0: T).(eq T (subst d v t0) (TLRef n))) +(eq_ind nat (S (plus n O)) (\lambda (n0: nat).(eq T (subst d v (TLRef n0)) +(TLRef n))) (eq_ind_r T (TLRef (pred (S (plus n O)))) (\lambda (t0: T).(eq T +t0 (TLRef n))) (eq_ind nat (plus n O) (\lambda (n0: nat).(eq T (TLRef n0) +(TLRef n))) (f_equal nat T TLRef (plus n O) n (sym_eq nat n (plus n O) +(plus_n_O n))) (pred (S (plus n O))) (pred_Sn (plus n O))) (subst d v (TLRef +(S (plus n O)))) (subst_lref_gt v d (S (plus n O)) (le_n_S d (plus n O) +(le_plus_trans d n O H)))) (plus n (S O)) (plus_n_Sm n O)) (lift (S O) d +(TLRef n)) (lift_lref_ge n (S O) d H)))))) (\lambda (k: K).(\lambda (t0: +T).(\lambda (H: ((\forall (d: nat).(eq T (subst d v (lift (S O) d t0)) +t0)))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(eq T (subst d v +(lift (S O) d t1)) t1)))).(\lambda (d: nat).(eq_ind_r T (THead k (lift (S O) +d t0) (lift (S O) (s k d) t1)) (\lambda (t2: T).(eq T (subst d v t2) (THead k +t0 t1))) (eq_ind_r T (THead k (subst d v (lift (S O) d t0)) (subst (s k d) v +(lift (S O) (s k d) t1))) (\lambda (t2: T).(eq T t2 (THead k t0 t1))) +(f_equal3 K T T T THead k k (subst d v (lift (S O) d t0)) t0 (subst (s k d) v +(lift (S O) (s k d) t1)) t1 (refl_equal K k) (H d) (H0 (s k d))) (subst d v +(THead k (lift (S O) d t0) (lift (S O) (s k d) t1))) (subst_head k v (lift (S +O) d t0) (lift (S O) (s k d) t1) d)) (lift (S O) d (THead k t0 t1)) +(lift_head k t0 t1 (S O) d)))))))) t)). + +theorem subst_subst0: + \forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall (d: nat).((subst0 +d v t1 t2) \to (eq T (subst d v t1) (subst d v t2)))))) +\def + \lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (d: nat).(\lambda +(H: (subst0 d v t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t: +T).(\lambda (t0: T).(\lambda (t3: T).(eq T (subst n t t0) (subst n t t3)))))) +(\lambda (v0: T).(\lambda (i: nat).(eq_ind_r T (lift i O v0) (\lambda (t: +T).(eq T t (subst i v0 (lift (S i) O v0)))) (eq_ind nat (plus (S O) i) +(\lambda (n: nat).(eq T (lift i O v0) (subst i v0 (lift n O v0)))) (eq_ind T +(lift (S O) i (lift i O v0)) (\lambda (t: T).(eq T (lift i O v0) (subst i v0 +t))) (eq_ind_r T (lift i O v0) (\lambda (t: T).(eq T (lift i O v0) t)) +(refl_equal T (lift i O v0)) (subst i v0 (lift (S O) i (lift i O v0))) +(subst_lift_SO v0 (lift i O v0) i)) (lift (plus (S O) i) O v0) (lift_free v0 +i (S O) O i (le_n (plus O i)) (le_O_n i))) (S i) (refl_equal nat (S i))) +(subst i v0 (TLRef i)) (subst_lref_eq v0 i)))) (\lambda (v0: T).(\lambda (u2: +T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v0 u1 +u2)).(\lambda (H1: (eq T (subst i v0 u1) (subst i v0 u2))).(\lambda (t: +T).(\lambda (k: K).(eq_ind_r T (THead k (subst i v0 u1) (subst (s k i) v0 t)) +(\lambda (t0: T).(eq T t0 (subst i v0 (THead k u2 t)))) (eq_ind_r T (THead k +(subst i v0 u2) (subst (s k i) v0 t)) (\lambda (t0: T).(eq T (THead k (subst +i v0 u1) (subst (s k i) v0 t)) t0)) (eq_ind_r T (subst i v0 u2) (\lambda (t0: +T).(eq T (THead k t0 (subst (s k i) v0 t)) (THead k (subst i v0 u2) (subst (s +k i) v0 t)))) (refl_equal T (THead k (subst i v0 u2) (subst (s k i) v0 t))) +(subst i v0 u1) H1) (subst i v0 (THead k u2 t)) (subst_head k v0 u2 t i)) +(subst i v0 (THead k u1 t)) (subst_head k v0 u1 t i)))))))))) (\lambda (k: +K).(\lambda (v0: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (i: +nat).(\lambda (_: (subst0 (s k i) v0 t4 t3)).(\lambda (H1: (eq T (subst (s k +i) v0 t4) (subst (s k i) v0 t3))).(\lambda (u: T).(eq_ind_r T (THead k (subst +i v0 u) (subst (s k i) v0 t4)) (\lambda (t: T).(eq T t (subst i v0 (THead k u +t3)))) (eq_ind_r T (THead k (subst i v0 u) (subst (s k i) v0 t3)) (\lambda +(t: T).(eq T (THead k (subst i v0 u) (subst (s k i) v0 t4)) t)) (eq_ind_r T +(subst (s k i) v0 t3) (\lambda (t: T).(eq T (THead k (subst i v0 u) t) (THead +k (subst i v0 u) (subst (s k i) v0 t3)))) (refl_equal T (THead k (subst i v0 +u) (subst (s k i) v0 t3))) (subst (s k i) v0 t4) H1) (subst i v0 (THead k u +t3)) (subst_head k v0 u t3 i)) (subst i v0 (THead k u t4)) (subst_head k v0 u +t4 i)))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda +(i: nat).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0 +u1) (subst i v0 u2))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4: +T).(\lambda (_: (subst0 (s k i) v0 t3 t4)).(\lambda (H3: (eq T (subst (s k i) +v0 t3) (subst (s k i) v0 t4))).(eq_ind_r T (THead k (subst i v0 u1) (subst (s +k i) v0 t3)) (\lambda (t: T).(eq T t (subst i v0 (THead k u2 t4)))) (eq_ind_r +T (THead k (subst i v0 u2) (subst (s k i) v0 t4)) (\lambda (t: T).(eq T +(THead k (subst i v0 u1) (subst (s k i) v0 t3)) t)) (eq_ind_r T (subst i v0 +u2) (\lambda (t: T).(eq T (THead k t (subst (s k i) v0 t3)) (THead k (subst i +v0 u2) (subst (s k i) v0 t4)))) (eq_ind_r T (subst (s k i) v0 t4) (\lambda +(t: T).(eq T (THead k (subst i v0 u2) t) (THead k (subst i v0 u2) (subst (s k +i) v0 t4)))) (refl_equal T (THead k (subst i v0 u2) (subst (s k i) v0 t4))) +(subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4)) +(subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1 +t3 i))))))))))))) d v t1 t2 H))))). + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma index b996dc365..3f5d5414d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma @@ -16,6 +16,8 @@ include "LambdaDelta-1/subst0/tlt.ma". +include "LambdaDelta-1/subst/props.ma". + include "LambdaDelta-1/tau1/cnt.ma". include "LambdaDelta-1/ex0/props.ma".