Library Decidable

Require Export Unicode.Utf8_core.
Require Import Bool List Le String Showable HoTT.

The Decidable Class

This code is mostly imported from https://github.com/HoTT/HoTT. We are defining it here to be independent of the Coq/HoTT library.

We can not use the Decidable class of Coq because its definition is in Prop (using ∨) instead of Type (using +). All the predicates defined in this file are proof-relevant.

Decidability

Class Decidable (A : Type) := dec : A + (not A ).

A DecidableProp A is, essentially, isomorphic to Bool: it is either true or false.

Class DecidableProp (A : Type) := {
    dec_p :> Decidable A;
    is_hprop_p :> IsHProp A }.

Instance DecidableProp_Decidable_HProp (A : Type) {Hdec: Decidable A}
         {Hprop:IsHProp A} : DecidableProp A :=
  {|dec_p := Hdec ; is_hprop_p := Hprop |}.

The canonical example of a DecidableProp is the decidable equality for a type A, as per Hedberg theorem. We package it in a dedicated class.

Class DecidablePaths (A : Type) := {
dec_paths : ∀ a b : A, Decidable (a = b)
}.

Hedberg theorem is a standard theorem of HoTT: it states that if a type A has decidable equality, then it is a hSet, i.e. its equality is proof-irrelevant. See the proof at https://github.com/HoTT in HoTT/theories/Basics/Decidable.v

Instance Hedberg (A : Type) `{DecidablePaths A} : IsHSet A.

Instance DecidablePaths_DecidableProp A
(DecidablePaths_A : DecidablePaths A)
: ∀ (a b : A), DecidableProp (a = b).
Defined.

Checkability

Class Checkable (A : Type) :=
  {
    checkP : Type;
    checkP_dec : Decidable checkP ;
    convert : checkP → A
  }.

Class CheckableProp (A : Type) := {
    check :> Checkable A;
    is_hprop_c :> IsHProp A }.

Instance checkable_decidable (A : Type) {H:Checkable A} : Decidable (@checkP _ H)
  := checkP_dec.

Instance decidable_is_checkable (A : Type) {H:Decidable A} : Checkable A
  := {| checkP := A ; checkP_dec := H ; convert := id |}.

Instance decidablep_is_checkableprop (A : Type) {H:DecidableProp A} : CheckableProp A
  := {| is_hprop_c := _ |}.

A few instances

Set Implicit Arguments.

Reflecting a boolean as a decidable property

Instance Decidable_bool (t : bool) : Decidable (Is_true t) :=
  match t with
    | true ⇒ inl tt
    | false ⇒ inr id
  end.

Instances for bool

Instance Decidable_eq_bool : ∀ (x y : bool), Decidable (eq x y).
Defined.

Instance DecidablePaths_bool : DecidablePaths bool :=
{ dec_paths := Decidable_eq_bool }.

Instances for nat

Instance Decidable_eq_nat : ∀ (x y : nat), Decidable (eq x y).
Defined.

Instance DecidablePaths_nat : DecidablePaths nat :=
{ dec_paths := Decidable_eq_nat }.

Instances for list

Instance Decidable_eq_list : ∀ A (HA: DecidablePaths A)
(x y: list A), Decidable (eq x y).
Defined.

Instance for decidable equality on list

Instance DecidablePaths_list :
∀ A (HA: DecidablePaths A), DecidablePaths (list A) :=
{ dec_paths := Decidable_eq_list HA }.

Instance for less than

Instance Decidable_le_nat : ∀ (x y : nat), Decidable (x ≤ y).
Defined.

Instances for option

Instance Decidable_eq_option : ∀ A (HA: DecidablePaths A)
  (x y: option A), Decidable (eq x y).
Defined.

Instance DecidablePaths_option :
  ∀ A (HA: DecidablePaths A), DecidablePaths (option A) :=
    { dec_paths := Decidable_eq_option HA }.

Instances for logical connectives

Instance Decidable_and P Q (HP : Decidable P)
(HQ : Decidable Q) : Decidable (P × Q).
Defined.

Instance Decidable_or P Q (HP : Decidable P)
        (HQ : Decidable Q) : Decidable (P + Q).
Defined.

Instance Decidable_not P (HP : Decidable P) :
  Decidable (not P).
Defined.

Instance Decidable_implies P Q (HP : Decidable P)
  (HQ : Decidable Q) : Decidable (P → Q).
Defined.

Instance Decidable_True : Decidable True := inl I.

Instance Decidable_False : Decidable False.
Defined.

Instance DecidablePaths_unit : DecidablePaths unit.
Defined.

Decidability of proven properties

Instance Decidable_proven (P : Type) (ev : P): Decidable P :=
  inl ev.

Instance DecidablePaths_prod A B `{DecidablePaths A} `{DecidablePaths B}:
  DecidablePaths (A ×B).
Defined.

Instance DecidablePaths_fun A B A'
         (H : ∀ a, DecidablePaths (B a)) (f : A' → A)
  a' : DecidablePaths (B (f a')) .