solvers.v 6.28 KB
 Michael Sammler committed Mar 31, 2021 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 ``````From refinedc.lithium Require Import base tactics_extend simpl_classes infrastructure. (** * [refined_solver] Version of naive_solver which fails faster. *) Tactic Notation "refined_solver" tactic(tac) := unfold iff, not in *; repeat match goal with | H : context [∀ _, _ ∧ _ ] |- _ => repeat setoid_rewrite forall_and_distr in H; revert H | H : context [Is_true _ ] |- _ => repeat setoid_rewrite Is_true_eq in H | |- Is_true _ => repeat setoid_rewrite Is_true_eq end; let rec go := repeat match goal with (**i solve the goal *) | |- _ => fast_done (**i intros *) | |- ∀ _, _ => intro (**i simplification of assumptions *) | H : False |- _ => destruct H | H : _ ∧ _ |- _ => (* Work around bug https://coq.inria.fr/bugs/show_bug.cgi?id=2901 *) let H1 := fresh in let H2 := fresh in destruct H as [H1 H2]; try clear H | H : ∃ _, _ |- _ => let x := fresh in let Hx := fresh in destruct H as [x Hx]; try clear H | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2) (**i simplify and solve equalities *) (* | |- _ => progress simplify_eq/= *) | |- _ => progress subst; csimpl in * (**i operations that generate more subgoals *) | |- _ ∧ _ => split (* | |- Is_true (bool_decide _) => apply (bool_decide_pack _) *) (* | |- Is_true (_ && _) => apply andb_True; split *) | H : _ ∨ _ |- _ => let H1 := fresh in destruct H as [H1|H1]; try clear H (* | H : Is_true (_ || _) |- _ => *) (* apply orb_True in H; let H1 := fresh in destruct H as [H1|H1]; try clear H *) (**i solve the goal using the user supplied tactic *) | |- _ => solve [tac] end; (**i use recursion to enable backtracking on the following clauses. *) match goal with (**i instantiation of the conclusion *) | |- ∃ x, _ => no_new_unsolved_evars ltac:(eexists; go) | |- _ ∨ _ => first [left; go | right; go] (* | |- Is_true (_ || _) => apply orb_True; first [left; go | right; go] *) | _ => (**i instantiations of assumptions. *) match goal with | H : ?P → ?Q |- _ => let H' := fresh "H" in assert P as H'; [clear H; go|]; specialize (H H'); clear H'; go end end in go. Tactic Notation "refined_solver" := refined_solver eauto. (** * [normalize_and_simpl_goal] *) Lemma intro_and_True P : (P ∧ True) → P. Proof. naive_solver. Qed. Ltac normalize_and_simpl_goal_step := first [ progress normalize_goal; simpl | lazymatch goal with | |- ∃ _, _ => fail 1 "normalize_and_simpl_goal stop in exist" end | lazymatch goal with | |- _ ∧ _ => idtac | _ => refine (intro_and_True _ _) end; refine (apply_simpl_and _ _ _ _ _); lazymatch goal with | |- true = true → _ => move => _; split_and? end | lazymatch goal with (* relying on the fact that unification variables cannot contain dependent variables to distinguish between dependent and non dependent forall *) | |- ?P -> ?Q => lazymatch type of P with | Prop => first [ progress normalize_goal_impl | notypeclasses refine (apply_simpl_impl _ _ _ _ _); [ solve [refine _] |]; simpl; match goal with | |- true = true -> _ => move => _ | |- false = false -> ?P → _ => move => _; match P with | ∃ _, _ => case | _ = _ => let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi | _ => check_hyp_not_exists P; intros ?; subst | _ => move => _ end end] (* just some unused variable, forget it *) | _ => move => _ end | |- forall _ : ?P, _ => lazymatch P with | (prod _ _) => case | unit => case | _ => intro end end ]. Ltac normalize_and_simpl_goal := repeat normalize_and_simpl_goal_step. (** * [compute_map_lookup] *) Ltac compute_map_lookup := lazymatch goal with | |- ?Q !! _ = Some _ => try (is_var Q; unfold Q) | _ => fail "unknown goal for compute_map_lookup" end; solve [repeat lazymatch goal with | |- <[?x:=?s]> ?Q !! ?y = Some ?res => lazymatch x with | y => change_no_check (Some s = Some res); reflexivity | _ => change_no_check (Q !! y = Some res) end end ]. (** * Enriching the context for lia *) Definition enrich_marker {A} (f : A) : A := f. Ltac enrich_context_base := repeat match goal with | |- context C [ Z.quot ?a ?b ] => let G := context C[enrich_marker Z.quot a b] in change_no_check G; try have ?:=Z.quot_lt a b ltac:(lia) ltac:(lia); try have ?:=Z.quot_pos a b ltac:(lia) ltac:(lia) | |- context C [ Z.rem ?a ?b ] => let G := context C[enrich_marker Z.rem a b] in change_no_check G; try have ?:=Z.rem_bound_pos a b ltac:(lia) ltac:(lia) | |- context C [ Z.modulo ?a ?b ] => let G := context C[enrich_marker Z.modulo a b] in change_no_check G; try have ?:=Z.mod_bound_pos a b ltac:(lia) ltac:(lia) | |- context C [ length (filter ?P ?l) ] => let G := context C[enrich_marker length (filter P l)] in change_no_check G; pose proof (filter_length P l) end. Ltac enrich_context_tac := enrich_context_base. Ltac enrich_context := enrich_context_tac; unfold enrich_marker. (* Open Scope Z_scope. *) (* Goal ∀ n m, 0 < n → 1 < m → n `quot` m = n `rem` m. *) (* move => n m ??. enrich_context. *) (* Abort. *) (** * [solve_goal] *) Ltac solve_goal_prepare_tac := idtac. Ltac solve_goal_normalized_prepare_tac := idtac. `````` Michael Sammler committed Jun 10, 2021 165 166 167 168 169 170 171 172 173 174 175 176 177 ``````Local Open Scope Z_scope. Ltac reduce_closed_Z_tac := idtac. Ltac reduce_closed_Z := idtac; reduce_closed_Z_tac; repeat match goal with | |- context [?a ≪ ?b] => progress reduce_closed (a ≪ b) | H : context [?a ≪ ?b] |- _ => progress reduce_closed (a ≪ b) | |- context [?a ≫ ?b] => progress reduce_closed (a ≫ b) | H : context [?a ≫ ?b] |- _ => progress reduce_closed (a ≫ b) end. `````` Michael Sammler committed Mar 31, 2021 178 179 180 181 ``````Ltac solve_goal := try fast_done; solve_goal_prepare_tac; normalize_and_simpl_goal; `````` Michael Sammler committed Jun 10, 2021 182 `````` solve_goal_normalized_prepare_tac; reduce_closed_Z; enrich_context; `````` Michael Sammler committed Mar 31, 2021 183 184 `````` repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //; refined_solver lia.``````