]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma
update in delayed-updating
[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / vpushs.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 "apps_2/notation/models/roplus_5.ma".
16 include "static_2/syntax/lenv.ma".
17 include "apps_2/models/veq.ma".
18
19 (* MULTIPLE PUSH FOR MODEL EVALUATIONS **************************************)
20
21 inductive vpushs (M) (gv) (lv): relation2 lenv (evaluation M) ≝
22 | vpushs_atom: vpushs M gv lv (⋆) lv
23 | vpushs_abbr: ∀v,d,K,V. vpushs M gv lv K v → ⟦V⟧[gv,v] = d → vpushs M gv lv (K.ⓓV) (⫯[0←d]v)
24 | vpushs_abst: ∀v,d,K,V. vpushs M gv lv K v → vpushs M gv lv (K.ⓛV) (⫯[0←d]v)
25 | vpushs_unit: ∀v,d,I,K. vpushs M gv lv K v → vpushs M gv lv (K.ⓤ[I]) (⫯[0←d]v)
26 | vpushs_repl: ∀v1,v2,L. vpushs M gv lv L v1 → v1 ≗ v2 → vpushs M gv lv L v2
27 .
28
29 interpretation "multiple push (model evaluation)"
30    'ROPlus M gv L lv v  = (vpushs M gv lv L v).
31
32 (* Basic inversion lemmas ***************************************************)
33
34 fact vpushs_inv_atom_aux (M) (gv) (lv): is_model M →
35                                         ∀v,L. L ⨁{M}[gv] lv ≘ v →
36                                         ⋆ = L → lv ≗ v.
37 #M #gv #lv #HM #v #L #H elim H -v -L
38 [ #_ /2 width=1 by veq_refl/
39 | #v #d #K #V #_ #_ #_ #H destruct
40 | #v #d #K #V #_ #_ #H destruct
41 | #v #d #I #K #_ #_ #H destruct
42 | #v1 #v2 #L #_ #Hv12 #IH #H destruct
43   /3 width=3 by veq_trans/
44 ]
45 qed-.
46
47 lemma vpushs_inv_atom (M) (gv) (lv): is_model M →
48                                      ∀v. ⋆ ⨁{M}[gv] lv ≘ v → lv ≗ v.
49 /2 width=4 by vpushs_inv_atom_aux/ qed-.
50
51 fact vpushs_inv_abbr_aux (M) (gv) (lv): is_model M →
52                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
53                                         ∀K,V. K.ⓓV = L →
54                                         ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
55 #M #gv #lv #HM #y #L #H elim H -y -L
56 [ #Y #X #H destruct
57 | #v #d #K #V #Hv #Hd #_ #Y #X #H destruct
58   /3 width=3 by veq_refl, ex2_intro/
59 | #v #d #K #V #_ #_ #Y #X #H destruct
60 | #v #d #I #K #_ #_ #Y #X #H destruct
61 | #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct
62   elim IH -IH [|*: // ] #v #Hv #Hv1
63   /3 width=5 by veq_trans, ex2_intro/
64 ]
65 qed-.
66
67 lemma vpushs_inv_abbr (M) (gv) (lv): is_model M →
68                                      ∀y,K,V. K.ⓓV ⨁{M}[gv] lv ≘ y →
69                                      ∃∃v. K ⨁[gv] lv ≘ v & ⫯[0←⟦V⟧[gv,v]]v ≗ y.
70 /2 width=3 by vpushs_inv_abbr_aux/ qed-.
71
72 fact vpushs_inv_abst_aux (M) (gv) (lv): is_model M →
73                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
74                                         ∀K,W. K.ⓛW = L →
75                                         ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
76 #M #gv #lv #HM #y #L #H elim H -y -L
77 [ #Y #X #H destruct
78 | #v #d #K #V #_ #_ #_ #Y #X #H destruct
79 | #v #d #K #V #Hv #_ #Y #X #H destruct
80   /3 width=4 by veq_refl, ex2_2_intro/
81 | #v #d #I #K #_ #_ #Y #X #H destruct
82 | #v1 #v2 #L #_ #Hv12 #IH #Y #X #H destruct
83   elim IH -IH [|*: // ] #v #d #Hv #Hv1
84   /3 width=6 by veq_trans, ex2_2_intro/
85 ]
86 qed-.
87
88 lemma vpushs_inv_abst (M) (gv) (lv): is_model M →
89                                      ∀y,K,W. K.ⓛW ⨁{M}[gv] lv ≘ y →
90                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
91 /2 width=4 by vpushs_inv_abst_aux/ qed-.
92
93 fact vpushs_inv_unit_aux (M) (gv) (lv): is_model M →
94                                         ∀y,L. L ⨁{M}[gv] lv ≘ y →
95                                         ∀I,K. K.ⓤ[I] = L →
96                                         ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
97 #M #gv #lv #HM #y #L #H elim H -y -L
98 [ #Z #Y #H destruct
99 | #v #d #K #V #_ #_ #_ #Z #Y #H destruct
100 | #v #d #K #V #_ #_ #Z #Y #H destruct
101 | #v #d #I #K #Hv #_ #Z #Y #H destruct
102   /3 width=4 by veq_refl, ex2_2_intro/
103 | #v1 #v2 #L #_ #Hv12 #IH #Z #Y #H destruct
104   elim IH -IH [|*: // ] #v #d #Hv #Hv1
105   /3 width=6 by veq_trans, ex2_2_intro/
106 ]
107 qed-.
108
109 lemma vpushs_inv_unit (M) (gv) (lv): is_model M →
110                                      ∀y,I,K. K.ⓤ[I] ⨁{M}[gv] lv ≘ y →
111                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
112 /2 width=4 by vpushs_inv_unit_aux/ qed-.
113
114 (* Basic forward lemmas *****************************************************)
115
116 lemma vpushs_fwd_bind (M) (gv) (lv): is_model M →
117                                      ∀y,I,K. K.ⓘ[I] ⨁{M}[gv] lv ≘ y →
118                                      ∃∃v,d. K ⨁[gv] lv ≘ v & ⫯[0←d]v ≗ y.
119 #M #gv #lv #HM #y * [ #I | * #V ] #L #H
120 [ /2 width=2 by vpushs_inv_unit/
121 | elim (vpushs_inv_abbr … H) // -H #v #HL #Hv
122   /2 width=4 by ex2_2_intro/
123 | /2 width=2 by vpushs_inv_abst/
124 ]
125 qed-.