]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/POPLmark/Fsub/defndb.ma
new definition of lleq allows to complete the proof of lemma 1000
[helm.git] / matita / matita / contribs / POPLmark / Fsub / defndb.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 include "Fsub/util.ma".
16 include "nat/le_arith.ma".
17 include "nat/lt_arith.ma".
18
19 (*** representation of Fsub types ***)  
20 inductive Typ : Set ≝
21   | TVar : nat → Typ          (* type var *)
22   | Top : Typ                 (* maximum type *)
23   | Arrow : Typ → Typ → Typ   (* functions *) 
24   | Forall : Typ → Typ → Typ. (* universal type *)
25
26 (* representation of bounds *)
27
28 record bound : Set ≝ { 
29                           istype : bool;    (* is subtyping bound? *)
30                           btype  : Typ      (* type to which the name is bound *)
31                      }.
32
33 (*** Type Well-Formedness judgement ***)
34
35 inductive WFType : list bound → Typ → Prop ≝
36   | WFT_TVar : ∀G,n,T.n < length ? G → (nth ? G (mk_bound true Top) n = mk_bound true T) → 
37                WFType G (TVar n)
38   | WFT_Top : ∀G.WFType G Top
39   | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U)
40   | WFT_Forall : ∀G,T,U.WFType G T → WFType (mk_bound true T::G) U → 
41                  WFType G (Forall T U).
42
43 (*** Environment Well-Formedness judgement ***)
44
45 inductive WFEnv : list bound → Prop ≝
46   | WFE_Empty : WFEnv (nil ?)
47   | WFE_cons : ∀B,T,G.WFEnv G → WFType G T → WFEnv (mk_bound B T :: G).
48             
49 let rec lift T h k on T ≝
50 match T with
51 [ TVar n ⇒ TVar (match (leb k n) with [true ⇒ n + h | false ⇒ n])
52 | Top ⇒ Top
53 | Arrow U V ⇒ Arrow (lift U h k) (lift V h k)
54 | Forall U V ⇒ Forall (lift U h k) (lift V h (S k))].
55             
56 (*** Subtyping judgement ***)              
57 inductive JSubtype : list bound → Typ → Typ → Prop ≝
58   | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
59   | SA_Refl_TVar : ∀G,n.WFEnv G → WFType G (TVar n) → JSubtype G (TVar n) (TVar n)
60   | SA_Trans_TVar : ∀G,n,T,U.n < length ? G → 
61                       nth ? G (mk_bound true Top) n = mk_bound true U → 
62                       JSubtype G (lift U (S n) O) T → JSubtype G (TVar n) T
63   | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 → 
64                JSubtype G (Arrow S1 S2) (Arrow T1 T2)
65   | SA_All : ∀G,S1,S2,T1,T2. 
66              JSubtype G T1 S1 → JSubtype (mk_bound true T1 :: G) S2 T2 →
67              JSubtype G (Forall S1 S2) (Forall T1 T2).
68
69 notation "hvbox(e ⊢ break ta ⊴  break tb)" 
70   non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.  
71 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
72
73 notation > "hvbox(\Forall S.T)" 
74   non associative with precedence 65 for @{ 'forall $S $T}.
75 notation < "hvbox('All' \sub S. break T)" 
76   non associative with precedence 65 for @{ 'forall $S $T}.
77 interpretation "universal type" 'forall S T = (Forall S T).
78   
79 notation "#x" with precedence 79 for @{'tvar $x}.
80 interpretation "bound tvar" 'tvar x = (TVar x).
81
82 notation "⊤" with precedence 90 for @{'toptype}.
83 interpretation "toptype" 'toptype = Top.
84
85 notation "hvbox(s break ⇛ t)"
86   right associative with precedence 60 for @{ 'arrow $s $t }.
87 interpretation "arrow type" 'arrow S T = (Arrow S T).
88
89 notation "hvbox(⊴ T)"
90   non associative with precedence 65 for @{ 'subtypebound $T }.
91 interpretation "subtyping bound" 'subtypebound T = (mk_bound true T).  
92
93 (****** PROOFS ********)
94
95 (*** theorems about lists ***)
96
97 let rec flift f k on k ≝ match k with
98 [ O ⇒ f
99 | S p ⇒ flift (λn.match n with [ O ⇒ O | S m ⇒ S (f m) ]) p ]. 
100
101 let rec perm T f ≝ match T with
102 [ TVar m ⇒ TVar (f m)
103 | Top ⇒ Top
104 | Arrow U V ⇒ Arrow (perm U f) (perm V f)
105 | Forall U V ⇒ Forall (perm U f) (perm V (flift f 1))].
106
107 definition blift : bound → nat → bound ≝ 
108 λB,n.match B with [ mk_bound b t ⇒ mk_bound b (lift t n O) ].
109
110 definition bperm : bound → (nat→nat) → bound ≝
111 λB,f.match B with [ mk_bound b t ⇒ mk_bound b (perm t f) ].
112  
113 definition incl : list bound → list bound → (nat → nat) → Prop ≝
114 λG,H,f.injective ?? f → ∀n.n < length ? G → 
115   bperm (blift (nth ? G (mk_bound true Top) n) (S n)) f =
116   blift (nth ? H (mk_bound true Top) (f n)) (S (f n)).
117   
118 lemma lift_lift : ∀T,n,m,k.lift (lift T n k) m k = lift T (n+m) k.
119 intros 3;elim T;simplify;
120 [apply (leb_elim k n1);intros;simplify;
121  [apply leb_elim;intros;simplify;
122   [apply eq_f;rewrite < assoc_plus;reflexivity
123   |elim H1;autobatch]
124  |rewrite > lt_to_leb_false
125   [simplify;reflexivity
126   |autobatch]]
127 |*:autobatch]
128 qed.
129
130 lemma lift_O : ∀T,k.lift T O k = T.
131 intro;elim T;simplify
132 [cases (leb k n);simplify;autobatch paramodulation
133 |*:autobatch]
134 qed.
135
136 lemma flift_flift : ∀h,k,f.flift (flift f h) k = flift f (h+k).
137 intros 2;elim h;simplify
138 [reflexivity
139 |rewrite > H;reflexivity]
140 qed.
141
142 lemma eq_f_g_to_eq_fx_gx : ∀A,B:Type.∀f,g:A → B.∀x.f = g → f x = g x.
143 intros;rewrite > H;reflexivity;
144 qed.
145
146 lemma flift_S : ∀n,m,f.flift f (S n) (S m) = S (flift f n m).
147 intros 2;elim n
148 [reflexivity
149 |cut (flift f (S (S n1)) (S m) = flift (flift f (S n1)) 1 (S m))
150  [rewrite > Hcut;simplify;reflexivity
151  |change in match (S (S n1)) with (1 + (S n1));rewrite > sym_plus;
152   apply eq_f_g_to_eq_fx_gx;symmetry;apply flift_flift]]
153 qed.
154
155 lemma le_flift : ∀k,n.k ≤ n → ∀f.k ≤ flift f k n.
156 intro;elim k
157 [autobatch
158 |cut (∃p.n1 = S p)
159  [elim Hcut;rewrite > H2;rewrite > flift_S;apply le_S_S;apply H;
160   rewrite > H2 in H1;autobatch
161  |elim H1
162   [exists[apply n]
163    reflexivity
164   |elim H3;exists[apply (S a)]
165    apply eq_f;assumption]]]
166 qed.
167
168 lemma le_flift2 : ∀k,n.n < k → ∀f.flift f k n = n.
169 intro;elim k
170 [elim (not_le_Sn_O ? H)
171 |generalize in match H1;cases n1;intros
172  [cut (flift f (S n) O = flift (flift f n) 1 O)
173   [rewrite > Hcut;reflexivity
174   |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation]
175  |rewrite > flift_S;apply eq_f;apply H;autobatch]]
176 qed.
177
178 lemma lift_perm : ∀T,n,f,k.perm (lift T (S n) k) (flift f (S k)) = lift (perm (lift T n k) (flift f k)) 1 k.
179 intros 2;elim T;simplify;
180 [apply (leb_elim k n1);simplify;intros
181  [apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1);
182   cut (flift (flift f 1) k (n1+S n) = flift (flift f k) 1 (n1+S n))
183   [rewrite > Hcut;rewrite < plus_n_Sm;simplify;
184    apply (leb_elim k (flift f k (n1+n)));simplify;intros
185    [rewrite > sym_plus in ⊢ (???%);simplify;reflexivity
186    |elim H1;elim k in H
187     [autobatch
188     |apply le_flift;autobatch]]
189   |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation]
190  |apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1);
191   rewrite > le_flift2 [|autobatch]
192   apply (leb_elim k (flift f k n1));simplify;intro
193   [rewrite > le_flift2 in H1 [|autobatch]
194    elim (H H1)
195   |symmetry;apply le_flift2;autobatch]]
196 |reflexivity
197 |apply eq_f2;change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1);
198   rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch
199 |apply eq_f2
200  [change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1);
201   rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch
202  |change in ⊢ (??(??%)?) with (flift (flift (flift f 1) k) 1);
203   rewrite > flift_flift in ⊢ (??%?);
204   rewrite > sym_plus in ⊢ (? ? (? ? (? ? %)) ?);
205   rewrite > flift_flift;
206   simplify in ⊢ (? ? (? ? (? ? %)) ?);
207   rewrite > H1;do 2 apply eq_f_g_to_eq_fx_gx;
208   apply eq_f;apply eq_f;
209   change in ⊢ (???%) with (flift (flift f k) 1);
210   rewrite > flift_flift;rewrite > sym_plus;reflexivity]]
211 qed.
212
213 lemma blift_bperm : ∀B,n,f.bperm (blift B (S n)) (flift f 1) = blift (bperm (blift B n) f) 1.
214 intros;cases B;simplify;apply eq_f;
215 change in ⊢ (? ? ? (? (? ? %) ? ?)) with (flift f O);
216 apply lift_perm;
217 qed.
218
219 definition lifter : nat → nat → nat → nat ≝
220  λn,k,m.match (leb k m) with
221  [ true ⇒ m+n
222  | false ⇒ m ].
223  
224 lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g.
225 intro;elim T
226 [4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x)
227  [rewrite > (H f g);
228   [rewrite > (H1 (flift f 1) (flift g 1));
229    [reflexivity
230    |assumption]
231   |assumption]
232  |intro;simplify;cases x
233   [reflexivity
234   |simplify;rewrite > H2;reflexivity]]
235 |*:simplify;autobatch]
236 qed.
237
238 lemma flift_lifter : ∀p,n,m,k.flift (lifter n k) p m = lifter n (k+p) m.
239 intro;elim p
240 [simplify;autobatch paramodulation
241 |change in ⊢ (? ? (? ? % ?) ?) with (1+n);
242  rewrite < plus_n_Sm;whd in ⊢ (???%);
243  transitivity (flift (flift (lifter n1 k) n) 1 m)
244  [apply eq_f_g_to_eq_fx_gx;rewrite > sym_plus;autobatch
245  |unfold lifter;simplify;
246   change in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? (? % ? ?)] ?) with (lifter n1 k);
247   cases m
248   [simplify;reflexivity
249   |simplify;rewrite > H;unfold lifter;cases (leb (k+n) n2);reflexivity]]]
250 qed.
251
252 lemma lift_perm2 : ∀T,n,k.lift T n k = perm T (lifter n k).
253 intros 2;elim T;simplify
254 [1,2,3:autobatch
255 |rewrite < H;change in ⊢ (???(??(??%))) with (flift (lifter n k) 1);
256  rewrite > H1;
257  rewrite > (extensional_perm ? (lifter n (S k)) (flift (lifter n k) 1))
258  [reflexivity
259  |intro;symmetry;autobatch]]
260 qed.
261
262 lemma incl_cons : ∀G,H,f,T.injective ?? f → incl G H f → 
263                            incl (⊴ T::G) (⊴ perm T f :: H) (flift f 1).
264 intros;unfold;intros 2;
265 elim n;
266 [simplify;change in ⊢ (? ? (? ? (? ? %)) ?) with (flift f 1);
267  rewrite > lift_perm;rewrite > lift_O;reflexivity
268 |simplify in H5;lapply (le_S_S_to_le ?? H5);clear H5;
269  simplify in ⊢ (? ? ? (? % ?));
270  simplify in ⊢ (? ? (? (? % ?) ?) ?);
271  unfold in H2;rewrite > (blift_bperm ? ? f);
272  rewrite > (H2 ?? Hletin);
273  [cases (nth bound H (mk_bound true Top) (f n1));
274   simplify;rewrite > lift_lift;rewrite > sym_plus;
275   reflexivity
276  |assumption]]
277 qed.
278
279 lemma injective_flift : ∀f,n.injective ?? f → injective ?? (flift f n).
280 intros;elim n
281 [simplify;assumption
282 |change in ⊢ (? ? ? (? ? %)) with (1+n1);rewrite > sym_plus;
283  rewrite < flift_flift;unfold;intros 2;
284  cases (decidable_eq_nat x 0)
285  [rewrite > le_flift2
286   [cases (decidable_eq_nat y 0)
287    [intro;autobatch paramodulation
288    |elim y in H3
289     [elim H3;reflexivity
290     |simplify in H5;destruct]]
291   |rewrite > H2;autobatch]
292  |generalize in match H2;cases x
293   [intros;elim H3;reflexivity
294   |intro;cases y;simplify;intros;destruct;
295    rewrite > (H1 ?? Hcut);reflexivity]]]
296 qed.
297
298 lemma injective_lifter : ∀n,k.injective ?? (lifter n k).
299 intros;unfold;intros;unfold lifter in H;
300 apply (leb_elim k x);intros;
301 [rewrite > (le_to_leb_true ?? H1) in H;apply (leb_elim k y);intros;
302  [rewrite > (le_to_leb_true ?? H2) in H;simplify in H;
303   autobatch
304  |lapply (not_le_to_lt ?? H2) as H3;rewrite > (lt_to_leb_false ?? H3) in H;
305   simplify in H;rewrite < H in H2;elim H2;autobatch]
306 |lapply (not_le_to_lt ?? H1) as H2;rewrite > (lt_to_leb_false ?? H2) in H;
307  apply (leb_elim k y);intros
308  [rewrite > (le_to_leb_true ?? H3) in H;simplify in H;rewrite > H in H1;
309   elim H1;autobatch
310  |lapply (not_le_to_lt ?? H3) as H4;rewrite > (lt_to_leb_false ?? H4) in H;
311   simplify in H;assumption]]
312 qed.
313
314 lemma incl_append : ∀G,H. incl G (H@G) (lifter (length ? H) O).
315 intros;unfold;intros;
316 cut (nth ? G (⊴ ⊤) n = nth ? (H@G) (⊴ ⊤) (lifter (length ? H) O n))
317 [rewrite < Hcut;cases (nth bound G (⊴ ⊤) n);simplify;
318  rewrite < lift_perm2;rewrite > lift_lift;reflexivity
319 |elim H
320  [simplify;rewrite < plus_n_O;reflexivity
321  |simplify;rewrite < plus_n_Sm;apply H3]] 
322 qed.
323
324 lemma flift_id : ∀m,n.flift (λx.x) m n = n.
325 intro;elim m
326 [reflexivity
327 |change in ⊢ (??(??%?)?) with (1+n);rewrite > sym_plus;
328  transitivity (flift (flift (λx.x) n) 1 n1)
329  [apply eq_f_g_to_eq_fx_gx;autobatch
330  |simplify;generalize in match H;cases n1;intro
331   [reflexivity
332   |simplify;apply eq_f;apply H1]]]
333 qed. 
334
335 lemma perm_id : ∀T,n.T = perm T (flift (λx.x) n).
336 intro;elim T;
337 [1:simplify;rewrite > flift_id;reflexivity
338 |4:whd in ⊢ (???%);rewrite > flift_flift;rewrite < H1;rewrite < H;reflexivity
339 |*:simplify;autobatch]
340 qed.
341
342 lemma perm_compose : ∀T,f,g.perm (perm T f) g = perm T (λx.g (f x)).
343 intro;elim T
344 [reflexivity
345 |reflexivity
346 |simplify;autobatch
347 |simplify;rewrite > H;
348  change in ⊢ (? ? (? ? (? (? ? %) ?)) ?) with (flift f 1);
349  change in ⊢ (? ? (? ? (? ? %)) ?) with (flift g 1);
350  rewrite > H1;
351  change in ⊢ (? ? ? (? ? (? ? %))) with (flift (λx.g (f x)) 1);
352  rewrite > (extensional_perm ? (λx.flift g 1 (flift f 1 x)) (flift (λx.g (f x)) 1));
353  [reflexivity
354  |intros;cases x;simplify;reflexivity]]
355 qed.
356
357 lemma WFT_env_incl : ∀G,T.WFType G T → ∀H,f.injective nat nat f → incl G H f →
358                           (∀n. n < length ? G → f n < length ? H) → 
359                           WFType H (perm T f).
360 intros 3;elim H
361 [simplify;unfold in H5;lapply (H5 H4 n H1);
362  cut (∃T.nth ? H3 (mk_bound true Top) (f n) = mk_bound true T)
363  [elim Hcut;apply WFT_TVar
364   [apply a
365   |*:autobatch]
366  |rewrite > H2 in Hletin;simplify in Hletin;
367   elim (nth bound H3 (mk_bound true Top) (f n)) in Hletin;elim b in H7
368   [exists[apply t1]
369    reflexivity
370   |simplify in H7;destruct]]
371 |2:simplify;autobatch
372 |simplify;autobatch width=4 size=9
373 |simplify;apply WFT_Forall
374  [autobatch
375  |apply H4
376   [change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
377   |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption
378   |intro;cases n;simplify;intros;autobatch depth=4]]]
379 qed.
380
381 lemma WFT_env_incl2: ∀G,T.WFType G T → ∀H.length ? G = length ? H →
382 (∀n,U.n < length ? G → nth ? G (mk_bound true Top) n = mk_bound true U → 
383  ∃V.nth ? H (mk_bound true Top) n = mk_bound true V) →
384  WFType H T.
385 intros 3;elim H
386 [elim (H5 n t)
387  [apply WFT_TVar
388   [2:applyS H1
389   |3:apply H6]
390  |assumption
391  |assumption]
392 |autobatch
393 |apply WFT_Arrow;autobatch
394 |apply WFT_Forall;try autobatch;
395  apply H4;
396  [simplify;autobatch
397  |intros;elim n in H8 H9
398   [exists[apply t]
399    reflexivity
400   |elim (H7 n1 U ? H10)
401    [exists[apply a]
402     assumption
403    |apply le_S_S_to_le;apply H9]]]]
404 qed.
405
406 lemma WFT_extends : ∀G,H,U,P,T.WFType (G@(mk_bound true U::H)) T → WFType (G@(mk_bound true P::H)) T.
407 intros;apply (WFT_env_incl2 ?? H1)
408 [elim G;simplify
409  [reflexivity
410  |rewrite > H2;reflexivity]
411 |intros 3;elim (decidable_eq_nat n (length ? G))
412  [exists [apply P]
413   elim G in n H3
414   [simplify in H4;destruct;reflexivity
415   |simplify;simplify in H5;rewrite > H5;simplify;apply H3;reflexivity]
416  |exists [apply U1]
417   elim G in n H3 H4 0
418   [simplify;intro;elim n1
419    [elim H3;reflexivity
420    |simplify in H5;simplify;assumption]
421   |simplify;intros 4;elim n1
422    [simplify in H5;simplify;assumption
423    |simplify;apply H3
424     [intro;elim H5;autobatch
425     |apply H6]]]]]
426 qed.
427
428 lemma WFE_extends : ∀G,H,U,P.WFType H P → WFEnv (G@(mk_bound true U::H)) → WFEnv (G@(mk_bound true P::H)).
429 intros;cut (WFType H U)
430 [generalize in match H2;elim G 0;simplify;intros
431  [inversion H3;intros;destruct;autobatch
432  |generalize in match H4;cases a;intros;apply WFE_cons
433   [inversion H4;intros;destruct;autobatch
434   |inversion H5;intros;destruct;autobatch]]
435 |elim G in H2 0;simplify;intros;
436  [inversion H2;intros;destruct;assumption
437  |apply H2;inversion H3;simplify;intros;destruct;assumption]]
438 qed.
439
440 (*** lemmata relating subtyping and well-formedness ***)
441
442 lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
443 intros;elim H;assumption.
444 qed.
445
446 lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
447 intros;elim H
448   [1,2:autobatch
449   |elim H4;split;autobatch 
450   |decompose;autobatch size=7
451   |decompose;split
452    [apply WFT_Forall;
453     [assumption
454     |apply (WFT_env_incl2 ?? H2) [reflexivity]
455      simplify;intros 3;elim n
456      [exists[apply t]
457       reflexivity
458      |exists[apply U1]
459       assumption]]
460    |autobatch]]
461 qed.
462
463 lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
464 intros;elim (JS_to_WFT ? ? ? H);assumption;
465 qed.
466
467 lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
468 intros;elim (JS_to_WFT ? ? ? H);assumption;
469 qed.