Add snd_interpf_side_conditions_gen_Some

1 files changed, 45 insertions, 0 deletions

diff --git a/src/Compilers/Named/InterpSideConditionsInterp.v b/src/Compilers/Named/InterpSideConditionsInterp.v
new file mode 100644
index 000000000..72bb9c9e0
--- /dev/null
+++ b/src/Compilers/Named/InterpSideConditionsInterp.v
@@ -0,0 +1,45 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Named.InterpSideConditions.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Option.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {Name : Type}
+          {interp_base_type : base_type_code -> Type}
+          {Context : Context Name interp_base_type}
+          {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
+          {interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop}.
+
+  Local Notation exprf := (@exprf base_type_code op Name).
+  Local Notation expr := (@expr base_type_code op Name).
+
+  Lemma snd_interpf_side_conditions_gen_eq {t} {ctx : Context} {e}
+    : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e
+      = option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e).
+  Proof.
+    revert ctx; induction e; intros;
+      repeat first [ reflexivity
+                   | progress subst
+                   | progress inversion_option
+                   | progress unfold option_map, LetIn.Let_In in *
+                   | break_innermost_match_step
+                   | break_innermost_match_hyps_step
+                   | progress simpl in *
+                   | match goal with
+                     | [ H : forall ctx, interpf ?e = _, H' : context[interpf ?e] |- _ ]
+                       => rewrite H in H'
+                     | [ H : forall ctx, interpf ?e = _ |- context[interpf ?e] ]
+                       => rewrite H
+                     end ].
+  Qed.
+  Lemma snd_interpf_side_conditions_gen_Some {t} {ctx : Context} {e v}
+    : interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e = Some v
+      <-> option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e) = Some v.
+  Proof. rewrite snd_interpf_side_conditions_gen_eq; reflexivity. Qed.
+End language.