From: Ferruccio Guidi Date: Wed, 6 Sep 2006 14:45:44 +0000 (+0000) Subject: dependences fixed X-Git-Tag: 0.4.95@7852~1074 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=260615773f01b051db400034a8df7c578fe53718;p=helm.git dependences fixed --- diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma index f1b0a886c..4e37576d2 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma @@ -135,6 +135,7 @@ alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con". alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con". +alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con". theorem f_equal: \forall A,B:Type. \forall f:A \to B. \forall x,y:A. x = y \to f x = f y. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/sequent_viewer.xml b/matita/contribs/LAMBDA-TYPES/Level-1/Base/sequent_viewer.xml new file mode 100644 index 000000000..6aab4a1c5 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/sequent_viewer.xml @@ -0,0 +1,2 @@ + +p:natn:natm:natH:p+n≤p+mnat diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma index 55d6153a8..fa3d9c061 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma @@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs". include "C/defs.ma". +include "s/defs.ma". + definition clen: C \to nat \def diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma index 685b59683..a33870137 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma @@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props". include "cnt/defs.ma". -include "lift/defs.ma". +include "lift/fwd.ma". theorem cnt_lift: \forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma index aedcf4a3a..aa283e8f4 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma @@ -20,6 +20,8 @@ include "C/defs.ma". include "lift/defs.ma". +include "r/defs.ma". + inductive drop: nat \to (nat \to (C \to (C \to Prop))) \def | drop_refl: \forall (c: C).(drop O O c c) | drop_drop: \forall (k: K).(\forall (h: nat).(\forall (c: C).(\forall (e: diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma index 3b7907d2d..d9578d9f3 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma @@ -16,10 +16,12 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props". -include "drop/defs.ma". +include "drop/fwd.ma". include "lift/props.ma". +include "r/props.ma". + theorem drop_skip_bind: \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma new file mode 100644 index 000000000..164dab30a --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs". + +include "drop/defs.ma". + +include "lift1/defs.ma". + +inductive drop1: PList \to (C \to (C \to Prop)) \def +| drop1_nil: \forall (c: C).(drop1 PNil c c) +| drop1_cons: \forall (c1: C).(\forall (c2: C).(\forall (h: nat).(\forall (d: +nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: PList).((drop1 hds +c2 c3) \to (drop1 (PCons h d hds) c1 c3)))))))). + +definition ctrans: + PList \to (nat \to (T \to T)) +\def + let rec ctrans (hds: PList) on hds: (nat \to (T \to T)) \def (\lambda (i: +nat).(\lambda (t: T).(match hds with [PNil \Rightarrow t | (PCons h d hds0) +\Rightarrow (let j \def (trans hds0 i) in (let u \def (ctrans hds0 i t) in +(match (blt j d) with [true \Rightarrow (lift h (minus d (S j)) u) | false +\Rightarrow u])))]))) in ctrans. + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma new file mode 100644 index 000000000..2e1f964ed --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma @@ -0,0 +1,162 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props". + +include "drop1/defs.ma". + +include "drop/props.ma". + +theorem drop1_skip_bind: + \forall (b: B).(\forall (e: C).(\forall (hds: PList).(\forall (c: +C).(\forall (u: T).((drop1 hds c e) \to (drop1 (Ss hds) (CHead c (Bind b) +(lift1 hds u)) (CHead e (Bind b) u))))))) +\def + \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(PList_ind (\lambda (p: +PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) +(CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u)))))) (\lambda (c: +C).(\lambda (u: T).(\lambda (H: (drop1 PNil c e)).(let H0 \def (match H in +drop1 return (\lambda (p: PList).(\lambda (c0: C).(\lambda (c1: C).(\lambda +(_: (drop1 p c0 c1)).((eq PList p PNil) \to ((eq C c0 c) \to ((eq C c1 e) \to +(drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u))))))))) with +[(drop1_nil c0) \Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H1: +(eq C c0 c)).(\lambda (H2: (eq C c0 e)).(eq_ind C c (\lambda (c1: C).((eq C +c1 e) \to (drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u)))) (\lambda +(H3: (eq C c e)).(eq_ind C e (\lambda (c: C).(drop1 PNil (CHead c (Bind b) u) +(CHead e (Bind b) u))) (drop1_nil (CHead e (Bind b) u)) c (sym_eq C c e H3))) +c0 (sym_eq C c0 c H1) H2)))) | (drop1_cons c1 c2 h d H0 c3 hds H1) +\Rightarrow (\lambda (H2: (eq PList (PCons h d hds) PNil)).(\lambda (H3: (eq +C c1 c)).(\lambda (H4: (eq C c3 e)).((let H5 \def (eq_ind PList (PCons h d +hds) (\lambda (e0: PList).(match e0 in PList return (\lambda (_: PList).Prop) +with [PNil \Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H2) +in (False_ind ((eq C c1 c) \to ((eq C c3 e) \to ((drop h d c1 c2) \to ((drop1 +hds c2 c3) \to (drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u)))))) +H5)) H3 H4 H0 H1))))]) in (H0 (refl_equal PList PNil) (refl_equal C c) +(refl_equal C e)))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: +PList).(\lambda (H: ((\forall (c: C).(\forall (u: T).((drop1 p c e) \to +(drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) +u))))))).(\lambda (c: C).(\lambda (u: T).(\lambda (H0: (drop1 (PCons n n0 p) +c e)).(let H1 \def (match H0 in drop1 return (\lambda (p0: PList).(\lambda +(c0: C).(\lambda (c1: C).(\lambda (_: (drop1 p0 c0 c1)).((eq PList p0 (PCons +n n0 p)) \to ((eq C c0 c) \to ((eq C c1 e) \to (drop1 (PCons n (S n0) (Ss p)) +(CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))))))) with +[(drop1_nil c0) \Rightarrow (\lambda (H1: (eq PList PNil (PCons n n0 +p))).(\lambda (H2: (eq C c0 c)).(\lambda (H3: (eq C c0 e)).((let H4 \def +(eq_ind PList PNil (\lambda (e0: PList).(match e0 in PList return (\lambda +(_: PList).Prop) with [PNil \Rightarrow True | (PCons _ _ _) \Rightarrow +False])) I (PCons n n0 p) H1) in (False_ind ((eq C c0 c) \to ((eq C c0 e) \to +(drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) +(CHead e (Bind b) u)))) H4)) H2 H3)))) | (drop1_cons c1 c2 h d H1 c3 hds H2) +\Rightarrow (\lambda (H3: (eq PList (PCons h d hds) (PCons n n0 p))).(\lambda +(H4: (eq C c1 c)).(\lambda (H5: (eq C c3 e)).((let H6 \def (f_equal PList +PList (\lambda (e0: PList).(match e0 in PList return (\lambda (_: +PList).PList) with [PNil \Rightarrow hds | (PCons _ _ p) \Rightarrow p])) +(PCons h d hds) (PCons n n0 p) H3) in ((let H7 \def (f_equal PList nat +(\lambda (e0: PList).(match e0 in PList return (\lambda (_: PList).nat) with +[PNil \Rightarrow d | (PCons _ n _) \Rightarrow n])) (PCons h d hds) (PCons n +n0 p) H3) in ((let H8 \def (f_equal PList nat (\lambda (e0: PList).(match e0 +in PList return (\lambda (_: PList).nat) with [PNil \Rightarrow h | (PCons n +_ _) \Rightarrow n])) (PCons h d hds) (PCons n n0 p) H3) in (eq_ind nat n +(\lambda (n1: nat).((eq nat d n0) \to ((eq PList hds p) \to ((eq C c1 c) \to +((eq C c3 e) \to ((drop n1 d c1 c2) \to ((drop1 hds c2 c3) \to (drop1 (PCons +n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) +u))))))))) (\lambda (H9: (eq nat d n0)).(eq_ind nat n0 (\lambda (n1: +nat).((eq PList hds p) \to ((eq C c1 c) \to ((eq C c3 e) \to ((drop n n1 c1 +c2) \to ((drop1 hds c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind +b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)))))))) (\lambda (H10: (eq +PList hds p)).(eq_ind PList p (\lambda (p0: PList).((eq C c1 c) \to ((eq C c3 +e) \to ((drop n n0 c1 c2) \to ((drop1 p0 c2 c3) \to (drop1 (PCons n (S n0) +(Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))))) +(\lambda (H11: (eq C c1 c)).(eq_ind C c (\lambda (c0: C).((eq C c3 e) \to +((drop n n0 c0 c2) \to ((drop1 p c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) +(CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)))))) (\lambda +(H12: (eq C c3 e)).(eq_ind C e (\lambda (c0: C).((drop n n0 c c2) \to ((drop1 +p c2 c0) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 +(lift1 p u))) (CHead e (Bind b) u))))) (\lambda (H13: (drop n n0 c +c2)).(\lambda (H14: (drop1 p c2 e)).(drop1_cons (CHead c (Bind b) (lift n n0 +(lift1 p u))) (CHead c2 (Bind b) (lift1 p u)) n (S n0) (drop_skip_bind n n0 c +c2 H13 b (lift1 p u)) (CHead e (Bind b) u) (Ss p) (H c2 u H14)))) c3 (sym_eq +C c3 e H12))) c1 (sym_eq C c1 c H11))) hds (sym_eq PList hds p H10))) d +(sym_eq nat d n0 H9))) h (sym_eq nat h n H8))) H7)) H6)) H4 H5 H1 H2))))]) in +(H1 (refl_equal PList (PCons n n0 p)) (refl_equal C c) (refl_equal C +e)))))))))) hds))). + +theorem drop1_cons_tail: + \forall (c2: C).(\forall (c3: C).(\forall (h: nat).(\forall (d: nat).((drop +h d c2 c3) \to (\forall (hds: PList).(\forall (c1: C).((drop1 hds c1 c2) \to +(drop1 (PConsTail hds h d) c1 c3)))))))) +\def + \lambda (c2: C).(\lambda (c3: C).(\lambda (h: nat).(\lambda (d: +nat).(\lambda (H: (drop h d c2 c3)).(\lambda (hds: PList).(PList_ind (\lambda +(p: PList).(\forall (c1: C).((drop1 p c1 c2) \to (drop1 (PConsTail p h d) c1 +c3)))) (\lambda (c1: C).(\lambda (H0: (drop1 PNil c1 c2)).(let H1 \def (match +H0 in drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: +C).(\lambda (_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c1) \to ((eq +C c0 c2) \to (drop1 (PCons h d PNil) c1 c3)))))))) with [(drop1_nil c) +\Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H2: (eq C c +c1)).(\lambda (H3: (eq C c c2)).(eq_ind C c1 (\lambda (c0: C).((eq C c0 c2) +\to (drop1 (PCons h d PNil) c1 c3))) (\lambda (H4: (eq C c1 c2)).(eq_ind C c2 +(\lambda (c0: C).(drop1 (PCons h d PNil) c0 c3)) (drop1_cons c2 c3 h d H c3 +PNil (drop1_nil c3)) c1 (sym_eq C c1 c2 H4))) c (sym_eq C c c1 H2) H3)))) | +(drop1_cons c0 c4 h0 d0 H1 c5 hds H2) \Rightarrow (\lambda (H3: (eq PList +(PCons h0 d0 hds) PNil)).(\lambda (H4: (eq C c0 c1)).(\lambda (H5: (eq C c5 +c2)).((let H6 \def (eq_ind PList (PCons h0 d0 hds) (\lambda (e: PList).(match +e in PList return (\lambda (_: PList).Prop) with [PNil \Rightarrow False | +(PCons _ _ _) \Rightarrow True])) I PNil H3) in (False_ind ((eq C c0 c1) \to +((eq C c5 c2) \to ((drop h0 d0 c0 c4) \to ((drop1 hds c4 c5) \to (drop1 +(PCons h d PNil) c1 c3))))) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList +PNil) (refl_equal C c1) (refl_equal C c2))))) (\lambda (n: nat).(\lambda (n0: +nat).(\lambda (p: PList).(\lambda (H0: ((\forall (c1: C).((drop1 p c1 c2) \to +(drop1 (PConsTail p h d) c1 c3))))).(\lambda (c1: C).(\lambda (H1: (drop1 +(PCons n n0 p) c1 c2)).(let H2 \def (match H1 in drop1 return (\lambda (p0: +PList).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop1 p0 c c0)).((eq +PList p0 (PCons n n0 p)) \to ((eq C c c1) \to ((eq C c0 c2) \to (drop1 (PCons +n n0 (PConsTail p h d)) c1 c3)))))))) with [(drop1_nil c) \Rightarrow +(\lambda (H2: (eq PList PNil (PCons n n0 p))).(\lambda (H3: (eq C c +c1)).(\lambda (H4: (eq C c c2)).((let H5 \def (eq_ind PList PNil (\lambda (e: +PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil +\Rightarrow True | (PCons _ _ _) \Rightarrow False])) I (PCons n n0 p) H2) in +(False_ind ((eq C c c1) \to ((eq C c c2) \to (drop1 (PCons n n0 (PConsTail p +h d)) c1 c3))) H5)) H3 H4)))) | (drop1_cons c0 c4 h0 d0 H2 c5 hds H3) +\Rightarrow (\lambda (H4: (eq PList (PCons h0 d0 hds) (PCons n n0 +p))).(\lambda (H5: (eq C c0 c1)).(\lambda (H6: (eq C c5 c2)).((let H7 \def +(f_equal PList PList (\lambda (e: PList).(match e in PList return (\lambda +(_: PList).PList) with [PNil \Rightarrow hds | (PCons _ _ p) \Rightarrow p])) +(PCons h0 d0 hds) (PCons n n0 p) H4) in ((let H8 \def (f_equal PList nat +(\lambda (e: PList).(match e in PList return (\lambda (_: PList).nat) with +[PNil \Rightarrow d0 | (PCons _ n _) \Rightarrow n])) (PCons h0 d0 hds) +(PCons n n0 p) H4) in ((let H9 \def (f_equal PList nat (\lambda (e: +PList).(match e in PList return (\lambda (_: PList).nat) with [PNil +\Rightarrow h0 | (PCons n _ _) \Rightarrow n])) (PCons h0 d0 hds) (PCons n n0 +p) H4) in (eq_ind nat n (\lambda (n1: nat).((eq nat d0 n0) \to ((eq PList hds +p) \to ((eq C c0 c1) \to ((eq C c5 c2) \to ((drop n1 d0 c0 c4) \to ((drop1 +hds c4 c5) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))))))) (\lambda +(H10: (eq nat d0 n0)).(eq_ind nat n0 (\lambda (n1: nat).((eq PList hds p) \to +((eq C c0 c1) \to ((eq C c5 c2) \to ((drop n n1 c0 c4) \to ((drop1 hds c4 c5) +\to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3))))))) (\lambda (H11: (eq +PList hds p)).(eq_ind PList p (\lambda (p0: PList).((eq C c0 c1) \to ((eq C +c5 c2) \to ((drop n n0 c0 c4) \to ((drop1 p0 c4 c5) \to (drop1 (PCons n n0 +(PConsTail p h d)) c1 c3)))))) (\lambda (H12: (eq C c0 c1)).(eq_ind C c1 +(\lambda (c: C).((eq C c5 c2) \to ((drop n n0 c c4) \to ((drop1 p c4 c5) \to +(drop1 (PCons n n0 (PConsTail p h d)) c1 c3))))) (\lambda (H13: (eq C c5 +c2)).(eq_ind C c2 (\lambda (c: C).((drop n n0 c1 c4) \to ((drop1 p c4 c) \to +(drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))) (\lambda (H14: (drop n n0 c1 +c4)).(\lambda (H15: (drop1 p c4 c2)).(drop1_cons c1 c4 n n0 H14 c3 (PConsTail +p h d) (H0 c4 H15)))) c5 (sym_eq C c5 c2 H13))) c0 (sym_eq C c0 c1 H12))) hds +(sym_eq PList hds p H11))) d0 (sym_eq nat d0 n0 H10))) h0 (sym_eq nat h0 n +H9))) H8)) H7)) H5 H6 H2 H3))))]) in (H2 (refl_equal PList (PCons n n0 p)) +(refl_equal C c1) (refl_equal C c2))))))))) hds)))))). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma index da4cb9245..41c5d1e46 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma @@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs". include "T/defs.ma". +include "s/defs.ma". + definition lref_map: ((nat \to nat)) \to (nat \to (T \to T)) \def diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma index f6f3eb39f..7c205f57a 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma @@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props". include "lift/fwd.ma". +include "s/props.ma". + theorem thead_x_lift_y_y: \forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t)) t) \to (\forall (P: Prop).P)))))) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma index 9ce6a4755..b67722f58 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma @@ -16,9 +16,9 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt". -include "lift/defs.ma". +include "lift/fwd.ma". -include "tlt/defs.ma". +include "tlt/props.ma". theorem lift_weight_map: \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma index 3492c7ba4..4b548cbff 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma @@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd". include "lift1/defs.ma". +include "lift/fwd.ma". + theorem lift1_lref: \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma index a47a50e07..eeec1fc7d 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma @@ -18,6 +18,10 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props". include "lift1/defs.ma". +include "lift/props.ma". + +include "drop1/defs.ma". + theorem lift1_xhg: \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))) @@ -53,3 +57,59 @@ t0))))) (refl_equal TList (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0)))) (lifts1 (Ss hds) (lifts (S O) O t0)) H) (lift1 (Ss hds) (lift (S O) O t)) (lift1_xhg hds t))))) ts)). +theorem lift1_free: + \forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds +(lift (S i) O t)) (lift (S (trans hds i)) O (ctrans hds i t))))) +\def + \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: +nat).(\forall (t: T).(eq T (lift1 p (lift (S i) O t)) (lift (S (trans p i)) O +(ctrans p i t)))))) (\lambda (i: nat).(\lambda (t: T).(refl_equal T (lift (S +i) O t)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (hds0: +PList).(\lambda (H: ((\forall (i: nat).(\forall (t: T).(eq T (lift1 hds0 +(lift (S i) O t)) (lift (S (trans hds0 i)) O (ctrans hds0 i t))))))).(\lambda +(i: nat).(\lambda (t: T).(eq_ind_r T (lift (S (trans hds0 i)) O (ctrans hds0 +i t)) (\lambda (t0: T).(eq T (lift h d t0) (lift (S (match (blt (trans hds0 +i) d) with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans +hds0 i) h)])) O (match (blt (trans hds0 i) d) with [true \Rightarrow (lift h +(minus d (S (trans hds0 i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans +hds0 i t)])))) (xinduction bool (blt (trans hds0 i) d) (\lambda (b: bool).(eq +T (lift h d (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S (match b +with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 +i) h)])) O (match b with [true \Rightarrow (lift h (minus d (S (trans hds0 +i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans hds0 i t)])))) (\lambda +(x_x: bool).(bool_ind (\lambda (b: bool).((eq bool (blt (trans hds0 i) d) b) +\to (eq T (lift h d (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S +(match b with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus +(trans hds0 i) h)])) O (match b with [true \Rightarrow (lift h (minus d (S +(trans hds0 i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans hds0 i +t)]))))) (\lambda (H0: (eq bool (blt (trans hds0 i) d) true)).(eq_ind_r nat +(plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))) (\lambda (n: nat).(eq +T (lift h n (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S (trans +hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t))))) +(eq_ind_r T (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) +(ctrans hds0 i t))) (\lambda (t0: T).(eq T t0 (lift (S (trans hds0 i)) O +(lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t))))) (refl_equal T +(lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 +i t)))) (lift h (plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))) (lift +(S (trans hds0 i)) O (ctrans hds0 i t))) (lift_d (ctrans hds0 i t) h (S +(trans hds0 i)) (minus d (S (trans hds0 i))) O (le_O_n (minus d (S (trans +hds0 i)))))) d (le_plus_minus (S (trans hds0 i)) d (bge_le (S (trans hds0 i)) +d (le_bge (S (trans hds0 i)) d (lt_le_S (trans hds0 i) d (blt_lt d (trans +hds0 i) H0))))))) (\lambda (H0: (eq bool (blt (trans hds0 i) d) +false)).(eq_ind_r T (lift (plus h (S (trans hds0 i))) O (ctrans hds0 i t)) +(\lambda (t0: T).(eq T t0 (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i +t)))) (eq_ind nat (S (plus h (trans hds0 i))) (\lambda (n: nat).(eq T (lift n +O (ctrans hds0 i t)) (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t)))) +(eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O +(ctrans hds0 i t)) (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t)))) +(refl_equal T (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t))) (plus h +(trans hds0 i)) (plus_comm h (trans hds0 i))) (plus h (S (trans hds0 i))) +(plus_n_Sm h (trans hds0 i))) (lift h d (lift (S (trans hds0 i)) O (ctrans +hds0 i t))) (lift_free (ctrans hds0 i t) (S (trans hds0 i)) h O d (eq_ind nat +(S (plus O (trans hds0 i))) (\lambda (n: nat).(le d n)) (eq_ind_r nat (plus +(trans hds0 i) O) (\lambda (n: nat).(le d (S n))) (le_S d (plus (trans hds0 +i) O) (le_plus_trans d (trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus +O (trans hds0 i)) (plus_comm O (trans hds0 i))) (plus O (S (trans hds0 i))) +(plus_n_Sm O (trans hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O +t)) (H i t)))))))) hds). + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma index c24e6622d..c0b188265 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma @@ -74,6 +74,10 @@ include "drop/fwd.ma". include "drop/props.ma". +include "drop1/defs.ma". + +include "drop1/props.ma". + include "G/defs.ma". include "next_plus/defs.ma".