From 5aef9a66966c8aa97041461d618b601e60e56c91 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 02:13:26 +0200
Subject: Be consistent in notation of simplify_eq/=
---
maptools.v | 8 ++++----
semprop.v | 2 +-
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}
Proof.
intros Hiel.
destruct (decide (i = j)).
- - split; try done. simplify_eq /=.
+ - split; try done. simplify_eq/=.
rewrite lookup_insert in Hiel. congruence.
- rewrite lookup_insert_ne in Hiel; try done.
exfalso. eapply lookup_empty_Some, Hiel.
@@ -259,7 +259,7 @@ Proof.
case_match.
- case_match; try done.
rewrite lookup_insert in H8. rewrite lookup_insert in H9.
- simplify_eq /=. split; try done.
+ simplify_eq/=. split; try done.
unfold map_Forall2, map_relation, option_relation.
intros j.
destruct (decide (i = j)).
@@ -275,7 +275,7 @@ Proof.
case_match; case_match; try done;
rewrite lookup_insert_ne in H11 by done;
rewrite lookup_insert_ne in H12 by done;
- by simplify_eq /=.
+ by simplify_eq/=.
- by rewrite lookup_insert in H8.
Qed.
@@ -305,7 +305,7 @@ Proof.
pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15.
- intros HForall2.
apply map_Forall2_destruct in HForall2 as Hm2.
- destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq /=.
+ destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq/=.
apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done.
set_solver.
Qed.
diff --git a/semprop.v b/semprop.v
index 2fe30af..7ab0707 100644
--- a/semprop.v
+++ b/semprop.v
@@ -42,7 +42,7 @@ Proof.
- exfalso. apply H. by exists bs.
- f_equal. by eapply matches_deterministic.
- apply map_insert_inv in H0 as [H01 H02].
- by simplify_eq /=.
+ by simplify_eq/=.
- f_equal. by eapply binop_deterministic.
- rewrite H4 in H. by apply is_Some_None in H.
- exfalso. apply H4. by exists bs.
--
cgit v1.2.3