solvers.v 6.28 KB
Newer Older
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.

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.


178
179
180
181
Ltac solve_goal :=
  try fast_done;
  solve_goal_prepare_tac;
  normalize_and_simpl_goal;
182
  solve_goal_normalized_prepare_tac; reduce_closed_Z; enrich_context;
183
184
  repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //;
  refined_solver lia.