Add Interp{ExprEta,Linearize}_ind

2 files changed, 24 insertions, 0 deletions

diff --git a/src/Compilers/EtaInterp.v b/src/Compilers/EtaInterp.v
index f59024b98..2b6bd9b86 100644
--- a/src/Compilers/EtaInterp.v
+++ b/src/Compilers/EtaInterp.v
@@ -94,6 +94,19 @@ Section language.
     : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x.
   Proof using Type. exact (@InterpExprEta' (Arrow s d) e). Qed.
 
+  Lemma InterpExprEta_ind {t} (P : _ -> Prop) {e x}
+    : P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta (t:=t) e) x).
+  Proof using Type. rewrite InterpExprEta; exact id. Qed.
+  Lemma InterpExprEta'_ind {t} (P : _ -> Prop) {e x}
+    : P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta' (t:=t) e) x).
+  Proof using Type. rewrite InterpExprEta'; exact id. Qed.
+  Lemma InterpExprEta_arrow_ind {s d} (P : _ -> Prop) {e x}
+    : P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x).
+  Proof using Type. rewrite InterpExprEta_arrow; exact id. Qed.
+  Lemma InterpExprEta'_arrow_ind {s d} (P : _ -> Prop) {e x}
+    : P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x).
+  Proof using Type. rewrite InterpExprEta'_arrow; exact id. Qed.
+
   Lemma eq_interp_eta {t e}
     : forall x, interp_eta interp_op (t:=t) e x = interp interp_op e x.
   Proof using Type. apply eq_interp_flat_type_eta. Qed.
diff --git a/src/Compilers/LinearizeInterp.v b/src/Compilers/LinearizeInterp.v
index 750d14da6..c22fc26a3 100644
--- a/src/Compilers/LinearizeInterp.v
+++ b/src/Compilers/LinearizeInterp.v
@@ -97,6 +97,10 @@ Section language.
       unfold Interp, Linearize_gen.
       eapply interp_linearize_gen.
     Qed.
+
+    Lemma InterpLinearize_gen_ind {t} (P : _ -> Prop) {e : Expr t} {x}
+      : P (Interp interp_op e x) -> P (Interp interp_op (Linearize_gen let_bind_op_args e) x).
+    Proof using Type. rewrite InterpLinearize_gen; exact id. Qed.
   End gen.
 
   Definition interpf_linearizef {t} e
@@ -119,6 +123,13 @@ Section language.
   Definition InterpANormal {t} (e : Expr t)
     : forall x, Interp interp_op (ANormal e) x = Interp interp_op e x
     := InterpLinearize_gen _ e.
+
+  Definition InterpLinearize_ind {t} (P : _ -> Prop) {e : Expr t} {x}
+    : P (Interp interp_op e x) -> P (Interp interp_op (Linearize e) x)
+    := InterpLinearize_gen_ind _ P.
+  Definition InterpANormal_ind {t} (P : _ -> Prop) {e : Expr t} {x}
+    : P (Interp interp_op e x) -> P (Interp interp_op (ANormal e) x)
+    := InterpLinearize_gen_ind _ P.
 End language.
 
 Hint Rewrite @interpf_under_letsf : reflective_interp.