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).
:=
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).
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).
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.
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).
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).
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