Skip to content

GitLab

Commit 079c2b54 authored by Michael Sammler's avatar Michael Sammler
Browse files

extract pure infrastructure to lithium

parent 40972f03
Pipeline #44415 passed with stage
in 29 minutes and 36 seconds
Hide whitespace changes
Inline Side-by-side
linux/pkvm/proofs/early_alloc/instances.v
View file @ 079c2b54
......@@ -33,10 +33,10 @@ Proof. rewrite !ly_size_PAGES. lia. Qed.
Typeclasses Opaque PAGES.
Global Opaque PAGES.
Hint Rewrite ly_size_ly_offset : refinedc_rewrite.
Hint Rewrite ly_size_PAGES_sub : refinedc_rewrite.
Hint Rewrite ly_size_PAGES : refinedc_rewrite.
Hint Rewrite ly_offset_PAGES : refinedc_rewrite.
Hint Rewrite ly_size_ly_offset : lithium_rewrite.
Hint Rewrite ly_size_PAGES_sub : lithium_rewrite.
Hint Rewrite ly_size_PAGES : lithium_rewrite.
Hint Rewrite ly_offset_PAGES : lithium_rewrite.
Hint Rewrite ly_size_ly_offset : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
......
theories/lithium/normalize.v 0 → 100644
View file @ 079c2b54
From refinedc.lithium Require Import base tactics_extend infrastructure.
(** * First version of normalization based on [autorewrite] *)
Create HintDb lithium_rewrite discriminated.
Ltac normalize_autorewrite :=
autorewrite with lithium_rewrite; exact: eq_refl.
Hint Rewrite @drop_0 @take_ge using can_solve_tac : lithium_rewrite.
Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : lithium_rewrite.
Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : lithium_rewrite.
Hint Rewrite <- @fmap_take @fmap_drop : lithium_rewrite.
Hint Rewrite @list_insert_fold : lithium_rewrite.
Hint Rewrite @list_insert_insert : lithium_rewrite.
Hint Rewrite @drop_drop : lithium_rewrite.
Hint Rewrite @tail_replicate @take_replicate @drop_replicate : lithium_rewrite.
Hint Rewrite <- @app_assoc @cons_middle : lithium_rewrite.
Hint Rewrite @app_nil_r @rev_involutive : lithium_rewrite.
Hint Rewrite <- @list_fmap_insert : lithium_rewrite.
Hint Rewrite <- minus_n_O plus_n_O minus_n_n : lithium_rewrite.
Hint Rewrite Nat2Z.id : lithium_rewrite.
Hint Rewrite Z2Nat.inj_mul Z2Nat.inj_sub Z2Nat.id using can_solve_tac : lithium_rewrite.
Hint Rewrite Nat.succ_pred_pos using can_solve_tac : lithium_rewrite.
Hint Rewrite Nat.add_assoc Nat.min_id : lithium_rewrite.
Hint Rewrite Z.quot_mul using can_solve_tac : lithium_rewrite.
Hint Rewrite <-Nat.mul_sub_distr_r Z.mul_add_distr_r Z.mul_sub_distr_r : lithium_rewrite.
Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : lithium_rewrite.
Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : lithium_rewrite.
Hint Rewrite keep_factor2_min_1 keep_factor2_twice : lithium_rewrite.
Local Definition lookup_insert_gmap A K `{Countable K} := lookup_insert (M := gmap K) (A := A).
Hint Rewrite lookup_insert_gmap : lithium_rewrite.
(** * Second version of normalization based on typeclasses *)
Class NormalizeWalk {A} (progress : bool) (a b : A) : Prop := normalize_walk: a = b.
Class Normalize {A} (progress : bool) (a b : A) : Prop := normalize: a = b.
Hint Mode NormalizeWalk + - + - : typeclass_instances.
Hint Mode Normalize + - + - : typeclass_instances.
Global Instance normalize_walk_protected A (x : A) :
NormalizeWalk false (protected x) (protected x) | 10.
Proof. done. Qed.
(* TODO: This does not go under binders *)
Lemma normalize_walk_app A B (f f' : A → B) x x' r p1 p2 p3
`{!NormalizeWalk p1 f f'}
`{!NormalizeWalk p2 x x'} `{!TCEq (p1 || p2) true}
`{!Normalize p3 (f' x') r}:
NormalizeWalk true (f x) r.
Proof. unfold NormalizeWalk, Normalize in *. naive_solver. Qed.
Hint Extern 50 (NormalizeWalk _ (?f ?x) _) => class_apply normalize_walk_app : typeclass_instances.
Global Instance normalize_walk_end_progress A (x x' : A) `{!Normalize true x x'} :
NormalizeWalk true x x' | 100.
Proof. done. Qed.
Global Instance normalize_walk_end A (x : A) :
NormalizeWalk false x x | 101.
Proof. done. Qed.
Global Instance normalize_end A (x : A): Normalize false x x | 100.
Proof. done. Qed.
Lemma normalize_fmap_length A B (f : A → B) l r p `{!Normalize p (length l) r} :
Normalize true (length (f <$> l)) r.
Proof. by rewrite fmap_length. Qed.
Hint Extern 5 (Normalize _ (length (_ <$> _)) _) => class_apply normalize_fmap_length : typeclass_instances.
Lemma normalize_insert_length A i (x : A) l r p `{!Normalize p (length l) r} :
Normalize true (length (<[i:=x]> l)) r.
Proof. by rewrite insert_length. Qed.
Hint Extern 5 (Normalize _ (length (<[_:=_]> _)) _) => class_apply normalize_insert_length : typeclass_instances.
Lemma normalize_app_length A (l1 l2 : list A) r1 r2 r3 p1 p2 p3
`{!Normalize p1 (length l1) r1} `{!Normalize p2 (length l2) r2} `{!Normalize p3 (r1 + r2)%nat r3}:
Normalize true (length (l1 ++ l2)) r3.
Proof. unfold Normalize in *; subst. by rewrite app_length. Qed.
Hint Extern 5 (Normalize _ (length (_ ++ _)) _) => class_apply normalize_app_length : typeclass_instances.
Lemma normalize_app_assoc A (l1 l2 l3 : list A) r1 r2 p1 p2
`{!Normalize p1 (l2 ++ l3) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true ((l1 ++ l2) ++ l3) r2.
Proof. unfold Normalize in *; subst. by rewrite -app_assoc. Qed.
Hint Extern 5 (Normalize _ (((_ ++ _) ++ _)) _) => class_apply normalize_app_assoc : typeclass_instances.
Lemma normalize_cons_middle A x (l1 l2 : list A) r1 r2 p1 p2
`{!Normalize p1 (x :: l2) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true (l1 ++ [x] ++ l2) r2.
Proof. unfold Normalize in *; subst. by rewrite -cons_middle. Qed.
(* The hint extern is especially imporant for this lemma as otherwise
tc search loops on goal of form l ++ [_]. *)
Hint Extern 5 (Normalize _ (_ ++ [_] ++ _) _) => class_apply normalize_cons_middle : typeclass_instances.
Lemma normalize_app_nil_r A (l : list A):
Normalize true (l ++ []) l.
Proof. unfold Normalize in *; subst. by rewrite app_nil_r. Qed.
Hint Extern 5 (Normalize _ (_ ++ []) _) => class_apply normalize_app_nil_r : typeclass_instances.
Lemma normalize_rev_involutive A (l : list A):
Normalize true (rev (rev l)) l.
Proof. unfold Normalize in *; subst. by rewrite rev_involutive. Qed.
Hint Extern 5 (Normalize _ (rev (rev _)) _) => class_apply normalize_rev_involutive : typeclass_instances.
Lemma normalize_minus_n_O n:
Normalize true (n - 0)%nat n.
Proof. unfold Normalize in *; subst. by rewrite -minus_n_O. Qed.
Hint Extern 5 (Normalize _ (_ - 0)%nat _) => class_apply normalize_minus_n_O : typeclass_instances.
Lemma normalize_rotate_length A n (l : list A) r p `{!Normalize p (length l) r} :
Normalize true (length (rotate n l)) r.
Proof. by rewrite rotate_length. Qed.
Hint Extern 5 (Normalize _ (length (rotate _ _)) _) => class_apply normalize_rotate_length : typeclass_instances.
Lemma normalize_replicate_length A n (l : list A) :
Normalize true (length (replicate n l)) n.
Proof. by rewrite replicate_length. Qed.
Hint Extern 5 (Normalize _ (length (replicate _ _)) _) => class_apply normalize_replicate_length : typeclass_instances.
Ltac normalize_tc :=
first [
lazymatch goal with
| |- ?a = ?b => change_no_check (NormalizeWalk true a b); solve [refine _]
end
| exact: eq_refl].
theories/lithium/solvers.v 0 → 100644
View file @ 079c2b54
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.
Ltac solve_goal :=
try fast_done;
solve_goal_prepare_tac;
normalize_and_simpl_goal;
solve_goal_normalized_prepare_tac; enrich_context;
repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //;
refined_solver lia.
theories/lithium/tactics.v
View file @ 079c2b54
From refinedc.lithium Require Export infrastructure simpl_classes simpl_instances interpreter tactics_extend.
From refinedc.lithium Require Export infrastructure simpl_classes simpl_instances interpreter tactics_extend normalize solvers.
theories/typing/automation/normalize.v
View file @ 079c2b54
From refinedc.typing Require Import type.
From refinedc.lithium Require Import tactics.
From refinedc.lithium Require Export normalize.
(** * First version of normalization based on [autorewrite] *)
Create HintDb refinedc_rewrite discriminated.
Ltac normalize_autorewrite :=
autorewrite with refinedc_rewrite; exact: eq_refl.
Hint Rewrite @drop_0 @take_ge using can_solve_tac : refinedc_rewrite.
Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : refinedc_rewrite.
Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : refinedc_rewrite.
Hint Rewrite <- @fmap_take @fmap_drop : refinedc_rewrite.
Hint Rewrite @list_insert_fold : refinedc_rewrite.
Hint Rewrite @list_insert_insert : refinedc_rewrite.
Hint Rewrite @drop_drop : refinedc_rewrite.
Hint Rewrite @tail_replicate @take_replicate @drop_replicate : refinedc_rewrite.
Hint Rewrite <- @app_assoc @cons_middle : refinedc_rewrite.
Hint Rewrite @app_nil_r @rev_involutive : refinedc_rewrite.
Hint Rewrite <- @list_fmap_insert : refinedc_rewrite.
Hint Rewrite <- minus_n_O plus_n_O minus_n_n : refinedc_rewrite.
Hint Rewrite Nat2Z.id : refinedc_rewrite.
Hint Rewrite Z2Nat.inj_mul Z2Nat.inj_sub Z2Nat.id using can_solve_tac : refinedc_rewrite.
Hint Rewrite Nat.succ_pred_pos using can_solve_tac : refinedc_rewrite.
Hint Rewrite Nat.add_assoc Nat.min_id : refinedc_rewrite.
Hint Rewrite Z.quot_mul using can_solve_tac : refinedc_rewrite.
Hint Rewrite <-Nat.mul_sub_distr_r Z.mul_add_distr_r Z.mul_sub_distr_r : refinedc_rewrite.
Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : refinedc_rewrite.
Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : refinedc_rewrite.
Hint Rewrite keep_factor2_min_1 keep_factor2_twice : refinedc_rewrite.
Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : refinedc_rewrite.
Hint Rewrite ly_size_ly_set_size ly_size_ly_with_align : refinedc_rewrite.
Local Definition lookup_insert_gmap A K `{Countable K} := lookup_insert (M := gmap K) (A := A).
Hint Rewrite lookup_insert_gmap : refinedc_rewrite.
Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : lithium_rewrite.
Hint Rewrite ly_size_ly_set_size ly_size_ly_with_align : lithium_rewrite.
(* The following lemma is a problem with Keyed Unification as it
unfolds e.g. layout_of *)
(* Lemma ly_size_of_mk_layout n : ly_size (mk_layout n) = n. *)
(* Proof. done. Qed. *)
(* Hint Rewrite ly_size_of_mk_layout : refinedc_rewrite. *)
(** * Second version of normalization based on typeclasses *)
Class NormalizeWalk {A} (progress : bool) (a b : A) : Prop := normalize_walk: a = b.
Class Normalize {A} (progress : bool) (a b : A) : Prop := normalize: a = b.
Hint Mode NormalizeWalk + - + - : typeclass_instances.
Hint Mode Normalize + - + - : typeclass_instances.
Global Instance normalize_walk_protected A (x : A) :
NormalizeWalk false (protected x) (protected x) | 10.
Proof. done. Qed.
(* TODO: This does not go under binders *)
Lemma normalize_walk_app A B (f f' : A → B) x x' r p1 p2 p3
`{!NormalizeWalk p1 f f'}
`{!NormalizeWalk p2 x x'} `{!TCEq (p1 || p2) true}
`{!Normalize p3 (f' x') r}:
NormalizeWalk true (f x) r.
Proof. unfold NormalizeWalk, Normalize in *. naive_solver. Qed.
Hint Extern 50 (NormalizeWalk _ (?f ?x) _) => class_apply normalize_walk_app : typeclass_instances.
Global Instance normalize_walk_end_progress A (x x' : A) `{!Normalize true x x'} :
NormalizeWalk true x x' | 100.
Proof. done. Qed.
Global Instance normalize_walk_end A (x : A) :
NormalizeWalk false x x | 101.
Proof. done. Qed.
Global Instance normalize_end A (x : A): Normalize false x x | 100.
Proof. done. Qed.
Lemma normalize_fmap_length A B (f : A → B) l r p `{!Normalize p (length l) r} :
Normalize true (length (f <$> l)) r.
Proof. by rewrite fmap_length. Qed.
Hint Extern 5 (Normalize _ (length (_ <$> _)) _) => class_apply normalize_fmap_length : typeclass_instances.
Lemma normalize_insert_length A i (x : A) l r p `{!Normalize p (length l) r} :
Normalize true (length (<[i:=x]> l)) r.
Proof. by rewrite insert_length. Qed.
Hint Extern 5 (Normalize _ (length (<[_:=_]> _)) _) => class_apply normalize_insert_length : typeclass_instances.
Lemma normalize_app_length A (l1 l2 : list A) r1 r2 r3 p1 p2 p3
`{!Normalize p1 (length l1) r1} `{!Normalize p2 (length l2) r2} `{!Normalize p3 (r1 + r2)%nat r3}:
Normalize true (length (l1 ++ l2)) r3.
Proof. unfold Normalize in *; subst. by rewrite app_length. Qed.
Hint Extern 5 (Normalize _ (length (_ ++ _)) _) => class_apply normalize_app_length : typeclass_instances.
Lemma normalize_app_assoc A (l1 l2 l3 : list A) r1 r2 p1 p2
`{!Normalize p1 (l2 ++ l3) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true ((l1 ++ l2) ++ l3) r2.
Proof. unfold Normalize in *; subst. by rewrite -app_assoc. Qed.
Hint Extern 5 (Normalize _ (((_ ++ _) ++ _)) _) => class_apply normalize_app_assoc : typeclass_instances.
Lemma normalize_cons_middle A x (l1 l2 : list A) r1 r2 p1 p2
`{!Normalize p1 (x :: l2) r1} `{!Normalize p2 (l1 ++ r1) r2}:
Normalize true (l1 ++ [x] ++ l2) r2.
Proof. unfold Normalize in *; subst. by rewrite -cons_middle. Qed.
(* The hint extern is especially imporant for this lemma as otherwise
tc search loops on goal of form l ++ [_]. *)
Hint Extern 5 (Normalize _ (_ ++ [_] ++ _) _) => class_apply normalize_cons_middle : typeclass_instances.
Lemma normalize_app_nil_r A (l : list A):
Normalize true (l ++ []) l.
Proof. unfold Normalize in *; subst. by rewrite app_nil_r. Qed.
Hint Extern 5 (Normalize _ (_ ++ []) _) => class_apply normalize_app_nil_r : typeclass_instances.
Lemma normalize_rev_involutive A (l : list A):
Normalize true (rev (rev l)) l.
Proof. unfold Normalize in *; subst. by rewrite rev_involutive. Qed.
Hint Extern 5 (Normalize _ (rev (rev _)) _) => class_apply normalize_rev_involutive : typeclass_instances.
Lemma normalize_minus_n_O n:
Normalize true (n - 0)%nat n.
Proof. unfold Normalize in *; subst. by rewrite -minus_n_O. Qed.
Hint Extern 5 (Normalize _ (_ - 0)%nat _) => class_apply normalize_minus_n_O : typeclass_instances.
Lemma normalize_rotate_length A n (l : list A) r p `{!Normalize p (length l) r} :
Normalize true (length (rotate n l)) r.
Proof. by rewrite rotate_length. Qed.
Hint Extern 5 (Normalize _ (length (rotate _ _)) _) => class_apply normalize_rotate_length : typeclass_instances.
Lemma normalize_replicate_length A n (l : list A) :
Normalize true (length (replicate n l)) n.
Proof. by rewrite replicate_length. Qed.
Hint Extern 5 (Normalize _ (length (replicate _ _)) _) => class_apply normalize_replicate_length : typeclass_instances.
Ltac normalize_tc :=
first [
lazymatch goal with
| |- ?a = ?b => change_no_check (NormalizeWalk true a b); solve [refine _]
end
| exact: eq_refl].
(* Hint Rewrite ly_size_of_mk_layout : lithium_rewrite. *)
theories/typing/automation/proof_state.v
View file @ 079c2b54
......@@ -81,11 +81,9 @@ Ltac prepare_sideconditions :=
end;
clear_unused_vars.
Ltac solve_goal :=
try fast_done;
Ltac solve_goal_prepare_tac ::=
prepare_sideconditions;
repeat match goal with | H : CASE_DISTINCTION_INFO _ _ _ |- _ => clear H end;
unprepared_solve_goal.
repeat match goal with | H : CASE_DISTINCTION_INFO _ _ _ |- _ => clear H end.
(** * Tactics for showing failures to the user *)
Ltac clear_for_print_goal :=
......
theories/typing/automation/solvers.v
View file @ 079c2b54
From refinedc.typing Require Import type.
From refinedc.lithium Require Import tactics.
(** * [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;