aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Rutger Broekhoff2024-06-27 02:13:26 +0200
committerLibravatar Rutger Broekhoff2024-06-27 02:13:26 +0200
commit5aef9a66966c8aa97041461d618b601e60e56c91 (patch)
treee437f49b12ad069731d61f6b95227de60d9ff88d
parentba973b2fa09e0ff203eec9770908a88e0ccfde70 (diff)
downloadmininix-formalization-5aef9a66966c8aa97041461d618b601e60e56c91.tar.gz
mininix-formalization-5aef9a66966c8aa97041461d618b601e60e56c91.zip
Be consistent in notation of simplify_eq/=
-rw-r--r--maptools.v8
-rw-r--r--semprop.v2
2 files changed, 5 insertions, 5 deletions
diff --git a/maptools.v b/maptools.v
index ce4022a..01e24c0 100644
--- a/maptools.v
+++ b/maptools.v
@@ -9,7 +9,7 @@ Lemma map_insert_empty_lookup {A} `{FinMap K M}
9Proof. 9Proof.
10 intros Hiel. 10 intros Hiel.
11 destruct (decide (i = j)). 11 destruct (decide (i = j)).
12 - split; try done. simplify_eq /=. 12 - split; try done. simplify_eq/=.
13 rewrite lookup_insert in Hiel. congruence. 13 rewrite lookup_insert in Hiel. congruence.
14 - rewrite lookup_insert_ne in Hiel; try done. 14 - rewrite lookup_insert_ne in Hiel; try done.
15 exfalso. eapply lookup_empty_Some, Hiel. 15 exfalso. eapply lookup_empty_Some, Hiel.
@@ -259,7 +259,7 @@ Proof.
259 case_match. 259 case_match.
260 - case_match; try done. 260 - case_match; try done.
261 rewrite lookup_insert in H8. rewrite lookup_insert in H9. 261 rewrite lookup_insert in H8. rewrite lookup_insert in H9.
262 simplify_eq /=. split; try done. 262 simplify_eq/=. split; try done.
263 unfold map_Forall2, map_relation, option_relation. 263 unfold map_Forall2, map_relation, option_relation.
264 intros j. 264 intros j.
265 destruct (decide (i = j)). 265 destruct (decide (i = j)).
@@ -275,7 +275,7 @@ Proof.
275 case_match; case_match; try done; 275 case_match; case_match; try done;
276 rewrite lookup_insert_ne in H11 by done; 276 rewrite lookup_insert_ne in H11 by done;
277 rewrite lookup_insert_ne in H12 by done; 277 rewrite lookup_insert_ne in H12 by done;
278 by simplify_eq /=. 278 by simplify_eq/=.
279 - by rewrite lookup_insert in H8. 279 - by rewrite lookup_insert in H8.
280Qed. 280Qed.
281 281
@@ -305,7 +305,7 @@ Proof.
305 pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15. 305 pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15.
306 - intros HForall2. 306 - intros HForall2.
307 apply map_Forall2_destruct in HForall2 as Hm2. 307 apply map_Forall2_destruct in HForall2 as Hm2.
308 destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq /=. 308 destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq/=.
309 apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done. 309 apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done.
310 set_solver. 310 set_solver.
311Qed. 311Qed.
diff --git a/semprop.v b/semprop.v
index 2fe30af..7ab0707 100644
--- a/semprop.v
+++ b/semprop.v
@@ -42,7 +42,7 @@ Proof.
42 - exfalso. apply H. by exists bs. 42 - exfalso. apply H. by exists bs.
43 - f_equal. by eapply matches_deterministic. 43 - f_equal. by eapply matches_deterministic.
44 - apply map_insert_inv in H0 as [H01 H02]. 44 - apply map_insert_inv in H0 as [H01 H02].
45 by simplify_eq /=. 45 by simplify_eq/=.
46 - f_equal. by eapply binop_deterministic. 46 - f_equal. by eapply binop_deterministic.
47 - rewrite H4 in H. by apply is_Some_None in H. 47 - rewrite H4 in H. by apply is_Some_None in H.
48 - exfalso. apply H4. by exists bs. 48 - exfalso. apply H4. by exists bs.