]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / frees_fqup.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 "static_2/s_computation/fqup_weight.ma".
16 include "static_2/static/lsubf_lsubr.ma".
17
18 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
19
20 (* Advanced properties ******************************************************)
21
22 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
23 lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+❨T❩ ≘ f.
24 #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
25 #G0 #L0 #T0 #IH #G #L * *
26 [ /3 width=2 by frees_sort, ex_intro/
27 | cases L -L /3 width=2 by frees_atom, ex_intro/
28   #L #I *
29   [ cases I -I #I [2: #V ] #HG #HL #HT destruct
30     [ elim (IH G L V) -IH
31       /3 width=2 by frees_pair, fqu_fqup, fqu_lref_O, ex_intro/
32     | -IH /3 width=2 by frees_unit, ex_intro/
33     ]
34   | #i #HG #HL #HT destruct
35     elim (IH G L (#i)) -IH
36     /3 width=2 by frees_lref, fqu_fqup, fqu_drop, ex_intro/
37   ]
38 | /3 width=2 by frees_gref, ex_intro/
39 | #p #I #V #T #HG #HL #HT destruct
40   elim (IH G L V) // #f1 #HV
41   elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
42   elim (pr_sor_isf_bi f1 (⫰f2))
43   /3 width=6 by frees_fwd_isfin, frees_bind, pr_isf_tl, ex_intro/
44 | #I #V #T #HG #HL #HT destruct
45   elim (IH G L V) // #f1 #HV
46   elim (IH G L T) -IH // #f2 #HT
47   elim (pr_sor_isf_bi f1 f2)
48   /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
49 ]
50 qed-.
51
52 (* Advanced main properties *************************************************)
53
54 theorem frees_bind_void:
55         ∀f1,L,V. L ⊢ 𝐅+❨V❩ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❨T❩ ≘ f2 →
56         ∀f. f1 ⋓ ⫰f2 ≘ f → ∀p,I. L ⊢ 𝐅+❨ⓑ[p,I]V.T❩ ≘ f.
57 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
58 elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
59 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
60 elim (pr_map_split_tl f2) * #g2 #H destruct
61 [ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct
62   lapply (lsubf_inv_refl … H02) -H02 #H02
63   lapply (pr_sor_eq_repl_fwd_dx … Hf … H02) -g2 #Hf
64   /2 width=5 by frees_bind/
65 | elim (lsubf_inv_unit2 … H02) -H02 * [ #g0 #Y #_ #_ #H destruct ]
66   #z1 #g0 #z #Z #Y #X #H02 #Hz1 #Hz #H0 #H destruct
67   lapply (lsubf_inv_refl … H02) -H02 #H02
68   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
69   lapply (pr_sor_eq_repl_back_sn … Hz … H02) -g0 #Hz
70   lapply (pr_sor_eq_repl_back_dx … Hz … H1) -z1 #Hz
71   lapply (pr_sor_comm … Hz) -Hz #Hz
72   lapply (pr_sor_mono … f Hz ?) // -Hz #H
73   lapply (pr_sor_inv_sle_sn … Hf) -Hf #Hf
74   lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by pr_eq_next/ -z #Hf0
75   @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
76   /2 width=1 by pr_sor_sle_dx/
77 ]
78 qed-.
79
80 (* Advanced inversion lemmas ************************************************)
81
82 lemma frees_inv_bind_void:
83       ∀f,p,I,L,V,T. L ⊢ 𝐅+❨ⓑ[p,I]V.T❩ ≘ f →
84       ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L.ⓧ ⊢ 𝐅+❨T❩ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
85 #f #p #I #L #V #T #H
86 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
87 elim (frees_total (L.ⓧ) T) #f0 #Hf0
88 lapply (lsubr_lsubf … Hf0 … Hf2) -Hf2 /2 width=5 by lsubr_unit/ #H20
89 elim (pr_map_split_tl f0) * #g0 #H destruct
90 [ elim (lsubf_inv_push2 … H20) -H20 #g2 #I #Y #H20 #H2 #H destruct
91   lapply (lsubf_inv_refl … H20) -H20 #H20
92   lapply (pr_sor_eq_repl_back_dx … Hf … H20) -g2 #Hf
93   /2 width=5 by ex3_2_intro/
94 | elim (lsubf_inv_unit2 … H20) -H20 * [ #g2 #Y #_ #_ #H destruct ]
95   #z1 #z0 #g2 #Z #Y #X #H20 #Hz1 #Hg2 #H2 #H destruct
96   lapply (lsubf_inv_refl … H20) -H20 #H0
97   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
98   lapply (pr_sor_eq_repl_back_sn … Hg2 … H0) -z0 #Hg2
99   lapply (pr_sor_eq_repl_back_dx … Hg2 … H1) -z1 #Hg2
100   @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
101   /2 width=3 by pr_sor_comm_23_idem/
102 ]
103 qed-.
104
105 lemma frees_ind_void (Q:relation3 …):
106       (
107         ∀f,L,s. 𝐈❨f❩ →  Q L (⋆s) f
108       ) → (
109         ∀f,i. 𝐈❨f❩ →  Q (⋆) (#i) (⫯*[i]↑f)
110       ) → (
111         ∀f,I,L,V.
112         L ⊢ 𝐅+❨V❩ ≘ f →  Q L V f→ Q (L.ⓑ[I]V) (#O) (↑f)
113       ) → (
114         ∀f,I,L. 𝐈❨f❩ →  Q (L.ⓤ[I]) (#O) (↑f)
115       ) → (
116         ∀f,I,L,i.
117         L ⊢ 𝐅+❨#i❩ ≘ f →  Q L (#i) f → Q (L.ⓘ[I]) (#(↑i)) (⫯f)
118       ) → (
119         ∀f,L,l. 𝐈❨f❩ →  Q L (§l) f
120       ) → (
121         ∀f1,f2,f,p,I,L,V,T.
122         L ⊢ 𝐅+❨V❩ ≘ f1 → L.ⓧ ⊢𝐅+❨T❩≘ f2 → f1 ⋓ ⫰f2 ≘ f →
123         Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
124       ) → (
125         ∀f1,f2,f,I,L,V,T.
126         L ⊢ 𝐅+❨V❩ ≘ f1 → L ⊢𝐅+❨T❩ ≘ f2 → f1 ⋓ f2 ≘ f →
127         Q L V f1 → Q L T f2 → Q L (ⓕ[I]V.T) f
128       ) →
129       ∀L,T,f. L ⊢ 𝐅+❨T❩ ≘ f →  Q L T f.
130 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
131 @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
132 [ #s #HG #HL #HT #f #H destruct -IH
133   lapply (frees_inv_sort … H) -H /2 width=1 by/
134 | cases L -L
135   [ #i #HG #HL #HT #f #H destruct -IH
136     elim (frees_inv_atom … H) -H #g #Hg #H destruct /2 width=1 by/
137   | #L #I * [ cases I -I #I [ | #V ] | #i ] #HG #HL #HT #f #H destruct
138     [ elim (frees_inv_unit … H) -H #g #Hg #H destruct /2 width=1 by/
139     | elim (frees_inv_pair … H) -H #g #Hg #H destruct
140       /4 width=2 by fqu_fqup, fqu_lref_O/
141     | elim (frees_inv_lref … H) -H #g #Hg #H destruct
142       /4 width=2 by fqu_fqup/
143     ]
144   ]
145 | #l #HG #HL #HT #f #H destruct -IH
146   lapply (frees_inv_gref … H) -H /2 width=1 by/
147 | #p #I #V #T #HG #HL #HT #f #H destruct
148   elim (frees_inv_bind_void … H) -H /3 width=7 by/
149 | #I #V #T #HG #HL #HT #f #H destruct
150   elim (frees_inv_flat … H) -H /3 width=7 by/
151 ]
152 qed-.