Commit 2f42e910 by Robbert Krebbers

### Make naive_solver deal with some Boolean connectives.

parent 693ced62
 ... ... @@ -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. ... ...
 ... ... @@ -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 stdpp Require Export numbers base decidable option. From stdpp Require Export numbers base option. Arguments length {_} _. Arguments cons {_} _ _. ... ...
 ... ... @@ -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 stdpp Require Export base decidable collections list. From stdpp Require Export collections list. Record listset A := Listset { listset_car: list A }. Arguments listset_car {_} _. ... ...
 ... ... @@ -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 stdpp Require Export base decidable collections list. From stdpp Require Export collections list. Record listset_nodup A := ListsetNoDup { listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car ... ...
 ... ... @@ -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 stdpp Require Export base tactics decidable. From stdpp 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) ... ...
 ... ... @@ -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 stdpp Require Export base decidable tactics list. From stdpp Require Export tactics list. (** * Arbitrary pre-, parial and total orders *) (** Properties about arbitrary pre-, partial, and total orders. We do not use ... ...
 ... ... @@ -3,7 +3,6 @@ From stdpp Require Export base tactics decidable orders option vector ... ...
 ... ... @@ -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 stdpp Require Export tactics. From stdpp 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.
 ... ... @@ -4,7 +4,7 @@ the development. *) From Coq Require Import Omega. From Coq Require Export Psatz. From stdpp Require Export base. From stdpp 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] ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!