Timings for Decidable.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import
Basics.Overture
Basics.PathGroupoids
Basics.Trunc
Basics.Tactics.
Local Open Scope trunc_scope.
Local Open Scope path_scope.
(** * Decidability *)
(** ** Definitions *)
(* NB: This has to come after our definition of [not] (which is in [Overture]), so that it refers to our [not] rather than the one in [Coq.Logic]. *)
Class Decidable (A : Type) :=
dec : A + (~ A).
(** The [decide_type] and [decide] tactic allow to automatically prove
decidable claims using previously written decision procedures that
compute. *)
Ltac decide_type A :=
let K := (eval hnf in (dec A)) in
match K with
| inl ?Z => exact Z
| inr ?Z => exact Z
end.
Ltac decide :=
match goal with
| [|- ?A] => decide_type A
end.
Class DecidablePaths (A : Type) :=
dec_paths : forall (x y : A), Decidable (x = y).
Global Existing Instance dec_paths.
Class Stable P := stable : ~~P -> P.
Global Instance stable_decidable P `{!Decidable P} : Stable P.
intros dn;destruct (dec P) as [p|n].
Global Instance stable_negation P : Stable (~ P).
exact (nnnp (fun np => np p)).
(**
Because [vm_compute] evaluates terms in [PROP] eagerly
and does not remove dead code we
need the decide_rel hack. Suppose we have [(x = y) =def (f x = f y)], now:
bool_decide (x = y) -> bool_decide (f x = f y) -> ...
As we see, the dead code [f x] and [f y] is actually evaluated,
which is of course an utter waste.
Therefore we introduce decide_rel and bool_decide_rel.
bool_decide_rel (=) x y -> bool_decide_rel (fun a b => f a = f b) x y -> ...
Now the definition of equality remains under a lambda and
our problem does not occur anymore!
*)
Definition decide_rel {A B} (R : A -> B -> Type)
{dec : forall x y, Decidable (R x y)} (x : A) (y : B)
: Decidable (R x y)
:= dec x y.
(** ** Decidable hprops *)
(** Contractible types are decidable. *)
Global Instance decidable_contr X `{Contr X} : Decidable X
:= inl (center X).
(** Thus, hprops have decidable equality. *)
Global Instance decidablepaths_hprop X `{IsHProp X} : DecidablePaths X
:= fun x y => dec (x = y).
(** Empty types are trivial. *)
Global Instance decidable_empty : Decidable Empty
:= inr idmap.
(** ** Transfer along equivalences *)
Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
: Decidable A -> Decidable B.
exact (inr (fun b => na (f^-1 b))).
Definition decidable_equiv' (A : Type) {B : Type} (f : A <~> B)
: Decidable A -> Decidable B
:= decidable_equiv A f.
Definition decidablepaths_equiv
(A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
: DecidablePaths A -> DecidablePaths B.
destruct (d (f^-1 x) (f^-1 y)) as [e|ne].
exact ((eisretr f x)^ @ ap f e @ eisretr f y).
Definition decidablepaths_equiv' (A : Type) {B : Type} (f : A <~> B)
: DecidablePaths A -> DecidablePaths B
:= decidablepaths_equiv A f.
(** ** Hedberg's theorem: any type with decidable equality is a set. *)
(** A weakly constant function is one all of whose values are equal (in a specified way). *)
Class WeaklyConstant {A B} (f : A -> B) :=
wconst : forall x y, f x = f y.
(** Any map that factors through an hprop is weakly constant. *)
Definition wconst_through_hprop {A B P} `{IsHProp P}
(f : A -> P) (g : P -> B)
: WeaklyConstant (g o f).
intros x y; apply (ap g), path_ishprop.
(** A type is collapsible if it admits a weakly constant endomap. *)
Class Collapsible (A : Type) :=
{ collapse : A -> A ;
wconst_collapse : WeaklyConstant collapse
}.
Global Existing Instance wconst_collapse.
Class PathCollapsible (A : Type) :=
path_coll : forall (x y : A), Collapsible (x = y).
Global Existing Instance path_coll.
Global Instance collapsible_decidable (A : Type) `{Decidable A}
: Collapsible A.
destruct (dec A) as [a | na].
intros x y; destruct (na x).
Global Instance pathcoll_decpaths (A : Type) `{DecidablePaths A}
: PathCollapsible A.
(** We give this a relatively high-numbered priority so that in deducing [IsHProp -> IsHSet] Coq doesn't detour via [DecidablePaths]. *)
Global Instance hset_pathcoll (A : Type) `{PathCollapsible A}
: IsHSet A | 1000.
assert (h : forall p:x=y, p = (collapse (idpath x))^ @ collapse p).
intros []; symmetry; by apply concat_Vp.
apply hprop_allpath; intros p q.
refine (h p @ _ @ (h q)^).
Definition collapsible_hprop (A : Type) `{IsHProp A}
: Collapsible A.
intros x y; apply path_ishprop.
Definition pathcoll_hset (A : Type) `{IsHSet A}
: PathCollapsible A.
intros x y; apply collapsible_hprop; exact _.
Corollary hset_decpaths (A : Type) `{DecidablePaths A}
: IsHSet A.
(** ** Truncation *)
(** Having decidable equality (which implies being an hset, by Hedberg's theorem above) is itself an hprop. *)
Global Instance ishprop_decpaths `{Funext} (A : Type)
: IsHProp (DecidablePaths A).
apply hprop_inhabited_contr; intros d.
assert (IsHSet A) by exact _.
apply path_forall; intros x; apply path_forall; intros y.
generalize (d x y); clear d; intros d.
generalize (d' x y); clear d'; intros d'.
destruct d as [d|nd]; destruct d' as [d'|nd'].
apply ap, path_forall; intros p; elim (nd p).