Require Import
  Basics.Overture
  Basics.PathGroupoids
  Basics.Trunc
  Basics.Tactics
  Basics.Iff.
[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 :=
  multimatch goal with
  | [|- ?A] => decide_type A
  | [|- ~ ?A] => decide_type A
  end.

Definition decidable_true {A : Type}
  (a : A)
  (P : forall (p : Decidable A), Type)
  (p : forall x, P (inl x))
  : forall p, P p.
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
forall p : Decidable A, P p
Proof.
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
forall p : Decidable A, P p
  intros [x|n].
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
x: A
P (inl x)
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
n: ~ A
P (inr n)
  -
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
x: A
P (inl x) apply p.
  -
A: Type
a: A
P: Decidable A -> Type
p: forall x : A, P (inl x)
n: ~ A
P (inr n) contradiction n.
Defined.

(** Replace a term [p] of the form [Decidable A] with [inl x] if we have a term [a : A] showing that [A] is true. *)
Ltac decidable_true p a :=
  generalize p;
  rapply (decidable_true a);
  try intro.

Definition decidable_false {A : Type}
  (n : not A)
  (P : forall (p : Decidable A), Type)
  (p : forall n', P (inr n'))
  : forall p, P p.
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
forall p : Decidable A, P p
Proof.
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
forall p : Decidable A, P p
  intros [x|n'].
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
x: A
P (inl x)
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
n': ~ A
P (inr n')
  -
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
x: A
P (inl x) contradiction n.
  -
A: Type
n: ~ A
P: Decidable A -> Type
p: forall n' : ~ A, P (inr n')
n': ~ A
P (inr n') apply p.
Defined.

(** Replace a term [p] of the form [Decidable A] with [inr na] if we have a term [n : not A] showing that [A] is false. *)
Ltac decidable_false p n :=
  generalize p;
  rapply (decidable_false n);
  try intro.

Class DecidablePaths (A : Type) :=
  dec_paths :: forall (x y : A), Decidable (x = y).

Class Stable P := stable : ~~P -> P.

(** We always have a map in the other direction. *)
Definition not_not_unit {P : Type} : P -> ~~P
  := fun x np => np x.

Instance ishprop_stable_hprop `{Funext} P `{IsHProp P} : IsHProp (Stable P)
  := istrunc_forall.

Instance stable_decidable P `{Decidable P} : Stable P.
P: Type
H: Decidable P
Stable P
Proof.
P: Type
H: Decidable P
Stable P
  intros dn.
P: Type
H: Decidable P
dn: ~~ P
P
  (* [dec P] either solves the goal or contradicts [dn]. *)
  by destruct (dec P).
Defined.

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 (not_not_unit p)).
Defined.

Definition iff_stable P `(Stable P) : ~~P <-> P.
P: Type
H: Stable P
~~ P <-> P
Proof.
P: Type
H: Stable P
~~ P <-> P
  split.
P: Type
H: Stable P
~~ P -> P
P: Type
H: Stable P
P -> ~~ P
  -
P: Type
H: Stable P
~~ P -> P exact stable.
  -
P: Type
H: Stable P
P -> ~~ P exact not_not_unit.
Defined.

Definition stable_iff {A B} (f : A <-> B)
  : Stable A -> Stable B.
A, B: Type
f: A <-> B
Stable A -> Stable B
Proof.
A, B: Type
f: A <-> B
Stable A -> Stable B
  intros stableA nnb.
A, B: Type
f: A <-> B
stableA: Stable A
nnb: ~~ B
B
  destruct f as [f finv].
A, B: Type
f: A -> B
finv: B -> A
stableA: Stable A
nnb: ~~ B
B
  exact (f (stableA (fun na => nnb (fun b => na (finv b))))).
Defined.

Definition stable_equiv' {A B} (f : A <~> B)
  : Stable A -> Stable B
  := stable_iff f.

Definition stable_equiv {A B} (f : A -> B) `{!IsEquiv f}
  : Stable A -> Stable B
  := stable_equiv' (Build_Equiv _ _ f _).

(**
  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. *)

Instance decidable_contr X `{Contr X} : Decidable X
  := inl (center X).

(** Thus, hprops have decidable equality. *)

Instance decidablepaths_hprop X `{IsHProp X} : DecidablePaths X
  := fun x y => dec (x = y).

(** Empty types are trivial. *)

Instance decidable_empty : Decidable Empty
  := inr idmap.


(** ** Transfer along equivalences *)

Definition decidable_iff {A B} (f : A <-> B)
  : Decidable A -> Decidable B.
A, B: Type
f: A <-> B
Decidable A -> Decidable B
Proof.
A, B: Type
f: A <-> B
Decidable A -> Decidable B
  intros [a|na].
A, B: Type
f: A <-> B
a: A
Decidable B
A, B: Type
f: A <-> B
na: ~ A
Decidable B
  -
A, B: Type
f: A <-> B
a: A
Decidable B exact (inl (fst f a)).
  -
A, B: Type
f: A <-> B
na: ~ A
Decidable B exact (inr (fun b => na (snd f b))).
Defined.

Definition decidable_equiv' (A : Type) {B : Type} (f : A <~> B)
: Decidable A -> Decidable B
  := decidable_iff f.

Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{!IsEquiv f}
: Decidable A -> Decidable B
  := decidable_equiv' _ (Build_Equiv _ _ 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
  }.

Class PathCollapsible (A : Type) :=
  path_coll :: forall (x y : A), Collapsible (x = y).

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.

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]. *)
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.

(** Hedberg's Theorem *)
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.

(** We can use Hedberg's Theorem to simplify a goal of the form [forall (d : Decidable (x = x :> A)), P d] when [A] has decidable paths. *)
Definition decidable_paths_refl (A : Type) `{DecidablePaths A}
  (x : A)
  (P : forall (d : Decidable (x = x)), Type)
  (Px : P (inl idpath))
  : forall d, P d.
A: Type
H: DecidablePaths A
x: A
P: Decidable (x = x) -> Type
Px: P (inl 1)
forall d : Decidable (x = x), P d
Proof.
A: Type
H: DecidablePaths A
x: A
P: Decidable (x = x) -> Type
Px: P (inl 1)
forall d : Decidable (x = x), P d
  rapply (decidable_true idpath).
A: Type
H: DecidablePaths A
x: A
P: Decidable (x = x) -> Type
Px: P (inl 1)
forall x0 : x = x, P (inl x0)
  intro p.
A: Type
H: DecidablePaths A
x: A
P: Decidable (x = x) -> Type
Px: P (inl 1)
p: x = x
P (inl p)
  (** We cannot eliminate [p : x = x] with path induction, but we can use Hedberg's theorem to replace this with [idpath]. *)
  assert (r : (idpath = p)) by apply path_ishprop.
A: Type
H: DecidablePaths A
x: A
P: Decidable (x = x) -> Type
Px: P (inl 1)
p: x = x
r: 1 = p
P (inl p)
  by destruct r.
Defined.

(** ** Truncation *)

(** Having decidable equality (which implies being an hset, by Hedberg's theorem above) is itself an hprop. *)

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'
  funext x 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.

(** ** Logical Laws *)

(** Various logical laws don't hold constructively as they do classically due to a required use of excluded middle. For us, this means that some laws require further assumptions on the decidability of propositions. *)

(** Here we give the dual De Morgan's Law which complements the one given in Iff.v.  One direction requires that one of the two propositions be decidable, while the other direction needs no assumption.  We state the latter property first, to avoid duplication in the proof. *)
Definition not_prod_sum_not A B : ~ A + ~ B -> ~ (A * B).
A, B: Type
~ A + ~ B -> ~ (A * B)
Proof.
A, B: Type
~ A + ~ B -> ~ (A * B)
  intros [na|nb] [a b].
A, B: Type
na: ~ A
a: A
b: B
Empty
A, B: Type
nb: ~ B
a: A
b: B
Empty
  -
A, B: Type
na: ~ A
a: A
b: B
Empty exact (na a).
  -
A, B: Type
nb: ~ B
a: A
b: B
Empty exact (nb b).
Defined.

Definition iff_not_prod A B `{Decidable A}
  : ~ (A * B) <-> ~ A + ~ B.
A, B: Type
H: Decidable A
~ (A * B) <-> ~ A + ~ B
Proof.
A, B: Type
H: Decidable A
~ (A * B) <-> ~ A + ~ B
  split.
A, B: Type
H: Decidable A
~ (A * B) -> ~ A + ~ B
A, B: Type
H: Decidable A
~ A + ~ B -> ~ (A * B)
  -
A, B: Type
H: Decidable A
~ (A * B) -> ~ A + ~ B intros np.
A, B: Type
H: Decidable A
np: ~ (A * B)
~ A + ~ B
    destruct (dec A) as [a|na].
A, B: Type
H: Decidable A
np: ~ (A * B)
a: A
~ A + ~ B
A, B: Type
H: Decidable A
np: ~ (A * B)
na: ~ A
~ A + ~ B
    +
A, B: Type
H: Decidable A
np: ~ (A * B)
a: A
~ A + ~ B exact (inr (fun b => np (a, b))).
    +
A, B: Type
H: Decidable A
np: ~ (A * B)
na: ~ A
~ A + ~ B exact (inl na).
  -
A, B: Type
H: Decidable A
~ A + ~ B -> ~ (A * B) apply not_prod_sum_not.
Defined.

Definition iff_not_prod' A B `{Decidable B}
  : ~ (A * B) <-> ~ A + ~ B.
A, B: Type
H: Decidable B
~ (A * B) <-> ~ A + ~ B
Proof.
A, B: Type
H: Decidable B
~ (A * B) <-> ~ A + ~ B
  split.
A, B: Type
H: Decidable B
~ (A * B) -> ~ A + ~ B
A, B: Type
H: Decidable B
~ A + ~ B -> ~ (A * B)
  -
A, B: Type
H: Decidable B
~ (A * B) -> ~ A + ~ B intros np.
A, B: Type
H: Decidable B
np: ~ (A * B)
~ A + ~ B
    destruct (dec B) as [b|nb].
A, B: Type
H: Decidable B
np: ~ (A * B)
b: B
~ A + ~ B
A, B: Type
H: Decidable B
np: ~ (A * B)
nb: ~ B
~ A + ~ B
    +
A, B: Type
H: Decidable B
np: ~ (A * B)
b: B
~ A + ~ B exact (inl (fun a => np (a, b))).
    +
A, B: Type
H: Decidable B
np: ~ (A * B)
nb: ~ B
~ A + ~ B exact (inr nb).
  -
A, B: Type
H: Decidable B
~ A + ~ B -> ~ (A * B) apply not_prod_sum_not.
Defined.