aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Decidableplus.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Decidableplus.v')
-rw-r--r--lib/Decidableplus.v244
1 files changed, 244 insertions, 0 deletions
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
new file mode 100644
index 00000000..932b885a
--- /dev/null
+++ b/lib/Decidableplus.v
@@ -0,0 +1,244 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(** This library provides type classes and tactics to decide logical
+ propositions by reflection into computable Boolean equalities.
+ It extends the [DecidableClass] module from the standard library
+ of Coq 8.5 with more instances of decidable properties, including
+ universal and existential quantification over finite types. *)
+
+(** Temporarily and for compatibility with Coq 8.4, this file includes
+ a copy of the relevant definitions from the Coq 8.5 [DecidableClass]
+ library. This library is copyright INRIA. *)
+
+Require Import Coqlib.
+
+Class Decidable (P : Prop) := {
+ Decidable_witness : bool;
+ Decidable_spec : Decidable_witness = true <-> P
+}.
+
+Lemma Decidable_sound : forall P (H : Decidable P),
+ Decidable_witness = true -> P.
+Proof.
+ intros. rewrite <- Decidable_spec. auto.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+ P -> Decidable_witness = true.
+Proof.
+ intros. rewrite Decidable_spec. auto.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+ ~ P -> Decidable_witness = false.
+Proof.
+ intros. destruct Decidable_witness eqn:E; auto. elim H0. eapply Decidable_sound; eauto.
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+ Decidable_witness = false -> ~ P.
+Proof.
+ intros; red; intros. rewrite (Decidable_complete P H) in H0 by auto. discriminate.
+Qed.
+
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
+
+Ltac _decide_ P H :=
+ let b := fresh "b" in
+ set (b := decide P) in *;
+ assert (H : decide P = b) by reflexivity;
+ clearbody b;
+ destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H].
+
+Tactic Notation "decide" constr(P) "as" ident(H) :=
+ _decide_ P H.
+
+Tactic Notation "decide" constr(P) :=
+ let H := fresh "H" in _decide_ P H.
+
+Ltac decide_goal := eapply Decidable_sound; reflexivity.
+
+(** Deciding logical connectives *)
+
+Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
+ Decidable_witness := negb (@Decidable_witness P dP)
+}.
+Next Obligation.
+ rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt.
+Qed.
+
+Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
+ Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
+}.
+Next Obligation.
+ rewrite eqb_true_iff.
+ split; intros.
+ split; intros; eapply Decidable_sound; [rewrite <- H | rewrite H]; eapply Decidable_complete; eauto.
+ destruct (@Decidable_witness Q dQ) eqn:D.
+ eapply Decidable_complete; rewrite H; eapply Decidable_sound; eauto.
+ eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto.
+Qed.
+
+Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
+ Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
+}.
+Next Obligation.
+ rewrite andb_true_iff. rewrite ! Decidable_spec. tauto.
+Qed.
+
+Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
+ Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
+}.
+Next Obligation.
+ rewrite orb_true_iff. rewrite ! Decidable_spec. tauto.
+Qed.
+
+Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
+ Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
+}.
+Next Obligation.
+ split.
+- intros. rewrite Decidable_complete in H by auto. eapply Decidable_sound; eauto.
+- intros. destruct (@Decidable_witness P dP) eqn:WP; auto.
+ eapply Decidable_complete. apply H. eapply Decidable_sound; eauto.
+Qed.
+
+(** Deciding equalities. *)
+
+Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y}) (x y: A) : Decidable (eq x y) := {|
+ Decidable_witness := proj_sumbool (eqdec x y)
+|}.
+Next Obligation.
+ split; intros. InvBooleans. auto. subst y. apply dec_eq_true.
+Qed.
+
+Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
+ Decidable_witness := Bool.eqb x y
+}.
+Next Obligation.
+ apply eqb_true_iff.
+Qed.
+
+Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
+ Decidable_witness := beq_nat x y
+}.
+Next Obligation.
+ apply beq_nat_true_iff.
+Qed.
+
+Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
+ Decidable_witness := Pos.eqb x y
+}.
+Next Obligation.
+ apply Pos.eqb_eq.
+Qed.
+
+Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
+ Decidable_witness := Z.eqb x y
+}.
+Next Obligation.
+ apply Z.eqb_eq.
+Qed.
+
+(** Deciding order on Z *)
+
+Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
+ Decidable_witness := Z.leb x y
+}.
+Next Obligation.
+ apply Z.leb_le.
+Qed.
+
+Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
+ Decidable_witness := Z.ltb x y
+}.
+Next Obligation.
+ apply Z.ltb_lt.
+Qed.
+
+(** Deciding properties over lists *)
+
+Program Instance Decidable_forall_in_list :
+ forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
+ Decidable (forall x:A, In x l -> P x) := {
+ Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
+}.
+Next Obligation.
+ rewrite List.forallb_forall. split; intros.
+- eapply Decidable_sound; eauto.
+- eapply Decidable_complete; eauto.
+Qed.
+
+Program Instance Decidable_exists_in_list :
+ forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
+ Decidable (exists x:A, In x l /\ P x) := {
+ Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
+}.
+Next Obligation.
+ rewrite List.existsb_exists. split.
+- intros (x & U & V). exists x; split; auto. eapply Decidable_sound; eauto.
+- intros (x & U & V). exists x; split; auto. eapply Decidable_complete; eauto.
+Qed.
+
+(** Types with finitely many elements. *)
+
+Class Finite (T: Type) := {
+ Finite_elements: list T;
+ Finite_elements_spec: forall x:T, In x Finite_elements
+}.
+
+(** Deciding forall and exists quantification over finite types. *)
+
+Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
+ Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
+}.
+Next Obligation.
+ rewrite List.forallb_forall. split; intros.
+- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec.
+- eapply Decidable_complete; eauto.
+Qed.
+
+Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
+ Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
+}.
+Next Obligation.
+ rewrite List.existsb_exists. split.
+- intros (x & A & B). exists x. eapply Decidable_sound; eauto.
+- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto.
+Qed.
+
+(** Some examples of finite types. *)
+
+Program Instance Finite_bool : Finite bool := {
+ Finite_elements := false :: true :: nil
+}.
+Next Obligation.
+ destruct x; auto.
+Qed.
+
+Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
+ Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
+}.
+Next Obligation.
+ apply List.in_prod; eapply Finite_elements_spec.
+Qed.
+
+Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
+ Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
+}.
+Next Obligation.
+ destruct x; auto. right; apply List.in_map; eapply Finite_elements_spec.
+Qed.
generated by cgit (git 2.34.1) at 2024-06-03 03:50:05 +0000