(* -*- mode: coq; mode: visual-line -*-  *)
Require Import
  Basics.Overture
  Basics.PathGroupoids
  Basics.Trunc
  Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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).
Arguments dec 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.
P: Type
Decidable0: Decidable P
Stable P
Proof.
P: Type
Decidable0: Decidable P
Stable P
  intros dn;destruct (dec P) as [p|n].
P: Type
Decidable0: Decidable P
dn: ~~ P
p: P
P
P: Type
Decidable0: Decidable P
dn: ~~ P
n: ~ P
P
  -
P: Type
Decidable0: Decidable P
dn: ~~ P
p: P
P assumption.
  -
P: Type
Decidable0: Decidable P
dn: ~~ P
n: ~ P
P apply Empty_rect,dn,n.
Qed.

Global Instance stable_negation P : Stable (~ P).
P: Type
Stable (~ P)
Proof.
P: Type
Stable (~ P)
  intros nnnp p.
P: Type
nnnp: ~~ ~ P
p: P
Empty
  exact (nnnp (fun np => np p)).
Defined.

(**
  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.
A, B: Type
f: A -> B
H: IsEquiv f
Decidable A -> Decidable B
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
Decidable A -> Decidable B
  intros [a|na].
A, B: Type
f: A -> B
H: IsEquiv f
a: A
Decidable B
A, B: Type
f: A -> B
H: IsEquiv f
na: ~ A
Decidable B
  -
A, B: Type
f: A -> B
H: IsEquiv f
a: A
Decidable B exact (inl (f a)).
  -
A, B: Type
f: A -> B
H: IsEquiv f
na: ~ A
Decidable B exact (inr (fun b => na (f^-1 b))).
Defined.

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.
A, B: Type
f: A -> B
H: IsEquiv f
DecidablePaths A -> DecidablePaths B
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
DecidablePaths A -> DecidablePaths B
  intros d x y.
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
Decidable (x = y)
  destruct (d (f^-1 x) (f^-1 y)) as [e|ne].
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
e: f^-1 x = f^-1 y
Decidable (x = y)
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
ne: f^-1 x <> f^-1 y
Decidable (x = y)
  -
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
e: f^-1 x = f^-1 y
Decidable (x = y) apply inl.
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
e: f^-1 x = f^-1 y
x = y exact ((eisretr f x)^ @ ap f e @ eisretr f y).
  -
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
ne: f^-1 x <> f^-1 y
Decidable (x = y) apply inr; intros p.
A, B: Type
f: A -> B
H: IsEquiv f
d: DecidablePaths A
x, y: B
ne: f^-1 x <> f^-1 y
p: x = y
Empty apply ne, ap, p.
Defined.

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).
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: P -> B
WeaklyConstant (g o f)
Proof.
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: P -> B
WeaklyConstant (g o f)
  intros x y; apply (ap g), path_ishprop.
Defined.

