Add more context proper lemmas

1 files changed, 95 insertions, 0 deletions

diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v
index 0827ae233..48cecde8f 100644
--- a/src/Compilers/Named/ContextProperties/Proper.v
+++ b/src/Compilers/Named/ContextProperties/Proper.v
@@ -1,8 +1,13 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.DestructHead.
 
 Section with_context.
   Context {base_type_code}
@@ -16,6 +21,9 @@ Section with_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).
+  Local Notation extend := (@extend base_type_code Name var Context).
+  Local Notation remove := (@remove base_type_code Name var Context).
+  Local Notation lookup := (@lookup base_type_code Name var Context).
 
   Global Instance context_equiv_Equivalence : Equivalence context_equiv | 10.
   Proof. split; repeat intro; congruence. Qed.
@@ -43,4 +51,91 @@ Section with_context.
   Qed.
   Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
   Proof. repeat intro; subst; auto. Qed.
+
+  Local Ltac proper_t2 t :=
+    let IHt1 := fresh "IHt1" in
+    let IHt2 := fresh "IHt2" in
+    induction t as [ | | ? IHt1 ? IHt2];
+    simpl;
+    repeat match goal with
+           | [ |- context[fun a b => ?f a b] ]
+             => change (fun a b => f a b) with f
+           end;
+    [ try exact _
+    | repeat intro; auto
+    | repeat intro; subst;
+      destruct_head_prod;
+      first [ eapply IHt2; [ eapply IHt1 | .. ]; auto
+            | idtac ] ].
+
+  Global Instance extend_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10.
+  Proof. proper_t2 t. Qed.
+  Global Instance remove_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10.
+  Proof. proper_t2 t. Qed.
+  Global Instance lookup_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10.
+  Proof.
+    proper_t2 t.
+    repeat match goal with
+           | [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ]
+             => let G' := context G[match lookup A ctx na, lookup B ctx nb with
+                                    | Some a, Some b => Some (a, b)
+                                    | _, _ => None
+                                    end] in
+                change G'
+           end.
+    break_innermost_match;
+      repeat match goal with
+             | _ => progress subst
+             | _ => progress inversion_option
+             | _ => reflexivity
+             | [ H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ]
+               => assert (x = y)
+                 by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity));
+                    clear H H'
+             end.
+  Qed.
 End with_context.
+
+Section language.
+  Context {base_type_code}
+          {base_type_code_dec : DecidableRel (@eq base_type_code)}
+          {Name}
+          {Name_dec : DecidableRel (@eq Name)}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {interp_base_type : base_type_code -> Type}
+          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}
+          {Context : @Context base_type_code Name interp_base_type}
+          {ContextOk : ContextOk Context}.
+
+  Local Notation context_equiv := (@context_equiv base_type_code Name interp_base_type Context).
+  Local Notation interpf := (@interpf base_type_code interp_base_type op Name Context interp_op).
+  Local Notation interp := (@interp base_type_code interp_base_type op Name Context interp_op).
+
+  Global Instance interpf_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@interpf t).
+  Proof.
+    intros c0 c1 Hc e e' ?; subst e'; revert c0 c1 Hc.
+    induction e;
+      repeat first [ progress subst
+                   | reflexivity
+                   | progress inversion_option
+                   | progress simpl in *
+                   | progress unfold LetIn.Let_In
+                   | intros; eapply lookupb_Proper; (assumption || reflexivity)
+                   | intros; eapply extendb_Proper; (assumption || reflexivity)
+                   | intros; eapply lookup_Proper; (assumption || reflexivity)
+                   | intros; eapply extend_Proper; (assumption || reflexivity)
+                   | intros; erewrite_hyp *; [ | eassumption ]
+                   | intros; erewrite_hyp *; [ reflexivity | ]
+                   | break_innermost_match_step
+                   | match goal with
+                     | [ H : interpf _ = ?x, H' : interpf _ = ?y |- _ ]
+                       => assert (x = y) by (rewrite <- H, <- H'; eauto); clear H H'
+                     end ].
+  Qed.
+
+  Global Instance interp_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> eq) (@interp t).
+  Proof.
+    intros ??? e e' ????; subst e'; subst.
+    eapply interpf_Proper; [ eapply extend_Proper; auto | reflexivity ].
+  Qed.
+End language.