From ab4c5855d8e7aecbeee8ff2ba83aada46f9bcef0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 3 May 2021 20:23:16 +0200
Subject: [PATCH] add tactic for solving computable goals
---
theories/decidable.v | 5 +++++
theories/list.v | 4 ++--
theories/numbers.v | 18 +++++++++---------
3 files changed, 16 insertions(+), 11 deletions(-)
diff --git a/theories/decidable.v b/theories/decidable.v
index 310eff9a..5471e733 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,6 +135,11 @@ Proof. apply bool_decide_eq_false. Qed.
Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
Proof. apply bool_decide_eq_false. Qed.
+(** The tactic [compute_done] solves a decidable goal by computing that it is
+true. *)
+Tactic Notation "compute_done" :=
+ apply (bool_decide_unpack _); vm_compute; exact I.
+
(** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2.
Notation bool_decide_false := bool_decide_eq_false_2.
diff --git a/theories/list.v b/theories/list.v
index 4468f28b..07bd5a51 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4537,7 +4537,7 @@ Ltac quote_Permutation :=
end.
Ltac solve_Permutation :=
quote_Permutation; apply rlist.eval_Permutation;
- apply (bool_decide_unpack _); by vm_compute.
+ compute_done.
Ltac quote_submseteq :=
match goal with
@@ -4549,7 +4549,7 @@ Ltac quote_submseteq :=
end.
Ltac solve_submseteq :=
quote_submseteq; apply rlist.eval_submseteq;
- apply (bool_decide_unpack _); by vm_compute.
+ compute_done.
Ltac decompose_elem_of_list := repeat
match goal with
diff --git a/theories/numbers.v b/theories/numbers.v
index bce80ceb..5b520176 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -856,7 +856,7 @@ Lemma Qp_mul_1_r p : p * 1 = p.
Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed.
Lemma Qp_1_1 : 1 + 1 = 2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_add_diag p : p + p = 2 * p.
Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed.
@@ -884,11 +884,11 @@ Proof.
by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
Qed.
Lemma Qp_inv_1 : /1 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_inv_half_half : /2 + /2 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_div_diag p : p / p = 1.
Proof. apply Qp_mul_inv_r. Qed.
@@ -917,13 +917,13 @@ Qed.
Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
Proof. unfold Qp_div; apply _. Qed.
Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
@@ -1218,7 +1218,7 @@ Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q.
Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed.
Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m.
Proof. by injection 1. Qed.
Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.
--
GitLab