]> matita.cs.unibo.it Git - helm.git/commitdiff
dependences fixed
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 6 Sep 2006 14:45:44 +0000 (14:45 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 6 Sep 2006 14:45:44 +0000 (14:45 +0000)
14 files changed:
matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
matita/contribs/LAMBDA-TYPES/Level-1/Base/sequent_viewer.xml [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma
matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma

index f1b0a886c3680fc6b2e4d9890c8c3d314988099a..4e37576d20ca04a51569ea5255cd539a6027db58 100644 (file)
@@ -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 (file)
index 0000000..6aab4a1
--- /dev/null
@@ -0,0 +1,2 @@
+<?xml version="1.0"?>
+<b:box xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:b="http://helm.cs.unibo.it/2003/BoxML" xmlns:helm="http://www.cs.unibo.it/helm" xmlns:xlink="http://www.w3.org/1999/xlink"><b:h><b:space width="0.5em"/><b:v><b:space width="0.5em"/><b:v><b:h helm:xref="h0"><b:obj><m:mi>p</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i1" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h1"><b:obj><m:mi>n</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i2" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h2"><b:obj><m:mi>m</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i3" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h3"><b:obj><m:mi>H</m:mi></b:obj><b:text>:</b:text><b:hv helm:xref="i4"><b:hv helm:xref="i6"><b:obj><m:mi helm:xref="i8">p</m:mi></b:obj><b:obj><m:mrow><m:mo helm:xref="i7" xlink:href="cic:/Coq/Init/Peano/plus.con">+</m:mo><m:mi helm:xref="i9">n</m:mi></m:mrow></b:obj></b:hv><b:h><b:obj><m:mo helm:xref="i5" xlink:href="cic:/Coq/Init/Peano/le.ind#xpointer(1/1)">&#x2264;</m:mo></b:obj><b:hv helm:xref="i10"><b:obj><m:mi helm:xref="i12">p</m:mi></b:obj><b:obj><m:mrow><m:mo helm:xref="i11" xlink:href="cic:/Coq/Init/Peano/plus.con">+</m:mo><m:mi helm:xref="i13">m</m:mi></m:mrow></b:obj></b:hv></b:h></b:hv></b:h></b:v><b:ink width="4cm" height="2px"/><b:space width="0.5em"/><b:obj><m:mi helm:xref="i14" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:v></b:h></b:box>
index 55d6153a88ebedba4b91da8c4be574976368bd02..fa3d9c0611648332abd40d7b4dd4101f536dbbd4 100644 (file)
@@ -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
index 685b59683601e9eca3314f4b08eae56ac1fbeb2e..a33870137ceea84afab8769b29ca7df0cf31fa0e 100644 (file)
@@ -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 
index aedcf4a3ae10a1ed7ca535265fe9653398f30980..aa283e8f42b20c1094ef6ac06e6b783dea532a2d 100644 (file)
@@ -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: 
index 3b7907d2dc622cee7ae1a99800e828a44e2f7360..d9578d9f33db84e76765f4bce0664452183804b2 100644 (file)
 
 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 (file)
index 0000000..164dab3
--- /dev/null
@@ -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 (file)
index 0000000..2e1f964
--- /dev/null
@@ -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)))))).
+
index da4cb9245856ddd4cdd1cc766edc7b8a71655a9c..41c5d1e464981bb0ee3f6530dfa4368658d70d02 100644 (file)
@@ -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
index f6f3eb39f38c12185daa3df8d47bcfa92a152cb4..7c205f57ad34ffdebb9fc1cb47662774fe123391 100644 (file)
@@ -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))))))
index 9ce6a4755689149bdf4a3a063c9845f4d12d7daa..b67722f58eca72d17f85f8253d96291c8a825580 100644 (file)
@@ -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 
index 3492c7ba4a79e04c0a82b0690a942db7464137de..4b548cbffbfb8ebff2ec046a43f3a70179ee7baa 100644 (file)
@@ -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))))
index a47a50e0771a52126b18aa89015dadd152d531ba..eeec1fc7d76e9e2c55a721b613b98d40c99d40f5 100644 (file)
@@ -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).
+
index c24e6622d24f863094b0405ccafad34f8ff17123..c0b188265a421764443a20860b5c4f7847f47fe9 100644 (file)
@@ -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".