]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/reqg_fqus.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / reqg_fqus.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/fqus_fqup.ma".
16 include "static_2/static/reqg_drops.ma".
17 include "static_2/static/reqg_fqup.ma".
18 include "static_2/static/reqg_reqg.ma".
19
20 (* GENERIC  EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES **********)
21
22 (* Properties with extended structural successor for closures ***************)
23
24 lemma fqu_teqg_conf (S) (b):
25       reflexive … S →
26       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂[b] ❨G2,L2,T1❩ →
27       ∀U2. U1 ≛[S] U2 →
28       ∃∃L,T2. ❨G1,L1,U2❩ ⬂[b] ❨G2,L,T2❩ & L2 ≛[S,T1] L & T1 ≛[S] T2.
29 #S #b #HS #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
30 [ #I #G #L #W #X #H >(teqg_inv_lref1 … H) -X
31   /3 width=5 by reqg_refl, fqu_lref_O, teqg_refl, ex3_2_intro/
32 | #I #G #L #W1 #U1 #X #H
33   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct
34   /3 width=5 by reqg_refl, fqu_pair_sn, ex3_2_intro/
35 | #p #I #G #L #W1 #U1 #Hb #X #H
36   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
37   /3 width=5 by reqg_pair_refl, fqu_bind_dx, ex3_2_intro/
38 | #p #I #G #L #W1 #U1 #Hb #X #H
39   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
40   /3 width=5 by reqg_refl, fqu_clear, ex3_2_intro/
41 | #I #G #L #W1 #U1 #X #H
42   elim (teqg_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
43   /3 width=5 by reqg_refl, fqu_flat_dx, ex3_2_intro/
44 | #I #G #L #T1 #U1 #HTU1 #U2 #HU12
45   elim (teqg_inv_lifts_sn … HU12 … HTU1) -U1
46   /3 width=5 by reqg_refl, fqu_drop, ex3_2_intro/
47 ]
48 qed-.
49
50 lemma teqg_fqu_trans (S) (b):
51       reflexive … S → symmetric … S →
52       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂[b] ❨G2,L2,T1❩ →
53       ∀U2. U2 ≛[S] U1 →
54       ∃∃L,T2. ❨G1,L1,U2❩ ⬂[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
55 #S #b #H1S #H2S #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
56 elim (fqu_teqg_conf … H12 U2) -H12
57 /3 width=5 by reqg_sym, teqg_sym, ex3_2_intro/
58 qed-.
59
60 (* Basic_2A1: uses: lleq_fqu_trans *)
61 lemma reqg_fqu_trans (S) (b):
62       reflexive … S →
63       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂[b] ❨G2,K2,U❩ →
64       ∀L1. L1 ≛[S,T] L2 →
65       ∃∃K1,U0. ❨G1,L1,T❩ ⬂[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
66 #S #b #HS #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
67 [ #I #G #L2 #V2 #L1 #H elim (reqg_inv_zero_pair_dx … H) -H
68   #K1 #V1 #HV1 #HV12 #H destruct
69   /3 width=9 by teqg_reqg_conf_sn, fqu_lref_O, ex3_2_intro/
70 | * [ #p ] #I #G #L2 #V #T #L1 #H
71   [ elim (reqg_inv_bind_refl … H)
72   | elim (reqg_inv_flat … H)
73   ] -H
74   /3 width=5 by fqu_pair_sn, teqg_refl, ex3_2_intro/
75 | #p #I #G #L2 #V #T #Hb #L1 #H elim (reqg_inv_bind_refl … H) -H
76   /3 width=5 by fqu_bind_dx, teqg_refl, ex3_2_intro/
77 | #p #I #G #L2 #V #T #Hb #L1 #H elim (reqg_inv_bind_void … H) -H
78   /3 width=5 by fqu_clear, teqg_refl, ex3_2_intro/
79 | #I #G #L2 #V #T #L1 #H elim (reqg_inv_flat … H) -H
80   /3 width=5 by fqu_flat_dx, teqg_refl, ex3_2_intro/
81 | #I #G #L2 #T #U #HTU #Y #HU
82   elim (reqg_fwd_dx … HU) #L1 #V1 #H destruct
83   /5 width=14 by reqg_inv_lifts_bi, fqu_drop, teqg_refl, drops_refl, drops_drop, ex3_2_intro/
84 ]
85 qed-.
86
87 (* Properties with optional structural successor for closures ***************)
88
89 lemma teqg_fquq_trans (S) (b):
90       reflexive … S → symmetric … S →
91       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂⸮[b] ❨G2,L2,T1❩ →
92       ∀U2. U2 ≛[S] U1 →
93       ∃∃L,T2. ❨G1,L1,U2❩ ⬂⸮[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
94 #S #b #H1S #H2S #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H
95 [ #H #U2 #HU21 elim (teqg_fqu_trans … H … HU21) -U1
96   /3 width=5 by fqu_fquq, ex3_2_intro/
97 | * #HG #HL #HT destruct /3 width=5 by reqg_refl, ex3_2_intro/
98 ]
99 qed-.
100
101 (* Basic_2A1: was just: lleq_fquq_trans *)
102 lemma reqg_fquq_trans (S) (b):
103       reflexive … S →
104       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂⸮[b] ❨G2,K2,U❩ →
105       ∀L1. L1 ≛[S,T] L2 →
106       ∃∃K1,U0. ❨G1,L1,T❩ ⬂⸮[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
107 #S #b #HS #G1 #G2 #L2 #K2 #T #U #H elim H -H
108 [ #H #L1 #HL12 elim (reqg_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
109 | * #HG #HL #HT destruct /3 width=5 by teqg_refl, ex3_2_intro/
110 ]
111 qed-.
112
113 (* Properties with plus-iterated structural successor for closures **********)
114
115 (* Basic_2A1: was just: lleq_fqup_trans *)
116 lemma reqg_fqup_trans (S) (b):
117       reflexive … S → symmetric … S → Transitive … S →
118       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂+[b] ❨G2,K2,U❩ →
119       ∀L1. L1 ≛[S,T] L2 →
120       ∃∃K1,U0. ❨G1,L1,T❩ ⬂+[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
121 #S #b #H1S #H2S #H3S #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
122 [ #G2 #K2 #U #HTU #L1 #HL12 elim (reqg_fqu_trans … HTU … HL12) -L2
123   /3 width=5 by fqu_fqup, ex3_2_intro/
124 | #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12
125   elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0
126   elim (reqg_fqu_trans … HU2 … HK0) -K // #K1 #U1 #HU1 #HU12 #HK12
127   elim (teqg_fqu_trans … HU1 … HU0) -U // #K3 #U3 #HU03 #HU31 #HK31
128   @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
129   /3 width=5 by reqg_trans, teqg_reqg_conf_sn, fqup_strap1, teqg_trans/
130 ]
131 qed-.
132
133 lemma teqg_fqup_trans (S) (b):
134       reflexive … S → symmetric … S → Transitive … S →
135       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂+[b] ❨G2,L2,T1❩ →
136       ∀U2. U2 ≛[S] U1 →
137       ∃∃L,T2. ❨G1,L1,U2❩ ⬂+[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
138 #S #b #H1S #H2S #H3S #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1
139 [ #G1 #L1 #U1 #H #U2 #HU21 elim (teqg_fqu_trans … H … HU21) -U1 //
140   /3 width=5 by fqu_fqup, ex3_2_intro/
141 | #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21
142   elim (teqg_fqu_trans … H … HU21) -U1 // #L0 #T #H1 #HTU #HL0
143   lapply (teqg_reqg_div … HTU … HL0) -HL0 // #HL0
144   elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2
145   elim (reqg_fqup_trans … H2 … HL0) -L // #K #U #H2 #HU1 #HK2
146   lapply (teqg_reqg_conf_sn … HUT1 … HK2) -HK2 // #HK2
147   /3 width=7 by reqg_trans, fqup_strap2, teqg_trans, ex3_2_intro/
148 ]
149 qed-.
150
151 (* Properties with star-iterated structural successor for closures **********)
152
153 lemma teqg_fqus_trans (S) (b):
154       reflexive … S → symmetric … S → Transitive … S →
155       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂*[b] ❨G2,L2,T1❩ →
156       ∀U2. U2 ≛[S] U1 →
157       ∃∃L,T2. ❨G1,L1,U2❩ ⬂*[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
158 #S #b #H1S #H2S #H3S #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H
159 [ #H elim (teqg_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/
160 | * #HG #HL #HT destruct /3 width=5 by reqg_refl, ex3_2_intro/
161 ]
162 qed-.
163
164 (* Basic_2A1: was just: lleq_fqus_trans *)
165 lemma reqg_fqus_trans (S) (b):
166       reflexive … S → symmetric … S → Transitive … S →
167       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂*[b] ❨G2,K2,U❩ →
168       ∀L1. L1 ≛[S,T] L2 →
169       ∃∃K1,U0. ❨G1,L1,T❩ ⬂*[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
170 #S #b #H1S #H2S #H3S #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
171 [ #H elim (reqg_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
172 | * #HG #HL #HT destruct /3 width=5 by teqg_refl, ex3_2_intro/
173 ]
174 qed-.