(** 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.
A: Type
H: Decidable A
Collapsible A
Proof.
A: Type
H: Decidable A
Collapsible A
  destruct (dec A) as [a | na].
A: Type
H: Decidable A
a: A
Collapsible A
A: Type
H: Decidable A
na: ~ A
Collapsible A
  -
A: Type
H: Decidable A
a: A
Collapsible A exists (const a).
A: Type
H: Decidable A
a: A
WeaklyConstant (const a)
    intros x y; reflexivity.
  -
A: Type
H: Decidable A
na: ~ A
Collapsible A exists idmap.
A: Type
H: Decidable A
na: ~ A
WeaklyConstant idmap
    intros x y; destruct (na x).
Defined.

Global Instance pathcoll_decpaths (A : Type) `{DecidablePaths A}
: PathCollapsible A.
A: Type
H: DecidablePaths A
PathCollapsible A
Proof.
A: Type
H: DecidablePaths A
PathCollapsible A
  intros x y; exact _.
Defined.

(** 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.
A: Type
H: PathCollapsible A
IsHSet A
Proof.
A: Type
H: PathCollapsible A
IsHSet A
  apply istrunc_S.
A: Type
H: PathCollapsible A
is_mere_relation A paths
  intros x y.
A: Type
H: PathCollapsible A
x, y: A
IsHProp (x = y)
  assert (h : forall p:x=y, p = (collapse (idpath x))^ @ collapse p).
A: Type
H: PathCollapsible A
x, y: A
forall p : x = y, p = (collapse 1)^ @ collapse p
A: Type
H: PathCollapsible A
x, y: A
h: forall p : x = y, p = (collapse 1)^ @ collapse p
IsHProp (x = y)
  {
A: Type
H: PathCollapsible A
x, y: A
forall p : x = y, p = (collapse 1)^ @ collapse p intros []; symmetry; by apply concat_Vp. }
A: Type
H: PathCollapsible A
x, y: A
h: forall p : x = y, p = (collapse 1)^ @ collapse p
IsHProp (x = y)
  apply hprop_allpath; intros p q.
A: Type
H: PathCollapsible A
x, y: A
h: forall p : x = y, p = (collapse 1)^ @ collapse p
p, q: x = y
p = q
  refine (h p @ _ @ (h q)^).
A: Type
H: PathCollapsible A
x, y: A
h: forall p : x = y, p = (collapse 1)^ @ collapse p
p, q: x = y
(collapse 1)^ @ collapse p =
(collapse 1)^ @ collapse q
  apply whiskerL.
A: Type
H: PathCollapsible A
x, y: A
h: forall p : x = y, p = (collapse 1)^ @ collapse p
p, q: x = y
collapse p = collapse q
  apply wconst.
Defined.

Definition collapsible_hprop (A : Type) `{IsHProp A}
: Collapsible A.
A: Type
IsHProp0: IsHProp A
Collapsible A
Proof.
A: Type
IsHProp0: IsHProp A
Collapsible A
  exists idmap.
A: Type
IsHProp0: IsHProp A
WeaklyConstant idmap
  intros x y; apply path_ishprop.
Defined.

Definition pathcoll_hset (A : Type) `{IsHSet A}
: PathCollapsible A.
A: Type
IsHSet0: IsHSet A
PathCollapsible A
Proof.
A: Type
IsHSet0: IsHSet A
PathCollapsible A
  intros x y; apply collapsible_hprop; exact _.
Defined.

Corollary hset_decpaths (A : Type) `{DecidablePaths A}
: IsHSet A.
A: Type
H: DecidablePaths A
IsHSet A
Proof.
A: Type
H: DecidablePaths A
IsHSet A
  exact _.
Defined.

(** ** 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).
H: Funext
A: Type
IsHProp (DecidablePaths A)
Proof.
H: Funext
A: Type
IsHProp (DecidablePaths A)
  apply hprop_inhabited_contr; intros d.
H: Funext
A: Type
d: DecidablePaths A
Contr (DecidablePaths A)
  assert (IsHSet A) by exact _.
H: Funext
A: Type
d: DecidablePaths A
X: IsHSet A
Contr (DecidablePaths A)
  apply (Build_Contr _ d).
H: Funext
A: Type
d: DecidablePaths A
X: IsHSet A
forall y : DecidablePaths A, d = y
  intros d'.
H: Funext
A: Type
d: DecidablePaths A
X: IsHSet A
d': DecidablePaths A
d = d'
  apply path_forall; intros x; apply path_forall; intros y.
H: Funext
A: Type
d: DecidablePaths A
X: IsHSet A
d': DecidablePaths A
x, y: A
d x y = d' x y
  generalize (d x y); clear d; intros d.
H: Funext
A: Type
X: IsHSet A
d': DecidablePaths A
x, y: A
d: Decidable (x = y)
d = d' x y
  generalize (d' x y); clear d'; intros d'.
H: Funext
A: Type
X: IsHSet A
x, y: A
d, d': Decidable (x = y)
d = d'
  destruct d as [d|nd]; destruct d' as [d'|nd'].
H: Funext
A: Type
X: IsHSet A
x, y: A
d, d': x = y
inl d = inl d'
H: Funext
A: Type
X: IsHSet A
x, y: A
d: x = y
nd': x <> y
inl d = inr nd'
H: Funext
A: Type
X: IsHSet A
x, y: A
nd: x <> y
d': x = y
inr nd = inl d'
H: Funext
A: Type
X: IsHSet A
x, y: A
nd, nd': x <> y
inr nd = inr nd'
  -
H: Funext
A: Type
X: IsHSet A
x, y: A
d, d': x = y
inl d = inl d' apply ap, path_ishprop.
  -
H: Funext
A: Type
X: IsHSet A
x, y: A
d: x = y
nd': x <> y
inl d = inr nd' elim (nd' d).
  -
H: Funext
A: Type
X: IsHSet A
x, y: A
nd: x <> y
d': x = y
inr nd = inl d' elim (nd d').
  -
H: Funext
A: Type
X: IsHSet A
x, y: A
nd, nd': x <> y
inr nd = inr nd' apply ap, path_forall; intros p; elim (nd p).
Defined.