diff options
-rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Composition.v | 11 | ||||
-rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v | 373 |
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. |