Rework and doc reflective pipeline (more Gallina)

2 files changed, 177 insertions, 207 deletions

diff --git a/src/Reflection/Z/Bounds/Pipeline/Composition.v b/src/Reflection/Z/Bounds/Pipeline/Composition.v
index 120f8c84f..56939e4bd 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Composition.v
+++ b/src/Reflection/Z/Bounds/Pipeline/Composition.v
@@ -8,6 +8,7 @@ Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.WfReflectiveGen.
 Require Import Crypto.Reflection.WfReflective.
 Require Import Crypto.Reflection.Eta.
+Require Import Crypto.Reflection.EtaWf.
 Require Import Crypto.Reflection.EtaInterp.
 Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
 Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition.
@@ -40,13 +41,13 @@ Definition PipelineCorrect
            (** ** pre-wf pipeline *)
            (He : e = PreWfPipeline (proj1_sig rexpr_sig))
            (** ** proving wf *)
-           (He_unnatize_for_wf : forall var, unnatize_expr 0 (e (fun t => (nat * var t)%type)) = e _)
+           (He_unnatize_for_wf : forall var, unnatize_expr 0 (ExprEta' e (fun t => (nat * var t)%type)) = ExprEta' e _)
            (Hwf : forall var1 var2,
-               let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (e _) (e _)) in
+               let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (ExprEta' e _) (ExprEta' e _)) in
                trueify P = P)
            (** ** post-wf-pipeline *)
            (Hpost : e_pkg = PostWfPipeline e input_bounds)
