]> matita.cs.unibo.it Git - helm.git/blob - fwd.ma
48d11a44e4fd10fd2b0526f9b2c64dc3989d4bf3
[helm.git] / fwd.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "basic_1/subst1/defs.ma".
18
19 include "basic_1/subst0/fwd.ma".
20
21 implied lemma subst1_ind:
22  \forall (i: nat).(\forall (v: T).(\forall (t1: T).(\forall (P: ((T \to 
23 Prop))).((P t1) \to (((\forall (t2: T).((subst0 i v t1 t2) \to (P t2)))) \to 
24 (\forall (t: T).((subst1 i v t1 t) \to (P t))))))))
25 \def
26  \lambda (i: nat).(\lambda (v: T).(\lambda (t1: T).(\lambda (P: ((T \to 
27 Prop))).(\lambda (f: (P t1)).(\lambda (f0: ((\forall (t2: T).((subst0 i v t1 
28 t2) \to (P t2))))).(\lambda (t: T).(\lambda (s0: (subst1 i v t1 t)).(match s0 
29 with [subst1_refl \Rightarrow f | (subst1_single x x0) \Rightarrow (f0 x 
30 x0)])))))))).
31
32 lemma subst1_gen_sort:
33  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1 
34 i v (TSort n) x) \to (eq T x (TSort n))))))
35 \def
36  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda 
37 (H: (subst1 i v (TSort n) x)).(subst1_ind i v (TSort n) (\lambda (t: T).(eq T 
38 t (TSort n))) (refl_equal T (TSort n)) (\lambda (t2: T).(\lambda (H0: (subst0 
39 i v (TSort n) t2)).(subst0_gen_sort v t2 i n H0 (eq T t2 (TSort n))))) x 
40 H))))).
41
42 lemma subst1_gen_lref:
43  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1 
44 i v (TLRef n) x) \to (or (eq T x (TLRef n)) (land (eq nat n i) (eq T x (lift 
45 (S n) O v))))))))
46 \def
47  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda 
48 (H: (subst1 i v (TLRef n) x)).(subst1_ind i v (TLRef n) (\lambda (t: T).(or 
49 (eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl 
50 (eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O 
51 v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v 
52 (TLRef n) t2)).(land_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2 
53 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v)))) (\lambda (H1: (eq 
54 nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2 
55 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i) 
56 (eq T t2 (lift (S n) O v)) H1 H2)))) (subst0_gen_lref v t2 i n H0)))) x 
57 H))))).
58
59 lemma subst1_gen_head:
60  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall 
61 (x: T).(\forall (i: nat).((subst1 i v (THead k u1 t1) x) \to (ex3_2 T T 
62 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead k u2 t2)))) (\lambda (u2: 
63 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2: 
64 T).(subst1 (s k i) v t1 t2))))))))))
65 \def
66  \lambda (k: K).(\lambda (v: T).(\lambda (u1: T).(\lambda (t1: T).(\lambda 
67 (x: T).(\lambda (i: nat).(\lambda (H: (subst1 i v (THead k u1 t1) 
68 x)).(subst1_ind i v (THead k u1 t1) (\lambda (t: T).(ex3_2 T T (\lambda (u2: 
69 T).(\lambda (t2: T).(eq T t (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
70 T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1 
71 t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k u1 
72 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) 
73 (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1 t2))) u1 t1 (refl_equal 
74 T (THead k u1 t1)) (subst1_refl i v u1) (subst1_refl (s k i) v t1)) (\lambda 
75 (t2: T).(\lambda (H0: (subst0 i v (THead k u1 t1) t2)).(or3_ind (ex2 T 
76 (\lambda (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 
77 u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3: 
78 T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: 
79 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v 
80 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))) (ex3_2 
81 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda 
82 (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3: 
83 T).(subst1 (s k i) v t1 t3)))) (\lambda (H1: (ex2 T (\lambda (u2: T).(eq T t2 
84 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2)))).(ex2_ind T (\lambda 
85 (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2)) 
86 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) 
87 (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: 
88 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda 
89 (H2: (eq T t2 (THead k x0 t1))).(\lambda (H3: (subst0 i v u1 
90 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 
91 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: 
92 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 t1 H2 (subst1_single i v u1 
93 x0 H3) (subst1_refl (s k i) v t1))))) H1)) (\lambda (H1: (ex2 T (\lambda (t3: 
94 T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 
95 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3: 
96 T).(subst0 (s k i) v t1 t3)) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq 
97 T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) 
98 (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: 
99 T).(\lambda (H2: (eq T t2 (THead k u1 x0))).(\lambda (H3: (subst0 (s k i) v 
100 t1 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k 
101 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: 
102 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) u1 x0 H2 (subst1_refl i v u1) 
103 (subst1_single (s k i) v t1 x0 H3))))) H1)) (\lambda (H1: (ex3_2 T T (\lambda 
104 (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: 
105 T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3: 
106 T).(subst0 (s k i) v t1 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: 
107 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v 
108 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T 
109 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: 
110 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3: 
111 T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda 
112 (H2: (eq T t2 (THead k x0 x1))).(\lambda (H3: (subst0 i v u1 x0)).(\lambda 
113 (H4: (subst0 (s k i) v t1 x1)).(ex3_2_intro T T (\lambda (u2: T).(\lambda 
114 (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 
115 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 
116 x1 H2 (subst1_single i v u1 x0 H3) (subst1_single (s k i) v t1 x1 H4))))))) 
117 H1)) (subst0_gen_head k v u1 t1 t2 i H0)))) x H))))))).
118
119 lemma subst1_gen_lift_lt:
120  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
121 (h: nat).(\forall (d: nat).((subst1 i (lift h d u) (lift h (S (plus i d)) t1) 
122 x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d)) t2))) (\lambda 
123 (t2: T).(subst1 i u t1 t2)))))))))
124 \def
125  \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda 
126 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i (lift h d u) (lift h (S 
127 (plus i d)) t1) x)).(subst1_ind i (lift h d u) (lift h (S (plus i d)) t1) 
128 (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h (S (plus i d)) t2))) 
129 (\lambda (t2: T).(subst1 i u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T 
130 (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t2))) (\lambda (t2: 
131 T).(subst1 i u t1 t2)) t1 (refl_equal T (lift h (S (plus i d)) t1)) 
132 (subst1_refl i u t1)) (\lambda (t2: T).(\lambda (H0: (subst0 i (lift h d u) 
133 (lift h (S (plus i d)) t1) t2)).(ex2_ind T (\lambda (t3: T).(eq T t2 (lift h 
134 (S (plus i d)) t3))) (\lambda (t3: T).(subst0 i u t1 t3)) (ex2 T (\lambda 
135 (t3: T).(eq T t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 
136 t3))) (\lambda (x0: T).(\lambda (H1: (eq T t2 (lift h (S (plus i d)) 
137 x0))).(\lambda (H2: (subst0 i u t1 x0)).(ex_intro2 T (\lambda (t3: T).(eq T 
138 t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 t3)) x0 H1 
139 (subst1_single i u t1 x0 H2))))) (subst0_gen_lift_lt u t1 t2 i h d H0)))) x 
140 H))))))).
141
142 lemma subst1_gen_lift_eq:
143  \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall 
144 (d: nat).(\forall (i: nat).((le d i) \to ((lt i (plus d h)) \to ((subst1 i u 
145 (lift h d t) x) \to (eq T x (lift h d t))))))))))
146 \def
147  \lambda (t: T).(\lambda (u: T).(\lambda (x: T).(\lambda (h: nat).(\lambda 
148 (d: nat).(\lambda (i: nat).(\lambda (H: (le d i)).(\lambda (H0: (lt i (plus d 
149 h))).(\lambda (H1: (subst1 i u (lift h d t) x)).(subst1_ind i u (lift h d t) 
150 (\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda 
151 (t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t 
152 u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
153
154 lemma subst1_gen_lift_ge:
155  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
156 (h: nat).(\forall (d: nat).((subst1 i u (lift h d t1) x) \to ((le (plus d h) 
157 i) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: 
158 T).(subst1 (minus i h) u t1 t2))))))))))
159 \def
160  \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda 
161 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i u (lift h d t1) 
162 x)).(\lambda (H0: (le (plus d h) i)).(subst1_ind i u (lift h d t1) (\lambda 
163 (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h d t2))) (\lambda (t2: 
164 T).(subst1 (minus i h) u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T (lift 
165 h d t1) (lift h d t2))) (\lambda (t2: T).(subst1 (minus i h) u t1 t2)) t1 
166 (refl_equal T (lift h d t1)) (subst1_refl (minus i h) u t1)) (\lambda (t2: 
167 T).(\lambda (H1: (subst0 i u (lift h d t1) t2)).(ex2_ind T (\lambda (t3: 
168 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst0 (minus i h) u t1 t3)) 
169 (ex2 T (\lambda (t3: T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 
170 (minus i h) u t1 t3))) (\lambda (x0: T).(\lambda (H2: (eq T t2 (lift h d 
171 x0))).(\lambda (H3: (subst0 (minus i h) u t1 x0)).(ex_intro2 T (\lambda (t3: 
172 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 (minus i h) u t1 t3)) x0 
173 H2 (subst1_single (minus i h) u t1 x0 H3))))) (subst0_gen_lift_ge u t1 t2 i h 
174 d H1 H0)))) x H)))))))).
175