aboutsummaryrefslogtreecommitdiffstats
path: root/semprop.v
diff options
context:
space:
mode:
authorLibravatar Rutger Broekhoff2024-06-27 01:56:05 +0200
committerLibravatar Rutger Broekhoff2024-06-27 01:56:05 +0200
commit4598e77a9406d8040357c943a05dd1ab939932db (patch)
treee990beaa94803da3585547f22e186e8819f6a887 /semprop.v
parent73df1945b31c0beee88cf4476df4ccd09d31403b (diff)
downloadmininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.tar.gz
mininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.zip
Tidy up project
* Write README.md * Add LICENSE * Clean up some theorems and proofs
Diffstat (limited to 'semprop.v')
-rw-r--r--semprop.v197
1 files changed, 30 insertions, 167 deletions
diff --git a/semprop.v b/semprop.v
index 3af718d..2fe30af 100644
--- a/semprop.v
+++ b/semprop.v
@@ -77,173 +77,36 @@ Proof.
77 intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. 77 intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2.
78 - (* L: id, R: id *) left. by eapply base_step_deterministic. 78 - (* L: id, R: id *) left. by eapply base_step_deterministic.
79 - (* L: id, R: ∘ *) simplify_eq/=. 79 - (* L: id, R: ∘ *) simplify_eq/=.
80 inv H. 80 inv H; try inv select (_ -->base b12);
81 + inv Hbase1. 81 (inv select (is_ctx _ _ _);
82 * inv H0. 82 [inv select (b21 -->base b22)
83 -- inv Hbase2. 83 |inv select (is_ctx_item _ _ _)]).
84 -- inv H. 84 simplify_option_eq.
85 * inv H0. 85 destruct sv; try discriminate.
86 -- inv Hbase2. 86 exfalso. clear uf. simplify_option_eq.
87 -- inv H1. inv H. 87 apply fmap_insert_lookup in H1. simplify_option_eq.
88 + inv Hbase1. 88 revert bs0 x H H1 Heqo.
89 * inv H0. 89 induction H2; intros bs0 x H' H1 Heqo; [inv Hbase2|].
90 -- inv Hbase2. 90 simplify_option_eq.
91 -- inv H. 91 inv H. destruct H'; try discriminate.
92 * inv H0. 92 inv H1. apply fmap_insert_lookup in H0. simplify_option_eq.
93 -- inv Hbase2. 93 by eapply IHis_ctx.
94 -- inv H. 94 - (* L: ∘, R: id *) simplify_eq/=.
95 + inv Hbase1. 95 inv H; try inv select (_ -->base b22);
96 * inv H0. 96 (inv select (is_ctx _ _ _);
97 -- inv Hbase2. 97 [inv select (b11 -->base b12)
98 -- inv H. 98 |inv select (is_ctx_item _ _ _)]).
99 * inv H0. 99 clear IHHctx1.
100 -- inv Hbase2. 100 simplify_option_eq.
101 -- inv H1. 101 destruct sv; try discriminate.
102 + inv Hbase1. 102 exfalso. simplify_option_eq.
103 * inv H0. 103 apply fmap_insert_lookup in H0. simplify_option_eq.
104 -- inv Hbase2. 104 revert bs0 x H H0 Heqo.
105 -- inv H. 105 induction H1; intros bs0 x H' H0 Heqo; [inv Hbase1|].
106 * inv H0. 106 simplify_option_eq.
107 -- inv Hbase2. 107 inv H. destruct H'; try discriminate.
108 -- inv H1. 108 inv H0. apply fmap_insert_lookup in H2. simplify_option_eq.
109 * inv H0. 109 by eapply IHis_ctx.
110 -- inv Hbase2.
111 -- inv H1. inv H.
112 + inv Hbase1.
113 inv H0.
114 * inv Hbase2.
115 * inv H.
116 + inv Hbase1.
117 * inv H0.
118 -- inv Hbase2.
119 -- inv H.
120 * inv H0.
121 -- inv Hbase2.
122 -- inv H.
123 + inv Hbase1.
124 inv H0.
125 * inv Hbase2.
126 * inv H.
127 + inv Hbase1.
128 inv H0.
129 * inv Hbase2.
130 * inv H.
131 + inv Hbase1.
132 inv H0.
133 * inv Hbase2.
134 * inv H.
135 + inv Hbase1.
136 * inv H0.
137 -- inv Hbase2.
138 -- inv H1.
139 * inv H0.
140 -- inv Hbase2.
141 -- inv H1.
142 * inv H0.
143 -- inv Hbase2.
144 -- inv H1.
145 + inv Hbase1.
146 inv H0.
147 * inv Hbase2.
148 * inv H.
149 simplify_option_eq.
150 destruct sv; try discriminate.
151 exfalso. clear uf. simplify_option_eq.
152 apply fmap_insert_lookup in H1. simplify_option_eq.
153 revert bs0 x H H1 Heqo.
154 induction H2; intros bs0 x H' H1 Heqo.
155 -- inv Hbase2.
156 -- simplify_option_eq.
157 inv H. destruct H'; try discriminate.
158 inv H1. apply fmap_insert_lookup in H0. simplify_option_eq.
159 by eapply IHis_ctx.
160 + inv Hbase1.
161 - (* L: ∘, R: id *)
162 simplify_eq/=.
163 inv H.
164 + inv Hbase2.
165 * inv Hctx1.
166 -- inv Hbase1.
167 -- inv H.
168 * inv Hctx1.
169 -- inv Hbase1.
170 -- inv H0. inv H.
171 + inv Hbase2.
172 * inv Hctx1.
173 -- inv Hbase1.
174 -- inv H.
175 * inv Hctx1.
176 -- inv Hbase1.
177 -- inv H.
178 + inv Hbase2.
179 * inv Hctx1.
180 -- inv Hbase1.
181 -- inv H.
182 * inv Hctx1.
183 -- inv Hbase1.
184 -- inv H0.
185 + inv Hbase2.
186 * inv Hctx1.
187 -- inv Hbase1.
188 -- inv H.
189 * inv Hctx1.
190 -- inv Hbase1.
191 -- inv H0.
192 * inv Hctx1.
193 -- inv Hbase1.
194 -- inv H0. inv H.
195 + inv Hbase2.
196 inv Hctx1.
197 * inv Hbase1.
198 * inv H.
199 + inv Hbase2.
200 * inv Hctx1.
201 -- inv Hbase1.
202 -- inv H.
203 * inv Hctx1.
204 -- inv Hbase1.
205 -- inv H.
206 + inv Hbase2.
207 inv Hctx1.
208 * inv Hbase1.
209 * inv H.
210 + inv Hbase2.
211 inv Hctx1.
212 * inv Hbase1.
213 * inv H.
214 + inv Hbase2.
215 inv Hctx1.
216 * inv Hbase1.
217 * inv H.
218 + inv Hbase2.
219 * inv Hctx1.
220 -- inv Hbase1.
221 -- inv H0.
222 * inv Hctx1.
223 -- inv Hbase1.
224 -- inv H0.
225 * inv Hctx1.
226 -- inv Hbase1.
227 -- inv H0.
228 + inv Hbase2.
229 inv Hctx1.
230 * inv Hbase1.
231 * clear IHHctx1.
232 inv H.
233 simplify_option_eq.
234 destruct sv; try discriminate.
235 exfalso. simplify_option_eq.
236 apply fmap_insert_lookup in H0. simplify_option_eq.
237 revert bs0 x H H0 Heqo.
238 induction H1; intros bs0 x H' H0 Heqo.
239 -- inv Hbase1.
240 -- simplify_option_eq.
241 inv H. destruct H'; try discriminate.
242 inv H0. apply fmap_insert_lookup in H2. simplify_option_eq.
243 eapply IHis_ctx.
244 ++ apply H2.
245 ++ apply Heqo0.
246 + inv Hbase2.
247 - (* L: ∘, R: ∘ *) 110 - (* L: ∘, R: ∘ *)
248 simplify_option_eq. 111 simplify_option_eq.
249 inv H; inv H0. 112 inv H; inv H0.
generated by cgit v1.2.3 (git 2.45.2) at 2024-12-26 06:47:53 +0000