Library Decide

Copyright (c) 2018 by Swirlds, Inc. Implemented by Karl Crary.

Require Import Bool.
Require Import List.
Require Export Decidable.

Require Import Tact.
Require Import Relation.

Definition incl {T : Type} (P Q : T -> Prop) :=
  forall x, P x -> Q x.

Kuratowski finite, I think.
Definition finite {T : Type} (P : T -> Prop) : Prop
  :=
  exists l, forall x, P x <-> In x l.

Lemma Is_true_decide :
  forall b, decidable (Is_true b).

Lemma dec_In :
  forall (T : Type) (x : T) (l : list T),
    (forall (x y : T), decidable (x = y))
    -> decidable (In x l).
nil
Lemma dec_and_dep :
  forall P Q,
    decidable P
    -> (P -> decidable Q)
    -> decidable (P /\ Q).

Lemma dec_equiv :
  forall (P Q : Prop),
    (P <-> Q)
    -> decidable P
    -> decidable Q.

Lemma finite_decide :
  forall (T : Type) (P : T -> Prop),
    (forall (x y : T), decidable (x = y))
    -> finite P
    -> forall x, decidable (P x).

Lemma dec_exists_finite :
  forall (T : Type) (P Q : T -> Prop),
    incl P Q
    -> finite Q
    -> (forall x, decidable (P x))
    -> decidable (exists x, P x).
nil
Lemma dec_forall_imp_finite :
  forall (T : Type) (P Q : T -> Prop),
    finite P
    -> (forall x, P x -> decidable (Q x))
    -> decidable (forall x, P x -> Q x).
nil
Lemma finite_equiv :
  forall (T : Type) (P Q : T -> Prop),
    (forall x, P x <-> Q x)
    -> finite P
    -> finite Q.

Lemma filter_to_finite :
  forall T (P : T -> Prop) l,
    (forall x, decidable (P x))
    -> (forall x, P x -> In x l)
    -> finite P.
nil
Lemma finite_subset :
  forall T (P Q : T -> Prop),
    incl P Q
    -> (forall x, decidable (P x))
    -> finite Q
    -> finite P.

Lemma finite_subset' :
  forall T (P Q : T -> Prop),
    (forall (x y : T), decidable (x = y))
    -> incl P Q
    -> (forall x, Q x -> decidable (P x))
    -> finite Q
    -> finite P.

Lemma finite_plus :
  forall (T : Type) (R : T -> T -> Prop) x,
    well_founded R
    -> (forall x y, decidable (R x y))
    -> (forall x, finite (fun y => R y x))
    -> finite (fun y => plus R y x).
nil
Lemma finite_star :
  forall (T : Type) (R : T -> T -> Prop) x,
    well_founded R
    -> (forall x y, decidable (R x y))
    -> (forall x, finite (fun y => R y x))
    -> finite (fun y => star R y x).

Lemma finite_exists :
  forall (S T : Type) (P : S -> Prop) (Q : S -> T -> Prop),
    finite P
    -> (forall x, P x -> finite (Q x))
    -> finite (fun y => exists x, P x /\ Q x y).
nil