diff options
author | Andres Erbsen <andreser@mit.edu> | 2019-01-08 04:21:38 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2019-01-09 22:49:02 -0500 |
commit | 3ca227f1137e6a3b65bc33f5689e1c230d591595 (patch) | |
tree | e1e5a2dd2a2f34f239d3276227ddbdc69eeeb667 /src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | |
parent | 3ec21c64b3682465ca8e159a187689b207c71de4 (diff) |
remove old pipeline
Diffstat (limited to 'src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v')
-rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v deleted file mode 100644 index 1217cd721..000000000 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v +++ /dev/null @@ -1,48 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Relations. -Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.InterpSideConditions. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy. -Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast. -Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. -Require Import Crypto.Util.PointedProp. - -Lemma MapCastCorrect - {round_up} - {t} (e : Expr t) - (Hwf : Wf e) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) - v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e v)), - Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b - /\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v) - /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v). -Proof. - apply MapCastCorrect; auto. - { apply is_bounded_by_interp_op. } - { apply pull_cast_genericize_op, is_bounded_by_interp_op. } -Qed. - -Lemma MapCastCorrect_eq - {round_up} - {t} (e : Expr t) - {evb ev} - (Hwf : Wf e) - (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) - : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) - v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) - (Hside : to_prop (InterpSideConditions e v)) - (Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds) - (Hev : ev = Compilers.Syntax.Interp interp_op e v), - evb = b - /\ Bounds.is_bounded_by b ev - /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev. -Proof. - intros; subst; apply MapCastCorrect; auto. -Qed. |