diff options
Diffstat (limited to 'src/RewriterRulesInterpGood.v')
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 1064 |
1 files changed, 252 insertions, 812 deletions
diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index c73867339..6ff9ef672 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -11,33 +11,11 @@ Require Import Crypto.UnderLetsProofs. Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. Require Import Crypto.Rewriter. Require Import Crypto.RewriterWf1. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Hints. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.ZSimplify.Core. -Require Import Crypto.Util.ZUtil.ZSimplify. -Require Import Crypto.Util.ZUtil.ZSimplify.Simple. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.AddGetCarry. -Require Import Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Zselect. -Require Import Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. -Require Import Crypto.Util.ZRange.BasicLemmas. -Require Import Crypto.Util.ZRange.OperationsBounds. -Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier. +Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Bool. Require Import Crypto.Util.ListUtil. @@ -45,7 +23,6 @@ Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.ListUtil.ForallIn. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Option. -Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. Import ListNotations. Local Open Scope list_scope. @@ -70,81 +47,81 @@ Module Compilers. Context {cast_outside_of_range : zrange -> Z -> Z}. Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). - - Local Lemma rlist_rect_eq {var A P ivar} Pnil Pcons ls - : @rlist_rect var A P ivar Pnil Pcons ls - = match invert_expr.reflect_list ls with - | Some ls - => Some (list_rect - (fun _ => _) - Pnil - (fun x xs rec => rec' <-- rec; Pcons x xs rec') - ls)%under_lets - | None => None - end. - Proof. cbv [rlist_rect Compile.option_bind' Option.bind]; reflexivity. Qed. - - Local Lemma UnderLets_interp_list_rect {A P} Pnil Pcons ls - : UnderLets.interp - (@ident_interp) - (list_rect - (fun _ : list A => UnderLets.UnderLets base.type ident _ P) - Pnil - (fun x xs rec => rec' <-- rec; Pcons x xs rec') - ls)%under_lets - = list_rect - (fun _ => P) - (UnderLets.interp (@ident_interp) Pnil) - (fun x xs rec => UnderLets.interp (@ident_interp) (Pcons x xs rec)) - ls. - Proof. - induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ]. - rewrite UnderLets.interp_splice, IHxs; reflexivity. - Qed. - - Local Lemma unfold_is_bounded_by_bool v r - : is_bounded_by_bool v r = true -> lower r <= v <= upper r. - Proof using Type. - cbv [is_bounded_by_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. - Qed. - - Local Lemma unfold_is_tighter_than_bool r1 r2 - : is_tighter_than_bool r1 r2 = true -> lower r2 <= lower r1 /\ upper r1 <= upper r2. - Proof using Type. - cbv [is_tighter_than_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. - Qed. - Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident_interp)). - Local Ltac do_cbv0 := - cbv [id - Compile.rewrite_rules_interp_goodT_curried - Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default pattern.base.lookup_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related - Reify.expr_value_to_rewrite_rule_replacement UnderLets.flat_map Compile.reify_expr_beta_iota Compile.reflect_expr_beta_iota Compile.reflect_ident_iota Compile.reify_to_UnderLets UnderLets.of_expr Compile.Base_value]; - cbn [UnderLets.splice Compile.reflect invert_expr.invert_Literal invert_expr.ident.invert_Literal Compile.splice_under_lets_with_value]. - Local Ltac do_cbv := - do_cbv0; - cbv [List.map List.fold_right List.rev list_rect orb List.app]. - Local Ltac start_interp_good := - apply Compile.rewrite_rules_interp_goodT_by_curried; - do_cbv; + cbv [List.skipn] in *; lazymatch goal with - | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ] - => let Q' := fresh in - pose Q as Q'; - change (forall x p, In (@existT A P x p) ls -> Q' x p); - apply (@forall_In_existT A P Q' ls); subst Q'; cbv [projT1 projT2 id] + | [ |- @Compile.rewrite_rules_interp_goodT ?ident ?pident ?pident_arg_types ?pident_to_typed ?ident_interp (rewrite_rules ?data ?var) ] + => let H := fresh in + pose proof (@Compile.rewrite_rules_interp_goodT_by_curried + _ _ _ pident_to_typed ident_interp (rewrite_rules data var) (rewrite_rules_specs data)) as H; + let h := head data in + cbv [rewrite_rules dummy_count rewrite_rules_specs h] in * |- ; + let h' := lazymatch type of H with context[Compile.rewrite_rules_interp_goodT_curried_cps _ _ _ ?v] => head v end in + unfold h' in H at 1; + cbv [Compile.rewrite_rules_interp_goodT_curried_cps pident_arg_types pident_to_typed] in H; + cbn [snd hd tl projT1 projT2] in H; + (* make [Qed] not take forever by explicitly recording a cast node *) + let H' := fresh in + pose proof H as H'; clear H; + apply H'; clear H' end; - do_cbv0; - repeat first [ progress intros - | match goal with - | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) - | [ |- True /\ _ ] => split; [ exact I | ] - | [ |- _ /\ _ ] => split; [ intros; exact I | ] - end - | progress cbn [eq_rect] in * ]; - cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related UnderLets.interp_related_gen] in *. + [ try assumption; + cbn [PrimitiveHList.hlist snd]; + repeat lazymatch goal with + | [ |- PrimitiveProd.Primitive.prod _ _ ] => constructor + | [ |- forall A x, x = x ] => reflexivity + end; + try assumption + | try match goal with + | [ H : PrimitiveHList.hlist _ _ |- _ ] => clear H + end; + let H := fresh in + intro H; hnf in H; + repeat first [ progress intros + | match goal with + | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) + | [ |- True /\ _ ] => split; [ exact I | ] + | [ |- _ /\ _ ] => split; [ intros; exact I | ] + | [ |- match (if ?b then _ else _) with Some _ => _ | None => _ end ] + => destruct b eqn:? + | [ |- True ] => exact I + end + | progress eta_expand + | progress cbn [eq_rect] in * ]; + cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp] in *; + cbn [fst snd] in *; + eta_expand; + split_andb; + repeat match goal with + | [ H : ?b = true |- _ ] => unique pose proof (@Reflect.reflect_bool _ b _ H) + | [ H : negb _ = false |- _ ] => rewrite Bool.negb_false_iff in H + | [ H : _ = false |- _ ] => rewrite <- Bool.negb_true_iff in H + end; + subst; cbv [ident.gets_inlined ident.literal] in *; + lazymatch goal with + | [ |- ?R ?v ] + => let v' := open_constr:(_) in + replace v with v'; + [ | symmetry; + unshelve eapply H; shelve_unifiable; + try eassumption; + try (repeat apply conj; assumption); + try match goal with + | [ |- ?A = ?B ] => first [ is_evar A | is_evar B ]; reflexivity + | [ |- ?T ] => is_evar T; exact I + | [ |- ?P ] (* TODO: Maybe we shouldn't simplify boolean expressions in rewriter reification, since we end up just having to undo it here in a kludgy way....... *) + => apply (proj2 (@Bool.reflect_iff P _ _)); + progress rewrite ?Bool.eqb_true_l, ?Bool.eqb_true_r, ?Bool.eqb_false_l, ?Bool.eqb_false_r; + let b := lazymatch goal with |- ?b = true => b end in + apply (proj1 (@Bool.reflect_iff _ b _)); + tauto + end ]; + clear H + end; + fold (@base.interp) in * + .. ]. Ltac recurse_interp_related_step := let do_replace v := @@ -192,767 +169,230 @@ Module Compilers. end. (* TODO: MOVE ME? *) - Local Ltac recursive_match_to_list_case term := + Local Ltac recursive_match_to_case term := + let contains_match x + := lazymatch x with + | context[match _ with nil => _ | _ => _ end] => true + | context[match _ with pair a b => _ end] => true + | context[match _ with true => _ | false => _ end] => true + | _ => false + end in lazymatch term with | context G[match ?ls with nil => ?N | cons x xs => @?C x xs end] => let T := type of N in let term := context G[list_case (fun _ => T) N C ls] in - recursive_match_to_list_case term - | context[match _ with nil => _ | _ => _ end] - => let G_f - := match term with - | context G[fun x : ?T => @?f x] - => lazymatch f with - | context[match _ with nil => _ | _ => _ end] - => let f' := fresh in - let T' := type of f in - constr:(((fun f' : T' => ltac:(let G' := context G[f'] in exact G')), - f)) - end - end in - lazymatch G_f with - | ((fun f' => ?G), (fun x : ?T => ?f)) - => let x' := fresh in - let rep := constr:(fun x' : T - => ltac:(let f := constr:(match x' with x => f end) in - let f := recursive_match_to_list_case f in - exact f)) in - let term := constr:(match rep with f' => G end) in - recursive_match_to_list_case term - end - | _ => term + recursive_match_to_case term + | context G[match ?v with pair a b => @?P a b end] + => let T := lazymatch type of P with forall a b, @?T a b => T end in + let term := context G[prod_rect (fun ab => T (fst ab) (snd ab)) P v] in + recursive_match_to_case term + | context G[match ?b with true => ?t | false => ?f end] + => let T := type of t in + let term := context G[bool_rect (fun _ => T) t f b] in + recursive_match_to_case term + | _ => let has_match := contains_match term in + match has_match with + | true + => let G_f + := match term with + | context G[fun x : ?T => @?f x] + => let has_match := contains_match f in + lazymatch has_match with + | true + => let f' := fresh in + let T' := type of f in + constr:(((fun f' : T' => ltac:(let G' := context G[f'] in exact G')), + f)) + end + end in + lazymatch G_f with + | ((fun f' => ?G), (fun x : ?T => ?f)) + => let x' := fresh in + let rep := constr:(fun x' : T + => ltac:(let f := constr:(match x' with x => f end) in + let f := recursive_match_to_case f in + exact f)) in + let term := constr:(match rep with f' => G end) in + recursive_match_to_case term + end + | false + => term + end end. - Local Ltac recursive_match_to_list_case_in_goal := + Local Ltac recursive_match_to_case_in_goal := let G := match goal with |- ?G => G end in - let G := recursive_match_to_list_case G in + let G := recursive_match_to_case G in change G. - Local Ltac interp_good_t_step_related := - first [ lazymatch goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- True ] => exact I - | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence - | [ |- ?G ] => has_evar G; reflexivity - | [ |- context[expr.interp_related_gen _ _ _ _] ] => reflexivity - | [ |- context[_ == _] ] => reflexivity - (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand - | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*) - end - | match goal with - | [ |- UnderLets.interp_related ?ii ?R (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) - | [ |- expr.interp_related_gen ?ii ?R (#ident.list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) - | [ |- expr.interp_related_gen ?ii ?R (#ident.list_case @ _ @ _ @ _)%expr (@list_case ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_case A (fun _ => P) N C ls) with (@ident.Thunked.list_case A P (fun _ => N) C ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@flat_map ?A ?B ?f ?ls) ] - => rewrite (@eq_flat_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@partition ?A ?f ?ls) ] - => rewrite (@eq_partition_list_rect A f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@List.map ?A ?B ?f ?ls) ] - => rewrite (@eq_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _ _) (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (List.repeat ?x ?n) ] - => rewrite (eq_repeat_nat_rect x n) - | [ |- ?R (nat_rect _ _ _ _ _) (@List.firstn ?A ?n ?ls) ] - => rewrite (@eq_firstn_nat_rect A n ls) - | [ |- ?R (nat_rect _ _ _ _ _) (@List.skipn ?A ?n ?ls) ] - => rewrite (@eq_skipn_nat_rect A n ls) - | [ |- ?R (list_rect _ _ _ _) (@List.rev ?A ?xs) ] - => rewrite (@eq_rev_list_rect A xs) - | [ |- ?R (list_rect _ _ _ _) (@List.length ?A ?xs) ] - => rewrite (@eq_length_list_rect A xs) - | [ |- ?R (list_rect _ _ _ _) (@List.flat_map ?A ?B ?f ?xs) ] - => rewrite (@eq_flat_map_list_rect A B f xs) - | [ |- ?R (list_rect _ _ _ _) (@List.partition ?A ?f ?xs) ] - => rewrite (@eq_partition_list_rect A f xs) - | [ |- ?R (nat_rect _ _ _ _ _) (@update_nth ?A ?n ?f ?xs) ] - => rewrite (@eq_update_nth_nat_rect A n f xs) - - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@flat_map ?A ?B ?f ?ls) ] - => rewrite (@eq_flat_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@partition ?A ?f ?ls) ] - => rewrite (@eq_partition_list_rect A f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@List.map ?A ?B ?f ?ls) ] - => rewrite (@eq_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr) (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] - => rewrite (@eq_fold_right_list_rect A B f v ls) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.firstn ?A ?n ?ls) ] - => rewrite (@eq_firstn_nat_rect A n ls) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.skipn ?A ?n ?ls) ] - => rewrite (@eq_skipn_nat_rect A n ls) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.rev ?A ?xs) ] - => rewrite (@eq_rev_list_rect A xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.length ?A ?xs) ] - => rewrite (@eq_length_list_rect A xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.flat_map ?A ?B ?f ?xs) ] - => rewrite (@eq_flat_map_list_rect A B f xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.partition ?A ?f ?xs) ] - => rewrite (@eq_partition_list_rect A f xs) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@update_nth ?A ?n ?f ?xs) ] - => rewrite (@eq_update_nth_nat_rect A n f xs) - | [ |- ?R (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - - - | [ |- expr.interp_related_gen _ _ (#ident.list_rect @ _ @ _ @ _)%expr (ident.Thunked.list_rect _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (list_rect _ _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.nat_rect @ _ @ _ @ _)%expr (ident.Thunked.nat_rect _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (nat_rect _ _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.list_case @ _ @ _ @ _)%expr (ident.Thunked.list_case _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_list_case_in_goal - end - | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related UnderLets.interp_related_gen type.related] in * - | progress cbv [Compile.option_bind' respectful expr.interp_related] in * - | progress fold (@type.interp _ base.interp) - | progress fold (@base.interp) - | progress change S with Nat.succ - | match goal with - | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat - | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map - | [ |- context[List.map (fun x => x) _] ] => rewrite map_id - | [ |- context[List.map _ (List.rev _)] ] => rewrite map_rev - | [ |- context[List.map _ (firstn _ _)] ] => rewrite <- firstn_map - | [ |- context[List.map _ (skipn _ _)] ] => rewrite <- skipn_map - | [ |- context[List.length (List.map _ _)] ] => rewrite map_length - | [ |- context[List.combine (List.map _ _) _] ] => rewrite combine_map_l - | [ |- context[List.combine _ (List.map _ _)] ] => rewrite combine_map_r - | [ |- context[expr.interp _ (reify_list _)] ] => rewrite expr.interp_reify_list - | [ |- context[expr.interp _ (UnderLets.to_expr ?e)] ] => rewrite UnderLets.interp_to_expr - | [ |- context[UnderLets.interp _ (UnderLets.splice_list _ _)] ] => rewrite UnderLets.interp_splice_list - | [ |- context[rlist_rect] ] => rewrite rlist_rect_eq - | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect - | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice - | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map - | [ |- context[expr.interp_related_gen _ _ (reify_list _)] ] - => rewrite expr.reify_list_interp_related_gen_iff - | [ H : context[expr.interp_related_gen _ _ (reify_list _)] |- _ ] - => rewrite expr.reify_list_interp_related_gen_iff in H - | [ |- expr.interp_related_gen ?ident_interp _ (UnderLets.to_expr ?x) ?y ] - => change (expr.interp_related ident_interp (UnderLets.to_expr x) y); - rewrite <- UnderLets.to_expr_interp_related_iff - | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff - | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff - | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff - | [ |- context[Forall2 _ (List.rev _) (List.rev _)] ] => rewrite Forall2_rev_iff - | [ |- context[Forall2 _ ?x ?x] ] => rewrite Forall2_Forall; cbv [Proper] - | [ |- context[Forall _ (seq _ _)] ] => rewrite Forall_seq - | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.firstn ?n ?l1) (List.firstn ?n ?l2) ] - => apply Forall2_firstn, H - | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.skipn ?n ?l1) (List.skipn ?n ?l2) ] - => apply Forall2_skipn, H - | [ |- Forall2 ?R (List.combine _ _) (List.combine _ _) ] - => eapply Forall2_combine; [ | eassumption | eassumption ] - | [ H : List.Forall2 _ ?l1 ?l2, H' : ?R ?v1 ?v2 |- ?R (nth_default ?v1 ?l1 ?x) (nth_default ?v2 ?l2 ?x) ] - => apply Forall2_forall_iff''; split; assumption - | [ H : List.Forall2 _ ?x ?y |- List.length ?x = List.length ?y ] - => eapply eq_length_Forall2, H - | [ |- exists fv xv, _ /\ _ /\ fv xv = ?f ?x ] - => exists f, x; repeat apply conj; [ solve [ repeat interp_good_t_step_related ] | | reflexivity ] - | [ |- _ /\ ?x = ?x ] => split; [ | reflexivity ] - | [ |- UnderLets.interp_related - ?ident_interp ?R - (list_rect - (fun _ : list (expr ?A) => UnderLets.UnderLets _ _ _ ?B) - ?Pnil - ?Pcons - ?ls) - (list_rect - (fun _ : list _ => ?B') - ?Pnil' - ?Pcons' - ?ls') ] - => apply (@UnderLets.list_rect_interp_related _ _ _ ident_interp A B Pnil Pcons ls B' Pnil' Pcons' ls' R) - | [ |- UnderLets.interp_related - ?ident_interp ?R - (list_rect - (fun _ : list (expr ?A) => ?B -> UnderLets.UnderLets _ _ _ ?C) - ?Pnil - ?Pcons - ?ls - ?x) - (list_rect - (fun _ : list _ => ?B' -> ?C') - ?Pnil' - ?Pcons' - ?ls' - ?x') ] - => apply (@UnderLets.list_rect_arrow_interp_related _ _ _ ident_interp A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R (expr.interp_related ident_interp)) - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] - => apply UnderLets.nat_rect_interp_related - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ] - => eapply UnderLets.nat_rect_arrow_interp_related; [ .. | eassumption ] - | [ |- UnderLets.interp_related _ _ (UnderLets.splice _ _) _ ] - => rewrite UnderLets.splice_interp_related_iff - | [ |- UnderLets.interp_related ?ident_interp _ (UnderLets.splice_list _ _) _ ] - => apply UnderLets.splice_list_interp_related_of_ex with (RA:=expr.interp_related ident_interp); exists (fun x => x); eexists; repeat apply conj; [ | | reflexivity ] - | [ H : UnderLets.interp_related _ _ ?e ?v1 |- UnderLets.interp_related _ _ ?e ?f ] - => let f := match (eval pattern v1 in f) with ?f _ => f end in - eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ e v1 f); [ | exact H ]; cbv beta - | [ H : forall x y, ?R x y -> UnderLets.interp_related _ _ (?e x) (?v1 y) |- UnderLets.interp_related _ _ (?e ?xv) ?f ] - => lazymatch f with - | context[v1 ?yv] - => let f := match (eval pattern (v1 yv) in f) with ?f _ => f end in - eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ (e xv) (v1 yv) f); [ | eapply H; assumption ] - end - | [ |- expr.interp_related_gen - _ _ - (#(ident.prod_rect) @ ?f @ ?e)%expr - match ?e' with pair a b => @?f' a b end ] - => let fh := fresh in - let eh := fresh in - set (fh := f); set (eh := e); cbn [expr.interp_related_gen]; subst fh eh; - exists (fun ev => match ev with pair a b => f' a b end), e'; - repeat apply conj; - [ | assumption | reflexivity ]; - exists (fun fv ev => match ev with pair a b => fv a b end), f'; - repeat apply conj; - [ cbn [type.interp type.related ident_interp]; cbv [respectful]; intros; subst; eta_expand; auto | | reflexivity ] - | [ |- expr.interp_related_gen - _ _ - (#(ident.bool_rect) @ ?t @ ?f @ ?b)%expr - (bool_rect ?P ?t' ?f' ?b') ] - => let th := fresh in - let fh := fresh in - let bh := fresh in - set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related_gen]; subst th fh bh; - unshelve - ((exists (bool_rect P t' f'), b'); repeat apply conj; - [ | shelve | reflexivity ]; - (exists (fun fv => bool_rect P t' (fv tt)), (fun _ => f')); repeat apply conj; - [ | shelve | reflexivity ]; - (exists (fun tv fv => bool_rect P (tv tt) (fv tt)), (fun _ => t')); repeat apply conj; - [ | shelve | reflexivity ]) - | [ |- @expr.interp_related_gen _ _ _ _ _ _ (type.base ?t) _ _ ] - => lazymatch t with - | base.type.type_base base.type.Z => idtac - | base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z) => idtac - end; - progress repeat recurse_interp_related_step - | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1), - _ /\ _ /\ fv ev = ?x ] - => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end; - lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end; - progress repeat recurse_interp_related_step - | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] - => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh - | [ H : expr.interp_related_gen _ _ ?x ?x' |- expr.interp_related_gen _ _ (?f @ ?x) (?f' ?x') ] - => let fh := fresh in - let xh := fresh in - set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; - exists f', x'; repeat apply conj; - [ | exact H | reflexivity ] - | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] => apply Forall2_update_nth - | [ H : zrange * zrange |- _ ] => destruct H - end - | progress intros - | progress subst - | assumption - | progress inversion_option - | progress destruct_head'_and - | progress destruct_head'_unit - | progress split_andb - | match goal with - | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2 - | [ |- firstn _ _ = firstn _ _ ] => apply f_equal2 - | [ |- skipn _ _ = skipn _ _ ] => apply f_equal2 - | [ |- rev _ = rev _ ] => apply f_equal - | [ |- List.app ?l1 ?l2 = List.app ?l1' ?l2 ] => apply f_equal2 - | [ |- List.app ?l1 ?l2 = List.app ?l1 ?l2' ] => apply f_equal2 - | [ |- cons _ _ = cons _ _ ] => apply f_equal2 - | [ |- list_rect _ ?Pnil ?Pcons ?ls = list_rect _ ?Pnil ?Pcons' ?ls ] - => apply list_rect_Proper; [ reflexivity | repeat intro | reflexivity ] - | [ |- bool_rect _ ?x ?y ?b = bool_rect _ ?x ?y ?b' ] - => apply f_equal3; [ reflexivity | reflexivity | solve [ repeat interp_good_t_step_related ] ] - | [ H : expr.wf _ ?v1 ?v2 |- expr.interp _ ?v1 = expr.interp _ ?v2 ] - => apply (expr.wf_interp_Proper _ _ _ H ltac:(assumption)) - | [ |- ?R (?f (?g (if ?b then ?x else ?y))) (bool_rect ?A ?B ?C ?D) ] - => rewrite <- (@Bool.pull_bool_if _ _ g b), <- (@Bool.pull_bool_if _ _ f b); - change (R (bool_rect _ (f (g x)) (f (g y)) b) (bool_rect A B C D)) - | [ |- context[invert_expr.reflect_list ?ls] ] - => destruct (invert_expr.reflect_list ls) eqn:?; expr.invert_subst - | [ |- ?f (nth_default _ _ _) = _ ] - => rewrite <- (@map_nth_default_always _ _ f) - | [ |- map ?f ?ls = map ?g ?ls ] => apply map_ext_in - | [ |- List.map _ (update_nth _ _ _) = update_nth _ _ _ ] => apply map_update_nth_ext - | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) - | [ H : forall v : unit, _ |- _ ] => specialize (H tt) - | [ H : _ = expr.interp ?ii ?v |- _ ] => is_var v; generalize dependent (expr.interp ii v); clear v - | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ] - => is_var b; destruct b; cbv [bool_rect] - | [ H : (forall x y, _ -> expr.interp _ (UnderLets.interp _ (?f1 x)) = expr.interp _ (UnderLets.interp _ (?f2 y))) - |- expr.interp _ (UnderLets.interp _ (?f1 ?x1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2)) ] - => apply H - | [ H : (forall x y, _ -> forall x' y', _ -> expr.interp _ (UnderLets.interp _ (?f1 x x')) = expr.interp _ (UnderLets.interp _ (?f2 y y'))) - |- expr.interp _ (UnderLets.interp _ (?f1 ?x1 ?y1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2 ?y2)) ] - => apply H - | [ |- context G[rwhen ?v ?b] ] - => let c := constr:(rwhen v b) in - let c := (eval cbv [rwhen] in c) in - let G' := context G[c] in - change G'; - destruct b eqn:? - | [ |- context G[rwhenl ?v ?b] ] - => let c := constr:(rwhenl v b) in - let c := (eval cbv [rwhenl] in c) in - let G' := context G[c] in - change G'; - destruct b eqn:? - | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H - | [ |- context[expr.interp ?ii ?v] ] - => is_var v; generalize dependent (expr.interp ii v); clear v; intro v - | [ |- context[Z.mul_split ?a ?b ?c] ] - => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod - | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct - | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ] - => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod - | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ] - => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod - | [ |- context[Z.add_get_carry_full ?a ?b ?c] ] - => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod - | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ] - => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod - | [ |- pair _ _ = pair _ _ ] => apply f_equal2 - | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia - | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia - | [ |- Z.opp _ = Z.opp _ ] => apply f_equal - end - | match goal with - | [ |- context[?f (list_rect _ _ _ _)] ] - => match f with - | expr.interp _ => idtac - | Compile.reify_expr => idtac - end; - erewrite (@push_f_list_rect _ _ f) - by (intros; - repeat first [ progress cbn [expr.interp ident.gen_interp UnderLets.interp Compile.reify_expr] - | rewrite UnderLets.interp_splice ]; - match goal with - | [ |- ?LHS = ?Pcons' ?x ?xs ?rec ] - => let LHS' := match (eval pattern x, xs, rec in LHS) with ?f _ _ _ => f end in - unify Pcons' LHS'; reflexivity - end) - | [ |- context[?f (nat_rect _ _ _ _)] ] - => match f with - | expr.interp _ => idtac - | UnderLets.interp _ => idtac - | Compile.reify_expr => idtac - end; - erewrite (@push_f_nat_rect _ _ f) - by (intros; - repeat first [ progress cbn [expr.interp ident.gen_interp UnderLets.interp Compile.reify_expr] - | rewrite UnderLets.interp_splice ]; - match goal with - | [ |- ?LHS = ?PS' ?x ?rec ] - => let LHS' := match (eval pattern x, rec in LHS) with ?f _ _ => f end in - unify PS' LHS'; reflexivity - end) - | [ |- ?f (list_rect _ _ _ _) = list_rect _ _ _ _ ] - => match f with - | expr.interp _ => idtac - | Compile.reify_expr => idtac - end; - erewrite (@push_f_list_rect _ _ f); - [ apply list_rect_Proper; repeat intro; try reflexivity | ] - | [ |- ?f (nat_rect _ _ _ _) = nat_rect _ _ _ _ ] - => match f with - | expr.interp _ => idtac - | UnderLets.interp _ => idtac - | Compile.reify_expr => idtac - end; - erewrite (@push_f_nat_rect _ _ f); - [ apply nat_rect_Proper_nondep; repeat intro; try reflexivity | ] - end - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress destruct_head'_or - | progress cbn [expr.interp_related_gen] in * - | match goal with - | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] - |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ] - => apply H - | [ H : forall x1 x2, ?R1 x1 x2 -> ?R2 (?f1 x1) (?f2 x2) |- ?R2 (?f1 _) (?f2 _) ] - => apply H - | [ H : forall x1 x2, ?R1 x1 x2 -> forall y1 y2, ?R2 y1 y2 -> ?R3 (?f1 x1 y1) (?f2 x2 y2) |- ?R3 (?f1 _ _) (?f2 _ _) ] - => apply H - | [ H : forall x x', ?Rx x x' -> forall y y', _ -> forall z z', ?Rz z z' -> ?R (?f x y z) (?f' x' y' z') |- ?R (?f _ _ _) (?f' _ _ _) ] - => apply H; clear H - | [ H : forall x x', _ -> forall y y', _ -> forall z z', _ -> forall w w', _ -> ?R (?f x y z w) (?f' x' y' z' w') |- ?R (?f _ _ _ _) (?f' _ _ _ _) ] - => apply H; clear H - end - | progress cbv [Option.bind] in * - | match goal with - | [ H : expr.interp_related_gen _ _ ?e ?v |- _ ] => is_var e; clear H e - end ]. - - Local Ltac interp_good_t_step_arith := - first [ lazymatch goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- True ] => exact I - | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence - | [ H : true = false |- _ ]=> exfalso; clear -H; congruence - | [ H : false = true |- _ ]=> exfalso; clear -H; congruence - end - | progress cbv [option_beq] in * - | match goal with - | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ] - => rewrite ZRange.normalize_idempotent in H - | [ |- context[ZRange.normalize (ZRange.normalize _)] ] - => rewrite ZRange.normalize_idempotent - | [ |- context[ident.cast (ZRange.normalize ?r)] ] - => rewrite ident.cast_normalize - | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ] - => rewrite ident.cast_normalize in H - | [ H : ?T, H' : ?T |- _ ] => clear H' - | [ H : context[is_bounded_by_bool _ (ZRange.normalize (-_))] |- _ ] - => rewrite ZRange.is_bounded_by_bool_move_opp_normalize in H - | [ |- context[is_bounded_by_bool _ (ZRange.normalize (-_))] ] - => rewrite ZRange.is_bounded_by_bool_move_opp_normalize - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ ?r ?v] ] - => rewrite (@ident.cast_in_normalized_bounds _ r v) by exact H - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ (-?r) (-?v)] ] - => rewrite (@ident.cast_in_normalized_bounds _ (-r) (-v)); - [ | clear -H ] - | [ |- context[ident.cast _ ?r (-ident.cast _ (-?r) ?v)] ] - => rewrite (ident.cast_in_normalized_bounds r (-ident.cast _ (-r) v)) - by (rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize; apply ident.cast_always_bounded) - | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] - => rewrite (@ident.cast_idempotent _ _ r) - | [ H : is_bounded_by_bool _ ?r = true |- _] - => is_var r; unique pose proof (ZRange.is_bounded_by_normalize _ _ H) - | [ H : lower ?x = upper ?x |- _ ] => is_var x; destruct x; cbn [upper lower] in * - | [ H : is_bounded_by_bool ?x (ZRange.normalize r[?y~>?y]) = true |- _ ] - => apply ZRange.is_bounded_by_bool_normalize_constant_iff in H - | [ H : is_bounded_by_bool ?x r[?y~>?y] = true |- _ ] - => apply ZRange.is_bounded_by_bool_constant_iff in H - end + Local Ltac preprocess_step := + first [ progress cbv [expr.interp_related respectful ident.literal ident.eagerly] in * + | progress cbn [fst snd base.interp base.base_interp Compile.value'] in * | progress intros | progress subst - | assumption - | progress destruct_head'_and - | progress Z.ltb_to_lt - | progress split_andb - | match goal with - | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia - | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia - | [ |- Z.opp _ = Z.opp _ ] => apply f_equal - end - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress destruct_head'_or - | match goal with - | [ |- context[-ident.cast _ (-?r) (-?v)] ] => rewrite (ident.cast_opp' r v) - | [ |- context[ident.cast ?coor ?r ?v] ] - => is_var v; - pose proof (@ident.cast_always_bounded coor r v); - generalize dependent (ident.cast coor r v); clear v; intro v; intros - | [ |- context[ident.cast ?coor ?r ?v] ] - => is_var v; is_var coor; - pose proof (@ident.cast_cases coor r v); - generalize dependent (ident.cast coor r v); intros - | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ] - => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than) - | [ H : is_bounded_by_bool (-?v) ?r = true, H' : (-?r <=? ?r')%zrange = true |- _ ] - => unique assert (is_bounded_by_bool v r' = true) - by (apply (@ZRange.is_bounded_by_of_is_tighter_than _ _ H'); - rewrite <- ZRange.is_bounded_by_bool_opp, ZRange.opp_involutive; exact H) - | [ H : is_bounded_by_bool ?v (-?r) = true |- _ ] - => is_var v; - unique assert (is_bounded_by_bool (-v) r = true) - by now rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize, ZRange.normalize_opp - | [ H : is_bounded_by_bool ?x r[0~>?v-1] = true |- _ ] - => progress (try unique assert (0 <= x); try unique assert (x <= v - 1)); - [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia.. - | ] - end - | progress cbn [expr.interp_related_gen] in * | match goal with - | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith - | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith - | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r - | [ |- context[Z.land _ (Z.ones _)] ] => rewrite Z.land_ones by auto using Z.log2_nonneg - | [ |- context[- - _] ] => rewrite Z.opp_involutive - | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H - | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] - => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith - | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm - | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H - | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H - | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ] - => rewrite <- H in H' - | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const - | [ H : 0 <= ?x, H' : ?x <= ?r - 1 |- context[?x mod ?r] ] - => rewrite (Z.mod_small x r) by (clear -H H'; lia) - | [ H : 0 <= ?x, H' : ?x <= ?y - 1 |- context[?x / ?y] ] - => rewrite (Z.div_small x y) by (clear -H H'; lia) - | [ H : ?x = 2^Z.log2 ?x |- _ ] - => unique assert (0 <= x) by (rewrite H; auto with zarith) - | [ |- _ mod ?x = _ mod ?x ] - => progress (push_Zmod; pull_Zmod) - | [ |- ?f (_ mod ?x) = ?f (_ mod ?x) ] - => progress (push_Zmod; pull_Zmod) - | [ |- _ mod ?x = _ mod ?x ] - => apply f_equal2; (lia + nia) - | _ => rewrite !Z.shiftl_mul_pow2 in * by auto using Z.log2_nonneg - | _ => rewrite !Z.land_ones in * by auto using Z.log2_nonneg - | H : ?x mod ?b * ?y <= _ - |- context [ (?x * ?y) mod ?b ] => - rewrite (PullPush.Z.mul_mod_l x y b); - rewrite (Z.mod_small (x mod b * y) b) by omega - | [ |- context[_ - ?x + ?x] ] => rewrite !Z.sub_add - | [ |- context[_ mod (2^_) * 2^_] ] => rewrite <- !Z.mul_mod_distr_r_full - | [ |- context[Z.land _ (Z.ones _)] ] => rewrite !Z.land_ones by lia - | [ |- context[2^?a * 2^?b] ] => rewrite <- !Z.pow_add_r by lia - | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l - | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r - | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r - | [ |- context[Zpos ?p * ?x / Zpos ?p] ] - => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) - | [ H : context[Zpos ?p * ?x / Zpos ?p] |- _ ] - => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) - | [ |- ?f (?a mod ?r) = ?f (?b mod ?r) ] => apply f_equal; apply f_equal2; lia - | [ |- context[-?a - ?b + ?c] ] => replace (-a - b + c) with (c - a - b) by (clear; lia) - | [ |- context[?x - ?y + ?z] ] - => lazymatch goal with - | [ |- context[z - y + x] ] - => progress replace (z - y + x) with (x - y + z) by (clear; lia) - end - | [ |- context[?x - ?y - ?z] ] - => lazymatch goal with - | [ |- context[x - z - y] ] - => progress replace (x - z - y) with (x - y - z) by (clear; lia) - end - | [ |- context[?x + ?y] ] - => lazymatch goal with - | [ |- context[y + x] ] - => progress replace (y + x) with (x + y) by (clear; lia) - end - | [ |- context[?x + ?y + ?z] ] - => lazymatch goal with - | [ |- context[x + z + y] ] - => progress replace (x + z + y) with (x + y + z) by (clear; lia) - | [ |- context[z + x + y] ] - => progress replace (z + x + y) with (x + y + z) by (clear; lia) - | [ |- context[z + y + x] ] - => progress replace (z + y + x) with (x + y + z) by (clear; lia) - | [ |- context[y + x + z] ] - => progress replace (y + x + z) with (x + y + z) by (clear; lia) - | [ |- context[y + z + x] ] - => progress replace (y + z + x) with (x + y + z) by (clear; lia) - end - | [ |- - ident.cast _ (-?r) (- (?x / ?y)) = ident.cast _ ?r (?x' / ?y) ] - => tryif constr_eq x x' then fail else replace x with x' by lia - | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast + | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match _ with pair a b => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match _ with true => _ | false => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match invert_expr.reflect_list ?ls with _ => _ end] ] + => destruct (invert_expr.reflect_list ls) eqn:? + | [ |- context G[expr.interp_related_gen ?ident_interp (fun t : ?T => ?vii t ?b)] ] + => progress change (fun t : T => vii t b) with (fun t : T => @Compile.value_interp_related _ ident_interp t b) end ]. - - Local Ltac remove_casts := + Local Ltac preprocess := repeat preprocess_step. + Local Ltac handle_extra_nbe := repeat match goal with - | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] - => rewrite ident.cast_idempotent - | [ H : context[ident.cast _ ?r (ident.cast _ ?r _)] |- _ ] - => rewrite ident.cast_idempotent in H - | [ |- context[ident.cast ?coor ?r ?v] ] - => is_var v; - pose proof (@ident.cast_always_bounded coor r v); - generalize dependent (ident.cast coor r v); - clear v; intro v; intros - | [ H : context[ident.cast ?coor ?r ?v] |- _ ] - => is_var v; - pose proof (@ident.cast_always_bounded coor r v); - generalize dependent (ident.cast coor r v); - clear v; intro v; intros - | [ H : context[ZRange.constant ?v] |- _ ] => unique pose proof (ZRange.is_bounded_by_bool_normalize_constant v) - | [ H : is_tighter_than_bool (?ZRf ?r1 ?r2) (ZRange.normalize ?rs) = true, - H1 : is_bounded_by_bool ?v1 ?r1 = true, - H2 : is_bounded_by_bool ?v2 ?r2 = true - |- _ ] - => let cst := multimatch goal with - | [ |- context[ident.cast ?coor rs (?Zf v1 v2)] ] => constr:(ident.cast coor rs (Zf v1 v2)) - | [ H : context[ident.cast ?coor rs (?Zf v1 v2)] |- _ ] => constr:(ident.cast coor rs (Zf v1 v2)) - end in - lazymatch cst with - | ident.cast ?coor rs (?Zf v1 v2) - => let lem := lazymatch constr:((ZRf, Zf)%core) with - | (ZRange.shiftl, Z.shiftl)%core => constr:(@ZRange.is_bounded_by_bool_shiftl v1 r1 v2 r2 H1 H2) - | (ZRange.shiftr, Z.shiftr)%core => constr:(@ZRange.is_bounded_by_bool_shiftr v1 r1 v2 r2 H1 H2) - | (ZRange.land, Z.land)%core => constr:(@ZRange.is_bounded_by_bool_land v1 r1 v2 r2 H1 H2) - end in - try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); - clear H; - rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1 v2)) in * by assumption - end - | [ H : is_tighter_than_bool (?ZRf ?r1) (ZRange.normalize ?rs) = true, - H1 : is_bounded_by_bool ?v1 ?r1 = true - |- _ ] - => let cst := multimatch goal with - | [ |- context[ident.cast ?coor rs (?Zf v1)] ] => constr:(ident.cast coor rs (Zf v1)) - | [ H : context[ident.cast ?coor rs (?Zf v1)] |- _ ] => constr:(ident.cast coor rs (Zf v1)) - end in - lazymatch cst with - | ident.cast ?coor rs (?Zf v1) - => let lem := lazymatch constr:((ZRf, Zf)%core) with - | (ZRange.cc_m ?s, Z.cc_m ?s)%core => constr:(@ZRange.is_bounded_by_bool_cc_m s v1 r1 H1) - end in - try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); - clear H; - rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1)) in * by assumption - end - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast ?coor ?r ?v] ] - => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true, H' : context[ident.cast ?coor ?r ?v] |- _ ] - => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption - | [ H : is_bounded_by_bool ?v ?r = true, - H' : is_tighter_than_bool ?r r[0~>?x-1]%zrange = true, - H'' : Z.eqb ?x ?m = true - |- context[?v mod ?m] ] - => unique assert (is_bounded_by_bool v r[0~>x-1] = true) - by (eapply ZRange.is_bounded_by_of_is_tighter_than; eassumption) - | _ => progress Z.ltb_to_lt - | _ => progress subst + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (expr.Ident _)) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related_gen ident_interp type.related]; reflexivity + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (reify_list _)) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen]; rewrite expr.reify_list_interp_related_gen_iff + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (_, _)%expr) ?x ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen]; + recurse_interp_related_step; + [ recurse_interp_related_step + | lazymatch x with + | (_, _) => reflexivity + | _ => etransitivity; [ | symmetry; apply surjective_pairing ]; reflexivity + end ]; + [ | reflexivity ]; cbn [fst snd]; + recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | [ |- List.Forall2 _ (List.map _ _) _ ] + => rewrite Forall2_map_l_iff + | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] + | [ |- List.Forall _ _ ] => rewrite Forall_forall; intros + | [ |- expr.interp_related_gen _ _ (expr.Ident _) _ ] + => cbn [expr.interp_related_gen ident_interp type.related]; reflexivity end. + Local Ltac fin_tac := + repeat first [ assumption + | progress change S with Nat.succ + | progress cbn [base.interp base.base_interp type.interp] in * + | progress fold (@type.interp _ base.interp) + | progress fold (@base.interp) + | progress subst + | progress cbv [respectful ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.option_rect pointwise_relation] + | progress intros + | solve [ auto ] + | match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- list_rect _ _ _ _ = ident.Thunked.list_rect _ _ _ _ ] + => cbv [ident.Thunked.list_rect]; apply list_rect_Proper; cbv [pointwise_relation]; intros + | [ |- list_rect (fun _ => ?A -> ?B) _ _ _ _ = list_rect _ _ _ _ _ ] + => apply list_rect_arrow_Proper; cbv [respectful]; intros + | [ |- nat_rect _ _ _ _ = ident.Thunked.nat_rect _ _ _ _ ] + => apply nat_rect_Proper_nondep; cbv [respectful] + | [ |- nat_rect (fun _ => ?A -> ?B) _ _ _ _ = nat_rect _ _ _ _ _ ] + => apply (@nat_rect_Proper_nondep_gen (A -> B) (eq ==> eq)%signature); cbv [respectful]; intros + | [ |- list_case _ _ _ ?ls = list_case _ _ _ ?ls ] + => is_var ls; destruct ls; cbn [list_case] + | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ] + => is_var b; destruct b; cbn [bool_rect] + | [ |- _ = ident.cast2 _ _ _ ] => cbv [ident.cast2]; break_innermost_match + end ]. + Local Ltac handle_reified_rewrite_rules_interp := + repeat first [ assumption + | match goal with + | [ |- UnderLets.interp_related _ _ (Reify.expr_value_to_rewrite_rule_replacement _ ?sda _) _ ] + => apply (@Reify.expr_value_to_rewrite_rule_replacement_interp_related cast_outside_of_range _ (@Reify.reflect_ident_iota_interp_related cast_outside_of_range) sda) - Local Ltac unfold_cast_lemmas := - repeat match goal with - | [ H : context[ZRange.normalize (ZRange.constant _)] |- _ ] - => rewrite ZRange.normalize_constant in H - | [ H : is_bounded_by_bool _ (ZRange.normalize ?r) = true |- _ ] - => is_var r; generalize dependent (ZRange.normalize r); clear r; intro r; intros - | [ H : is_bounded_by_bool ?x (ZRange.constant ?x) = true |- _ ] - => clear H - | [ H : is_bounded_by_bool ?x ?r = true |- _ ] - => is_var r; apply unfold_is_bounded_by_bool in H - | [ H : is_bounded_by_bool ?x r[_~>_] = true |- _ ] - => apply unfold_is_bounded_by_bool in H - | [ H : is_tighter_than_bool r[_~>_] r[_~>_] = true |- _ ] - => apply unfold_is_tighter_than_bool in H - | _ => progress cbn [lower upper] in * - | [ H : context[lower ?r] |- _ ] - => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] - | [ H : context[upper ?r] |- _ ] - => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] - | _ => progress Z.ltb_to_lt - end. + | [ |- UnderLets.interp_related_gen ?ii ?R (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.eager_list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_case @ _ @ _ @ _)%expr (@list_case ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_case A (fun _ => P) N C ls) with (@ident.Thunked.list_case A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.nat_rect @ _ @ _ @ _)%expr (@nat_rect (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@nat_rect (fun _ => P) N C ls) with (@ident.Thunked.nat_rect P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.eager_nat_rect @ _ @ _ @ _)%expr (@nat_rect (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@nat_rect (fun _ => P) N C ls) with (@ident.Thunked.nat_rect P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.bool_rect @ _ @ _ @ _)%expr (@bool_rect (fun _ => ?P) ?T ?F ?b) ] + => progress change (@bool_rect (fun _ => P) T F b) with (@ident.Thunked.bool_rect P (fun _ => T) (fun _ => F) b) + | [ |- expr.interp_related_gen ?ii ?R (#ident.option_rect @ _ @ _ @ _)%expr (@option_rect ?A (fun _ => ?P) ?S ?N ?o) ] + => progress change (@option_rect A (fun _ => P) S N o) with (@ident.Thunked.option_rect A P S (fun _ => N) o) - Local Ltac systematically_handle_casts := - remove_casts; unfold_cast_lemmas. + | [ |- match ?x with pair _ _ => _ end = prod_rect _ _ _ ] + => cbv [prod_rect]; eta_expand + + | [ |- expr.interp_related_gen _ _ (expr.Var _) _ ] + => cbn [expr.interp_related_gen] + | [ |- expr.interp_related_gen _ _ (expr.Ident _) _ ] + => cbn [expr.interp_related_gen ident_interp type.related]; fin_tac + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh; cbv beta; intros + | [ |- expr.interp_related_gen _ _ (expr.LetIn ?v ?f) (LetIn.Let_In ?V ?F) ] + => let vh := fresh in + set (vh := v); + let fh := fresh in + set (fh := f); + cbn [expr.interp_related_gen]; subst fh vh; cbv beta; + exists F, V; repeat apply conj; intros + | [ |- expr.interp_related_gen _ _ (?f @ ?x)%expr (?F ?X) ] + => let fh := fresh in + set (fh := f); + let xh := fresh in + set (xh := x); + cbn [expr.interp_related_gen]; subst fh xh; + exists F, X; repeat apply conj; [ | | reflexivity ] + + | [ |- _ = _ ] => solve [ fin_tac ] + end ]. - Local Ltac fin_with_nia := - lazymatch goal with - | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia - | _ => reflexivity || (Z.div_mod_to_quot_rem; (lia + nia)) - end. - Lemma nbe_rewrite_rules_interp_good - : rewrite_rules_interp_goodT nbe_rewrite_rules. + Local Notation specT rewriter_data + := (PrimitiveHList.hlist (@snd bool Prop) (List.skipn (dummy_count rewriter_data) (rewrite_rules_specs rewriter_data))) + (only parsing). + + Lemma nbe_rewrite_rules_interp_good (H : specT nbe_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules nbe_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related ]. - Qed. + Time all: preprocess; handle_extra_nbe; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma arith_rewrite_rules_interp_good max_const - : rewrite_rules_interp_goodT (arith_rewrite_rules max_const). + Lemma arith_rewrite_rules_interp_good max_const (H : specT (arith_rewriter_data max_const)) + : rewrite_rules_interp_goodT (rewrite_rules (arith_rewriter_data max_const) _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith; fin_with_nia ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma arith_with_casts_rewrite_rules_interp_good - : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. + Lemma arith_with_casts_rewrite_rules_interp_good (H : specT arith_with_casts_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules arith_with_casts_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith; fin_with_nia ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma strip_literal_casts_rewrite_rules_interp_good - : rewrite_rules_interp_goodT strip_literal_casts_rewrite_rules. + Lemma strip_literal_casts_rewrite_rules_interp_good (H : specT strip_literal_casts_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules strip_literal_casts_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith ]. - Qed. - - Local Ltac fancy_local_t := - repeat match goal with - | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, - H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H' - | [ H : forall s v v', ?invert_low s v = Some v' -> v = _ |- _ ] - => clear invert_low H - end. - Local Ltac more_fancy_arith_t := repeat autorewrite with zsimplify in *. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. Lemma fancy_rewrite_rules_interp_good (invert_low invert_high : Z -> Z -> option Z) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_interp_goodT fancy_rewrite_rules. + (H : specT (fancy_rewriter_data invert_low invert_high)) + : rewrite_rules_interp_goodT (rewrite_rules (fancy_rewriter_data invert_low invert_high) _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. Lemma fancy_with_casts_rewrite_rules_interp_good (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : zrange) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_interp_goodT (fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range). + (H : specT (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range)) + : rewrite_rules_interp_goodT (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _). Proof using Type. - Time start_interp_good. (* Finished transaction in 1.206 secs (1.207u,0.s) (successful) *) - Set Ltac Profiling. - Reset Ltac Profile. - Time all: repeat interp_good_t_step_related. (* Finished transaction in 13.259 secs (13.128u,0.132s) (successful) *) - Reset Ltac Profile. - Time all: fancy_local_t. (* Finished transaction in 0.051 secs (0.052u,0.s) (successful) *) - Time all: systematically_handle_casts. (* Finished transaction in 2.004 secs (1.952u,0.052s) (successful) *) - Time all: try solve [ repeat interp_good_t_step_arith ]. (* Finished transaction in 44.411 secs (44.004u,0.411s) (successful) *) - Qed. + Time start_interp_good. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. End with_cast. End RewriteRules. End Compilers. |