Commit 39c7307f authored by Robbert Krebbers's avatar Robbert Krebbers

Make naive_solver deal with some Boolean connectives.

parent 8ca359a5
...@@ -11,7 +11,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P. ...@@ -11,7 +11,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b. 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. Instance: Inj (=) () Is_true.
Proof. intros [] []; simpl; intuition. Qed. Proof. intros [] []; simpl; intuition. Qed.
...@@ -24,17 +24,17 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x ...@@ -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. (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)} 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). (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) : Lemma decide_True {A} `{Decision P} (x y : A) :
P (if decide P then x else y) = x. 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) : Lemma decide_False {A} `{Decision P} (x y : A) :
¬P (if decide P then x else y) = y. ¬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) : 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). (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 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
components is double negated, it will try to remove the double negation. *) 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 := ...@@ -95,7 +95,7 @@ Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
if dec then true else false. if dec then true else false.
Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P). 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) := Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with match goal with
...@@ -108,15 +108,15 @@ Tactic Notation "case_bool_decide" := ...@@ -108,15 +108,15 @@ Tactic Notation "case_bool_decide" :=
let H := fresh in case_bool_decide as H. let H := fresh in case_bool_decide as H.
Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P P. 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. 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. 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. 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. 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} : Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
(P Q) bool_decide P = bool_decide Q. (P Q) bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed. Proof. repeat case_bool_decide; tauto. Qed.
...@@ -138,7 +138,7 @@ Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)} ...@@ -138,7 +138,7 @@ Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
Proof. apply (sig_eq_pi _). Qed. Proof. apply (sig_eq_pi _). Qed.
Lemma dexists_proj1 `(P : A Prop) `{ x, Decision (P x)} (x : dsig P) p : Lemma dexists_proj1 `(P : A Prop) `{ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x. dexist (`x) p = x.
Proof. by apply dsig_eq. Qed. Proof. apply dsig_eq; reflexivity. Qed.
(** * Instances of Decision *) (** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *) (** 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 : ...@@ -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)} Instance sig_eq_dec `(P : A Prop) `{ x, ProofIrrel (P x)}
`{ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y). `{ 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 *) (** Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P Q) ¬P ¬Q. Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P Q) ¬P ¬Q.
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file collects general purpose definitions and theorems on lists that (** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *) are not in the Coq standard library. *)
From Coq Require Export Permutation. From Coq Require Export Permutation.
From prelude Require Export numbers base decidable option. From prelude Require Export numbers base option.
Arguments length {_} _. Arguments length {_} _.
Arguments cons {_} _ _. Arguments cons {_} _ _.
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates (** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *) 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 }. Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _. Arguments listset_car {_} _.
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file implements finite as unordered lists without duplicates. (** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *) 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 { Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option (** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *) 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 := Inductive option_reflect {A} (P : A Prop) (Q : Prop) : option A Type :=
| ReflectSome x : P x option_reflect P Q (Some x) | ReflectSome x : P x option_reflect P Q (Some x)
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file collects common properties of pre-orders and semi lattices. This (** 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. *) theory will mainly be used for the theory on collections and finite maps. *)
From Coq Require Export Sorted. 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 *) (** * Arbitrary pre-, parial and total orders *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use (** Properties about arbitrary pre-, partial, and total orders. We do not use
......
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
From prelude Require Export From prelude Require Export
base base
tactics tactics
decidable
orders orders
option option
vector vector
......
...@@ -2,20 +2,20 @@ ...@@ -2,20 +2,20 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *) (** This file collects facts on proof irrelevant types/propositions. *)
From Coq Require Import Eqdep_dec. 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. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
Instance: ProofIrrel True. Instance: ProofIrrel True.
Proof. by intros [] []. Qed. Proof. intros [] []; reflexivity. Qed.
Instance: ProofIrrel False. Instance: ProofIrrel False.
Proof. by intros []. Qed. Proof. intros []. Qed.
Instance and_pi (A B : Prop) : Instance and_pi (A B : Prop) :
ProofIrrel A ProofIrrel B ProofIrrel (A B). 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) : Instance prod_pi (A B : Type) :
ProofIrrel A ProofIrrel B ProofIrrel (A * B). 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) : Instance eq_pi {A} `{ x y : A, Decision (x = y)} (x y : A) :
ProofIrrel (x = y). ProofIrrel (x = y).
Proof. Proof.
...@@ -27,10 +27,10 @@ Proof. destruct b; simpl; apply _. Qed. ...@@ -27,10 +27,10 @@ Proof. destruct b; simpl; apply _. Qed.
Lemma sig_eq_pi `(P : A Prop) `{ x, ProofIrrel (P x)} Lemma sig_eq_pi `(P : A Prop) `{ x, ProofIrrel (P x)}
(x y : sig P) : x = y `x = `y. (x y : sig P) : x = y `x = `y.
Proof. Proof.
split; [by intros <- |]. split; [intros <-; reflexivity|].
destruct x as [x Hx], y as [y Hy]; simpl; intros; subst. destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
f_equal. apply proof_irrel. f_equal. apply proof_irrel.
Qed. Qed.
Lemma exists_proj1_pi `(P : A Prop) `{ x, ProofIrrel (P x)} Lemma exists_proj1_pi `(P : A Prop) `{ x, ProofIrrel (P x)}
(x : sig P) p : `x 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 @@ ...@@ -4,7 +4,7 @@
the development. *) the development. *)
From Coq Require Import Omega. From Coq Require Import Omega.
From Coq Require Export Psatz. 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. Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x.
Proof. intros ->; reflexivity. Qed. Proof. intros ->; reflexivity. Qed.
...@@ -430,6 +430,8 @@ Tactic Notation "naive_solver" tactic(tac) := ...@@ -430,6 +430,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
| H : _ _ |- _ => destruct H | H : _ _ |- _ => destruct H
| H : _, _ |- _ => destruct H | H : _, _ |- _ => destruct H
| H : ?P ?Q, H2 : ?P |- _ => specialize (H H2) | 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 *) (**i simplify and solve equalities *)
| |- _ => progress simplify_eq/= | |- _ => progress simplify_eq/=
(**i solve the goal *) (**i solve the goal *)
...@@ -441,6 +443,8 @@ Tactic Notation "naive_solver" tactic(tac) := ...@@ -441,6 +443,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
| reflexivity ] | reflexivity ]
(**i operations that generate more subgoals *) (**i operations that generate more subgoals *)
| |- _ _ => split | |- _ _ => split
| |- Is_true (bool_decide _) => apply (bool_decide_pack _)
| |- Is_true (_ && _) => apply andb_True; split
| H : _ _ |- _ => destruct H | H : _ _ |- _ => destruct H
(**i solve the goal using the user supplied tactic *) (**i solve the goal using the user supplied tactic *)
| |- _ => solve [tac] | |- _ => solve [tac]
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment