From 39c7307f809bc06546cb9ab44be61975a852503f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Mar 2016 14:00:33 +0100
Subject: [PATCH] Make naive_solver deal with some Boolean connectives.

---
 prelude/decidable.v     | 26 +++++++++++++-------------
 prelude/list.v          |  2 +-
 prelude/listset.v       |  2 +-
 prelude/listset_nodup.v |  2 +-
 prelude/option.v        |  2 +-
 prelude/orders.v        |  2 +-
 prelude/prelude.v       |  1 -
 prelude/proof_irrel.v   | 14 +++++++-------
 prelude/tactics.v       |  6 +++++-
 9 files changed, 30 insertions(+), 27 deletions(-)

diff --git a/prelude/decidable.v b/prelude/decidable.v
index 3e453e931..d57c025c5 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -11,7 +11,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
-Proof. destruct b. by left. right. intros []. Qed.
+Proof. destruct b. left; constructor. right. intros []. Qed.
 Instance: Inj (=) (↔) Is_true.
 Proof. intros [] []; simpl; intuition. Qed.
 
@@ -24,17 +24,17 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x
   (x : A) (y : B) : Decision (R x y) := dec x y.
 Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y)}
   (x : A) (y : B) : decide_rel R x y = decide (R x y).
-Proof. done. Qed.
+Proof. reflexivity. Qed.
 
 Lemma decide_True {A} `{Decision P} (x y : A) :
   P → (if decide P then x else y) = x.
-Proof. by destruct (decide P). Qed.
+Proof. destruct (decide P); tauto. Qed.
 Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
-Proof. by destruct (decide P). Qed.
+Proof. destruct (decide P); tauto. Qed.
 Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
-Proof. intros [??]. destruct (decide P), (decide Q); intuition. Qed.
+Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
 components is double negated, it will try to remove the double negation. *)
@@ -95,7 +95,7 @@ Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
 
 Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
-Proof. unfold bool_decide. destruct dec. by left. by right. Qed.
+Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
 
 Tactic Notation "case_bool_decide" "as" ident (Hd) :=
   match goal with
@@ -108,15 +108,15 @@ Tactic Notation "case_bool_decide" :=
   let H := fresh in case_bool_decide as H.
 
 Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P.
-Proof. unfold bool_decide. by destruct dec. Qed.
+Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
 Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
-Proof. by rewrite bool_decide_spec. Qed.
+Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
-Proof. by rewrite bool_decide_spec. Qed.
+Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
-Proof. by case_bool_decide. Qed.
+Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
-Proof. by case_bool_decide. Qed.
+Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
 Proof. repeat case_bool_decide; tauto. Qed.
@@ -138,7 +138,7 @@ Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
 Proof. apply (sig_eq_pi _). Qed.
 Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
-Proof. by apply dsig_eq. Qed.
+Proof. apply dsig_eq; reflexivity. Qed.
 
 (** * Instances of Decision *)
 (** Instances of [Decision] for operators of propositional logic. *)
@@ -184,7 +184,7 @@ Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
 
 Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
-Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
+Proof. refine (cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined.
 
 (** Some laws for decidable propositions *)
 Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
diff --git a/prelude/list.v b/prelude/list.v
index 025e8c278..f7527b30c 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -3,7 +3,7 @@
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
 From Coq Require Export Permutation.
-From prelude Require Export numbers base decidable option.
+From prelude Require Export numbers base option.
 
 Arguments length {_} _.
 Arguments cons {_} _ _.
diff --git a/prelude/listset.v b/prelude/listset.v
index a2ac816b1..fb8e8145b 100644
--- a/prelude/listset.v
+++ b/prelude/listset.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
-From prelude Require Export base decidable collections list.
+From prelude Require Export collections list.
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _.
diff --git a/prelude/listset_nodup.v b/prelude/listset_nodup.v
index f6d9c1971..40ee72baa 100644
--- a/prelude/listset_nodup.v
+++ b/prelude/listset_nodup.v
@@ -3,7 +3,7 @@
 (** This file implements finite as unordered lists without duplicates.
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
-From prelude Require Export base decidable collections list.
+From prelude Require Export collections list.
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/prelude/option.v b/prelude/option.v
index b80a955e4..90d7bc3ec 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
-From prelude Require Export base tactics decidable.
+From prelude Require Export tactics.
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/prelude/orders.v b/prelude/orders.v
index 423dc320e..93f0717b2 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -3,7 +3,7 @@
 (** This file collects common properties of pre-orders and semi lattices. This
 theory will mainly be used for the theory on collections and finite maps. *)
 From Coq Require Export Sorted.
-From prelude Require Export base decidable tactics list.
+From prelude Require Export tactics list.
 
 (** * Arbitrary pre-, parial and total orders *)
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
diff --git a/prelude/prelude.v b/prelude/prelude.v
index 3ffdba617..ad1f1cb45 100644
--- a/prelude/prelude.v
+++ b/prelude/prelude.v
@@ -3,7 +3,6 @@
 From prelude Require Export
   base
   tactics
-  decidable
   orders
   option
   vector
diff --git a/prelude/proof_irrel.v b/prelude/proof_irrel.v
index 7aebbb862..381a8a91f 100644
--- a/prelude/proof_irrel.v
+++ b/prelude/proof_irrel.v
@@ -2,20 +2,20 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 From Coq Require Import Eqdep_dec.
-From prelude Require Export tactics.
+From prelude Require Export base.
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
 Instance: ProofIrrel True.
-Proof. by intros [] []. Qed.
+Proof. intros [] []; reflexivity. Qed.
 Instance: ProofIrrel False.
-Proof. by intros []. Qed.
+Proof. intros []. Qed.
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
-Proof. intros ?? [??] [??]. by f_equal. Qed.
+Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
 Instance prod_pi (A B : Type) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
-Proof. intros ?? [??] [??]. by f_equal. Qed.
+Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
 Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) :
   ProofIrrel (x = y).
 Proof.
@@ -27,10 +27,10 @@ Proof. destruct b; simpl; apply _. Qed.
 Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x y : sig P) : x = y ↔ `x = `y.
 Proof.
-  split; [by intros <- |].
+  split; [intros <-; reflexivity|].
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x : sig P) p : `x ↾ p = x.
-Proof. by apply (sig_eq_pi _). Qed.
+Proof. apply (sig_eq_pi _); reflexivity. Qed.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index f8d438693..791e74159 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -4,7 +4,7 @@
 the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Psatz.
-From prelude Require Export base.
+From prelude Require Export decidable.
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
@@ -430,6 +430,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : _ ∧ _ |- _ => destruct H
   | H : ∃ _, _  |- _ => destruct H
   | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
+  | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
+  | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
   (**i solve the goal *)
@@ -441,6 +443,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
     | reflexivity ]
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
+  | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
+  | |- Is_true (_ && _) => apply andb_True; split
   | H : _ ∨ _ |- _ => destruct H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]
-- 
GitLab