Add context_equiv and prove some Proper lemmas

2 files changed, 49 insertions, 0 deletions

diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v
index 79a3f2f1c..010cf1fca 100644
--- a/src/Compilers/Named/ContextDefinitions.v
+++ b/src/Compilers/Named/ContextDefinitions.v
@@ -58,4 +58,7 @@ Section with_context.
       : forall (ctx : Context) n t t', lookupb t' (removeb t ctx n) n = None;
       lookupb_empty
       : forall n t, lookupb t (@empty _ _ _ Context) n = None }.
+
+  Definition context_equiv (a b : Context)
+    := forall n t, lookupb t a n = lookupb t b n.
 End with_context.
diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v
new file mode 100644
index 000000000..0827ae233
--- /dev/null
+++ b/src/Compilers/Named/ContextProperties/Proper.v
@@ -0,0 +1,46 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Util.Decidable.
+
+Section with_context.
+  Context {base_type_code}
+          {base_type_code_dec : DecidableRel (@eq base_type_code)}
+          {Name}
+          {Name_dec : DecidableRel (@eq Name)}
+          {var} {Context : @Context base_type_code Name var}
+          {ContextOk : ContextOk Context}.
+
+  Local Notation context_equiv := (@context_equiv base_type_code Name var Context).
+  Local Notation extendb := (@extendb base_type_code Name var Context).
+  Local Notation removeb := (@removeb base_type_code Name var Context).
+  Local Notation lookupb := (@lookupb base_type_code Name var Context).
+
+  Global Instance context_equiv_Equivalence : Equivalence context_equiv | 10.
+  Proof. split; repeat intro; congruence. Qed.
+  Global Instance context_equiv_Reflexive : Reflexive context_equiv | 10 := _.
+  Global Instance context_equiv_Symmetric : Symmetric context_equiv | 10 := _.
+  Global Instance context_equiv_Transitive : Transitive context_equiv | 10 := _.
+
+  Local Ltac proper_t n n' t t' :=
+    destruct (dec (n = n')), (dec (t = t')); subst;
+    repeat first [ reflexivity
+                 | rewrite lookupb_extendb_same by assumption
+                 | rewrite lookupb_extendb_different by assumption
+                 | rewrite lookupb_extendb_wrong_type by assumption
+                 | rewrite lookupb_removeb_same by assumption
+                 | rewrite lookupb_removeb_different by assumption
+                 | solve [ auto ] ].
+
+  Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10.
+  Proof.
+    intros ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'.
+  Qed.
+  Global Instance removeb_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10.
+  Proof.
+    intros ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'.
+  Qed.
+  Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
+  Proof. repeat intro; subst; auto. Qed.
+End with_context.