-           (Hpost_correct : e_pkg = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |})
+           (Hpost_correct : Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg)
            (** ** renaming *)
            (Hrenaming : e_final = e')
            (** ** bounds relaxation *)
@@ -64,10 +65,12 @@ Definition PipelineCorrect
 Proof.
   destruct rexpr_sig as [? Hrexpr].
   assert (Hwf' : Wf e)
-    by (eapply reflect_Wf;
+    by (apply (proj1 (@Wf_ExprEta'_iff _ _ _ e));
+        eapply reflect_Wf;
         [ .. | intros; split; [ eapply He_unnatize_for_wf | rewrite <- Hwf; apply trueify_true ] ];
         auto using base_type_eq_semidec_is_dec, op_beq_bl).
   clear Hwf He_unnatize_for_wf.
+  symmetry in Hpost_correct.
   subst; cbv [proj1_sig] in *.
   rewrite <- Hrexpr.
   eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ].
diff --git a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
index bf78e5a3a..9670aec1f 100644
--- a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -22,8 +22,8 @@ Require Import Crypto.Reflection.Z.Bounds.Interpretation.
 Require Import Crypto.Reflection.Z.Bounds.Relax.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Z.Reify.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
 Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition.
+Require Import Crypto.Reflection.Z.Bounds.Pipeline.Composition.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.SubstLet.
 Require Import Crypto.Util.FixedWordSizes.
@@ -49,229 +49,196 @@ Module Export Exports.
   Export Crypto.Reflection.Z.Bounds.Pipeline.Definition.Exports.
 End Exports.
 
-(** ** Pre-reification *)
-(** The [assert_reflective] tactic is the first one that gets run, and
-    it takes a goal of the form
-<<
-@Bounds.is_bounded_by (codomain T) bounds _
-  /\ cast_back_flat_const fW = fZ (cast_back_flat_const v)
->>
-    where [fW] must be a context variable.  It creates a second goal
-    of the form [{ rexpr | forall x, Interp _ rexpr x = fZ x }], which
-    is what reification works on.  This goal is placed first, and in
-    the second (original) subgoal, [fZ] is replaced with the
-    interpretation of the evar which will be filled with the reflected
-    constant. *)
-Ltac assert_reflective :=
-  lazymatch goal with
-  | [ |- @Bounds.is_bounded_by (codomain ?T) ?bounds _
-         /\ cast_back_flat_const ?fW = ?fZ (cast_back_flat_const ?v) ]
-    => let rexpr := fresh "rexpr" in
-       simple refine (let rexpr : { rexpr | forall x, Interp interp_op (t:=T) rexpr x = fZ x } := _ in _);
-       [ cbv [interp_flat_type interp_base_type Tuple.tuple Tuple.tuple'] in *;
-         subst fW
-       | rewrite <- (proj2_sig rexpr);
-         let rexpr' := fresh rexpr in
-         set (rexpr' := proj1_sig rexpr);
-         unfold proj1_sig in rexpr';
-         subst rexpr fZ ]
-  end.
-
 (** ** Reification *)
-(** The [rexpr_cbv] tactic unfolds various constants in a goal of the
-    form
+(** The [do_reify] tactic handles goals of the form
 <<
-{ rexpr | forall x, Interp _ rexpr x = f x }
+forall x, Interp _ ?e x = F
 >>
-    to get the goal into a form that [eexists; Reify_rhs] can handle.
-    This tactic is somewhat more general than it currently needs to
-    be; it can handle cases where [f] is already unfolded, cases
-    where [f] is a definition or a context variable, and cases where
-    [f] is some sort of uncurrying functional applied to a context
-    variable, definition, or unfolded term.  In the old pipeline, it
-    needed to handle all of these cases. *)
-Ltac rexpr_cbv :=
-  lazymatch goal with
-  | [ |- { rexpr | forall x, Interp _ (t:=?T) rexpr x = ?uncurry ?oper x } ]
-    => let operf := head oper in
-       let uncurryf := head uncurry in
-       try cbv delta [T]; try cbv delta [oper];
-       try cbv beta iota delta [uncurryf]
-  | [ |- { rexpr | forall x, Interp _ (t:=?T) rexpr x = ?oper x } ]
-    => let operf := head oper in
-       try cbv delta [T]; try cbv delta [oper]
-  end;
-  cbv beta iota delta [interp_flat_type interp_base_type].
-(** The [reify_sig] tactic handles a goal of the form
+    by reifying [F]. *)
+Ltac do_reify :=
+  cbv beta iota delta [Syntax.interp_flat_type Syntax.interp_base_type];
+  Reify_rhs; reflexivity.
+(** ** Input Boundedness Side-Conditions *)
+(** The tactic [handle_bounds_from_hyps] handles goals of the form
 <<
-{ rexpr | forall x, Interp _ rexpr x = f x }
+Bounds.is_bounded_by (_, _, ..., _) _
 >>
-    by reifying [f]. *)
-Ltac reify_sig :=
-  rexpr_cbv; eexists; Reify_rhs; reflexivity.
-(** The [do_reify] tactic runs [reify_sig] on the first goal, and
-    then, in the second goal left by [assert_reflective], reduces
-    projections of the reified pair (which was an evar, and is now
-    instantiated). *)
-Ltac do_reify := [ > reify_sig | cbv beta iota in * ].
+     by splitting them apart and looking in the context for hypotheses
+     that prove the bounds. *)
+Ltac handle_bounds_from_hyps :=
+  repeat match goal with
+         | _ => assumption
+         | [ |- cast_back_flat_const _ = cast_back_flat_const _ ] => reflexivity
+         | [ |- _ /\ _ ] => split
+         | [ |- Bounds.is_bounded_by (_, _) _ ] => split
+         end.
+(** ** Unfolding [Interp] *)
+(** The reduction strategies [interp_red], [extra_interp_red], and
+    [constant_simplification] (the latter two defined in
+    Pipeline/Definition.v) define the constants that get unfolded
+    before instantiating the original evar with [Interp _
+    vm_computed_reified_expression arguments]. *)
+Declare Reduction interp_red
+  := cbv [fst snd
+              Interp InterpEta interp_op interp interp_eta interpf interpf_step
+              interp_flat_type_eta interp_flat_type_eta_gen interp_flat_type
+              interp_base_type interp_op
+              SmartMap.SmartFlatTypeMap SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2
+              SmartMap.smart_interp_flat_map
+              codomain domain
+              lift_op Zinterp_op cast_const
+              ZToInterp interpToZ
+         ].
 
-(** ** Post-reification, pre-Wf transformations *)
-(** The [do_pre_wf_pipeline] tactic runs the part of the pipeline,
-    defined in Pipeline.Definition, which does not rely on
-    well-foundedness.  It operates on a goal of the form
-<<
-Bounds.is_bounded_by bounds (Interp _ fZ v')
-  /\ cast_back_flat_const fW = Interp _ fZ v'
->>
-    where [fZ] is expected to be a context variable, and does not
-    change the shape of the goal (it updates the definition of [fZ]). *)
-Ltac do_pre_wf_pipeline :=
-  lazymatch goal with
-  | [ |- Bounds.is_bounded_by ?bounds (Interp _ ?fZ ?v')
-         /\ cast_back_flat_const ?fW = Interp _ ?fZ ?v' ]
-    => rewrite <- !(InterpPreWfPipeline fZ);
-       let fZ' := fresh fZ in
-       rename fZ into fZ';
-       set (fZ := PreWfPipeline fZ');
-       vm_compute in fZ; clear fZ'
-  end.
+(** ** Solving Side-Conditions of Equality *)
+(** This section defines a number of different ways to solve goals of
+    the form [LHS = RHS] where [LHS] may contain evars and [RHS] must
+    not contain evars.  Most tactics use [abstract] to reduce the load
+    on [Defined] and to catch looping behavior early. *)
 
-(** ** Well-foundedness *)
-(** The [assert_wf] tactic adds an opaque hypothesis of type [Wf fZ]
-    to the context, pulling [fZ] from a goal of the form
-<<
-Bounds.is_bounded_by _ _ /\ cast_back_flat_const fW = Interp _ fZ _
->>
- *)
-Ltac prove_rexpr_wfT
-  := reflect_Wf Equality.base_type_eq_semidec_is_dec Equality.op_beq_bl.
-Ltac assert_wf :=
+(** The tactic [abstract_vm_compute_rhs] unifies [LHS] with the result
+    of [vm_compute]ing [RHS], and costs two [vm_compute]s. *)
+Ltac abstract_vm_compute_rhs :=
+  intros; clear;
   lazymatch goal with
-  | [ |- Bounds.is_bounded_by _ _ /\ cast_back_flat_const ?fW = Interp _ ?fZ _ ]
-    => assert (Wf fZ) by (clear; prove_rexpr_wfT)
+  | [ |- ?LHS = ?RHS ]
+    => let RHS' := (eval vm_compute in RHS) in
+       unify LHS RHS'; clear;
+       abstract vm_cast_no_check (eq_refl RHS')
   end.
-
-(** ** Post-Wf pipeline *)
-Notation rexpr_post_wf_pipeline_option rexprZ rexpr_bounds
-  := (PostWfPipeline rexprZ rexpr_bounds)
-       (only parsing).
-Notation rexpr_post_wf_pipeline_postprocess1 v
-  := (invert_Some v)
-       (only parsing).
-Notation get_output_type v := (OutputType v) (only parsing).
-Notation get_bounds v := (@output_bounds v) (only parsing).
-Notation get_output_expr v := (@output_expr v) (only parsing).
-Notation rexpr_post_wf_pipeline_postprocess2 v
-  := (renamify v)
-       (only parsing).
-
-Notation rexpr_correct_and_bounded rexprZ rexprW input_bounds output_bounds rexprZ_Wf
-  := (fun v v' Hv
-      => proj2
-           (@PostWfPipelineCorrect
-              _ rexprZ input_bounds rexprZ_Wf
-              output_bounds rexprW
-              _
-              v v' Hv))
-       (only parsing).
-
-Ltac rexpr_correct_and_bounded_obligation_tac :=
-  intros; subst_let; clear;
+(** The tactic [abstract_vm_compute_rhs_no_evar] costs only one
+    [vm_compute] and proves only evar-free goals.  Best when the cost
+    of retypechecking [RHS] is small, or at least smaller than the
+    cost of retypechecking [LHS]. *)
+Ltac abstract_vm_compute_rhs_no_evar :=
+  intros; clear;
+  match goal with
+  | [ |- ?LHS = ?RHS ]
+    => abstract vm_cast_no_check (eq_refl RHS)
+  end.
+(** The tactic [abstract_rhs] unifies [LHS] with [RHS]. *)
+Ltac abstract_rhs :=
+  intros; clear;
   lazymatch goal with
-  | [ |- ?x = Some ?y ]
-    => abstract vm_cast_no_check (eq_refl (Some y))
-  | _ => vm_compute; constructor
+  | [ |- ?LHS = ?RHS ]
+    => unify LHS RHS; clear;
+       abstract exact_no_check (eq_refl RHS)
   end.
-
-
-Ltac make_correctness rexprZ bounds Hcorrectness :=
-  let rexprW_pkgo := (eval vm_compute in (rexpr_post_wf_pipeline_option rexprZ bounds)) in
-  let rexprW_pkg := (eval vm_compute in (rexpr_post_wf_pipeline_postprocess1 rexprW_pkgo)) in
-  let rexprT := constr:(get_output_type rexprW_pkg) in
-  let rexprW' := (eval vm_compute in (get_output_expr rexprW_pkg)) in
-  let rexprW := (eval cbv beta iota zeta in (rexpr_post_wf_pipeline_postprocess2 rexprW')) in
-  let rexpr_output_bounds := (eval vm_compute in (get_bounds rexprW_pkg)) in
-  let rexprZ_Wf := lazymatch goal with H : Wf rexprZ |- _ => H end in
-  simple refine (let Hcorrectness := rexpr_correct_and_bounded rexprZ rexprW bounds rexpr_output_bounds rexprZ_Wf in _);
-  [ rexpr_correct_and_bounded_obligation_tac.. | clearbody Hcorrectness ].
-Ltac do_pose_correctness Hcorrectness :=
+(** The tactic [renamify_rhs] calls [renamify] on [RHS] and unifies
+    that with [LHS]; and then costs one [vm_compute] to prove the
+    equality. *)
+Ltac renamify_rhs :=
+  intros; clear;
   lazymatch goal with
-  | [ |- @Bounds.is_bounded_by (codomain ?T) ?bounds _
-         /\ cast_back_flat_const ?fW = Interp _ ?fZ (@cast_back_flat_const _ _ _ ?input_bounds ?v) ]
-    => make_correctness fZ input_bounds Hcorrectness
+  | [ |- ?LHS = ?RHS ]
+    => let RHS' := renamify RHS in
+       unify LHS RHS';
+       clear; abstract vm_cast_no_check (eq_refl RHS')
   end.
-Ltac pretighten_bounds tighter_bounds :=
+(** The tactic [abstract_cbv_rhs] unfies [LHS] with the result of
+    running [cbv] in [RHS], and costs a [cbv] and a [vm_compute].  Use
+    this if you don't want to lose binder names or otherwise can't use
+    [vm_compute]. *)
+Ltac abstract_cbv_rhs :=
+  intros; clear;
   lazymatch goal with
-  | [ |- @Bounds.is_bounded_by ?t ?relaxed_bounds _ /\ cast_back_flat_const ?v = ?k ]
-    => simple refine (@relax_output_bounds t tighter_bounds relaxed_bounds _ v k _ _)
+  | [ |- ?LHS = ?RHS ]
+    => let RHS' := (eval cbv in RHS) in
+       unify LHS RHS';
+       clear; abstract vm_cast_no_check (eq_refl RHS')
   end.
-Ltac posttighten_bounds :=
-  [ > clear; vm_compute; reflexivity | unfold eq_rect | clear; abstract vm_cast_no_check (eq_refl true) ].
-Ltac pretighten_bounds_from_correctness Hcorrectness :=
-  cbv beta iota zeta in Hcorrectness;
-  lazymatch type of Hcorrectness with
-  | forall v v', _ -> Bounds.is_bounded_by ?tighter_bounds _ /\ _
-    => pretighten_bounds tighter_bounds
+(** The tactic [abstract_cbv_interp_rhs] runs the interpretation
+    reduction strategies in [RHS] and unifies the result with [LHS],
+    and does not use the vm (and hence does not fully reduce things,
+    which is important for efficiency). *)
+Ltac abstract_cbv_interp_rhs :=
+  intros; clear;
+  lazymatch goal with
+  | [ |- ?LHS = ?RHS ]
+    => let RHS' := (eval interp_red in RHS) in
+       let RHS' := (eval extra_interp_red in RHS') in
+       let RHS' := lazymatch do_constant_simplification with
+                   | true => (eval constant_simplification in RHS')
+                   | _ => RHS'
+                   end in
+       unify LHS RHS'; abstract exact_no_check (eq_refl RHS')
   end.
-Ltac tighten_bounds_from_correctness Hcorrectness :=
-  pretighten_bounds_from_correctness Hcorrectness; posttighten_bounds.
 
-Declare Reduction interp_red := cbv [Interp InterpEta interp_op interp interp_eta interpf interpf_step interp_flat_type_eta interp_flat_type_eta_gen SmartMap.SmartFlatTypeMap codomain domain interp_flat_type interp_base_type SmartMap.smart_interp_flat_map lift_op Zinterp_op SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2 fst snd cast_const ZToInterp interpToZ].
-(* hopefully separating this out into a separate tactic will make it
-   show up in the Ltac profile *)
-Ltac clear_then_abstract_reflexivity x :=
-  clear; abstract exact_no_check (eq_refl x).
-Ltac specialize_Hcorrectness Hcorrectness :=
+(** ** Assembling the Pipeline *)
+(** The tactic [refine_with_pipeline_correct] uses the
+    [PipelineCorrect] lemma to create side-conditions.  It assumes the
+    goal is in exactly the form given in the conclusion of the
+    [PipelineCorrect] lemma. *)
+Ltac refine_with_pipeline_correct :=
   lazymatch goal with
-  | [ |- @Bounds.is_bounded_by (codomain ?T) ?bounds (Interp _ ?fZ ?v')
-         /\ cast_back_flat_const ?fW = Interp _ ?fZ ?v' ]
-    => let v := lazymatch v' with cast_back_flat_const ?v => v end in
-       specialize (Hcorrectness v' v);
-       lazymatch type of Hcorrectness with
-       | ?T -> Bounds.is_bounded_by _ _
-               /\ cast_back_flat_const (@Interp ?base_type ?interp_base_type ?op ?interp_op ?fWT ?fW' ?args) = _
-         => cut T;
-            [ (let H := fresh in intro H; specialize (Hcorrectness H); clear H);
-              rewrite <- (@eq_InterpEta base_type interp_base_type op interp_op fWT fW' args) in Hcorrectness
-            | ]
-       end;
-       [ lazymatch type of Hcorrectness with
-           Bounds.is_bounded_by _ _ /\ cast_back_flat_const ?fW' = _
-           => let fWev := (eval cbv delta [fW] in fW) in
-              let fW'_orig := fW' in
-              let fW' := (eval interp_red in fW') in
-              let fW' := (eval extra_interp_red in fW') in
-              let fW' := lazymatch do_constant_simplification with
-                         | true => (eval constant_simplification in fW')
-                         | _ => fW'
-                         end in
-              unify fWev fW';
-              replace fW with fW'_orig by clear_then_abstract_reflexivity fW
-         end
-       | ]
-  end.
-Ltac handle_bounds_from_hyps :=
-  repeat match goal with
-         | _ => assumption
-         | [ |- cast_back_flat_const _ = cast_back_flat_const _ ] => reflexivity
-         | [ |- _ /\ _ ] => split
-         | [ |- Bounds.is_bounded_by (_, _) _ ] => split
-         end.
-Ltac do_post_wf_pipeline :=
-  let Hcorrectness := fresh "Hcorrectness" in
-  do_pose_correctness Hcorrectness;
-  tighten_bounds_from_correctness Hcorrectness;
-  specialize_Hcorrectness Hcorrectness;
-  [ exact Hcorrectness
-  | handle_bounds_from_hyps ].
+  | [ |- _ /\ ?castback ?fW = ?fZ ?arg ]
+    => let lem := open_constr:(@PipelineCorrect _ _ _ _ _ _ _ _ _ _ _ _) in
+       simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _);
+       subst fW fZ
+  end;
+  [ eexists
+  | cbv [proj1_sig].. ].
+(** The tactic [solve_side_conditions] uses the above
+    reduction-and-proving-equality tactics to prove the
+    side-conditions of [PipelineCorrect].  Which tactic to use was
+    chosen in the following way:
+
+    - The default is [abstract_vm_compute_rhs]
+
+    - If the goal has no evar, instead use
+      [abstract_vm_compute_rhs_no_evar] (it's faster)
+
+    - If the [RHS] is already in [vm_compute]d form, use
+      [abstract_rhs] (saves a needless [vm_compute] which would be a
+      costly no-op)
+
+    - If the proof needs to be transparent and there are no evars and
+      you want the user to see the fully [vm_compute]d term on error,
+      use [vm_compute; reflexivity]
+
+    - If the user should see an unreduced term and you're proving [_ =
+      true], use [abstract vm_cast_no_check (eq_refl true)]
+
+    - If you want to preserve binder names, use [abstract_cbv_rhs]
+
+    The other choices are tactics that are specialized to the specific
+    side-condition for which they are used (reification, boundedness
+    of input, reduction of [Interp], renaming). *)
+Ltac solve_side_conditions :=
+  [>
+   (** ** reification *)
+   do_reify |
+   (** ** pre-wf pipeline *)
+   abstract_vm_compute_rhs |
+   (** ** reflective wf side-condition 1 *)
+   abstract_vm_compute_rhs_no_evar |
+   (** ** reflective wf side-condition 2 *)
+   abstract_vm_compute_rhs_no_evar |
+   (** ** post-wf pipeline *)
+   abstract_vm_compute_rhs |
+   (** ** post-wf pipeline gives [Some _] *)
+   abstract_rhs |
+   (** ** renaming binders *)
+   renamify_rhs |
+   (** ** types computed from given output bounds are the same as types computed from computed output bounds *)
+   (** N.B. the proof must be exactly [eq_refl] because it's used in a
+            later goal and needs to reduce *)
+   subst_let; clear; vm_compute; reflexivity |
+   (** ** computed output bounds are not looser than the given output bounds *)
+   (** we do subst and we don't [vm_compute] first because we want to
+       get an error message that displays the bounds *)
+   subst_let; clear; abstract vm_cast_no_check (eq_refl true) |
+   (** ** removal of a cast across the equality proof above *)
+   abstract_cbv_rhs |
+   (** ** unfolding of [interp] constants *)
+   abstract_cbv_interp_rhs |
+   (** ** boundedness of inputs *)
+   abstract handle_bounds_from_hyps ].
+
 
 (** ** The Entire Pipeline *)
 (** The [do_reflective_pipeline] tactic solves a goal of the form that
     is described at the top of this file, and is the public interface
     of this file. *)
 Ltac do_reflective_pipeline :=
-  assert_reflective;
-  do_reify;
-  do_pre_wf_pipeline;
-  assert_wf;
-  do_post_wf_pipeline.
+  refine_with_pipeline_correct; solve_side_conditions.