Coq Library
Tools

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.

Local imports

Open Scope signature_scope.
Set Implicit Arguments.

Decidability Properties over a finite type stored into a list

Section All_In.

Context {A: Type} `{SA: Setoid A}.
Variable (all_A: list A)
(all_A_prop: forall a, InA equiv a all_A).

Lemma All_In_dec_forall_exists:
forall (P: A -> Prop) (P_compat: Proper fequiv P)
(P_dec: forall a, {P a} + {~P a}),
{forall a, ~P a} + {exists a, P a}.

Lemma All_In_dec_forall_notforall:
forall (P: A -> Prop) (P_dec: forall a, {P a} + {~P a}),
{Proper fequiv P -> forall a, P a} + {~(forall a, P a)}.

Lemma All_In_dec_forall_ex0:
forall (DA: Decider (equiv (A := A))) (l: list A),
forall (P: A -> Prop) (P_compat: Proper fequiv P)
(P_dec: forall a, {InA equiv a l -> P a} + {~P a}),
{a | InA equiv a l /\ P a} +
{forall a, InA equiv a l -> ~P a}.

Lemma All_In_dec_forall_ex:
forall (P: A -> Prop) (P_compat: Proper fequiv P)
(P_dec: forall a, {P a} + {~P a}),
{a | P a} + {forall a, ~P a}.

Lemma All_In_dec_forall_ex':
forall (P: A -> Prop) (P_compat: Proper fequiv P)
(P_dec: forall a, {P a} + {~P a}),
{a | ~ P a} + {forall a, P a}.

Emptiness Test Enum:

Proves emptyness test (i.e. the fact that a function always returns None) using the assumption that every element of type A is stored in a list (hence finite enumerable).
Lemma emptiness_by_enumeration:
forall B (eqB: relation B) (f: A -> option B),
{Proper (equiv ==> eqoptionA eqB) f ->
(equiv ==> eqoptionA eqB) f (fun _ => None)}
+
{~(equiv ==> eqoptionA eqB) f (fun _ => None)}.

as above, emptiness is decidable + when f is not None everywhere, we can pick some node n such that (f n) is not None.
Lemma emptiness_by_enumeration_bis:
forall B (eqB: relation B)
(f: A -> option B) (f_compat: Proper (equiv ==> eqoptionA eqB) f),
{ n | exists s, f n = Some s }
+
{(equiv ==> eqoptionA eqB) f (fun _ => None)}.

End All_In.

Section All_In_Count.

Context {A: Type} `{SA: Setoid A} {A_dec: Decider (equiv (A := A))}.
Variable (all_A: list A)
(all_A_prop: forall a, InA equiv a all_A).

Lemma All_In_exists_Card_T:
forall (P: A -> Prop) (P_compat: Proper pequiv P)
(P_dec: forall x, {P x}+{~ P x}),
{ NP | Count.Num_Card Count.Same { x | P x } NP}.

Lemma All_In_exists_Card:
forall (P: A -> Prop) (P_compat: Proper pequiv P)
(P_clas: forall x, P x \/ ~ P x),
exists NP, Count.Num_Card Count.Same { x | P x } NP.

End All_In_Count.

Section All_In_2.

Context {A: Type} `{SA: Setoid A}.
Context {B: Type} `{SB: Setoid B}.

Fixpoint build_A_ListB (a: A) (l: list B): list (A*B) :=
match l with
| nil => nil
| b :: lb => (a, b) :: (build_A_ListB a lb)
end.

Lemma all_build_A_ListB:
forall a lb b aa,
InA equiv b lb -> aa == a -> InA equiv (aa, b) (build_A_ListB a lb).

Fixpoint build_ListA_ListB (la: list A) (lb: list B): list (A*B) :=
match la with
| nil => nil
| a :: la => (build_A_ListB a lb) ++ (build_ListA_ListB la lb)
end.

Lemma all_build_ListA_ListB:
forall la lb a b,
InA equiv a la -> InA equiv b lb ->
InA equiv (a, b) (build_ListA_ListB la lb).

Variable (all_A: list A) (all_A_prop: forall a, InA equiv a all_A).
Variable (all_B: list B) (all_B_prop: forall a, InA equiv a all_B).
Definition all_AB: list (A*B) := build_ListA_ListB all_A all_B.

Lemma all_AB_prop: forall ab, InA equiv ab all_AB.

Lemma All_In_dec_forall_exists_2:
forall (P: A -> B -> Prop)
(P_compat: Proper fequiv P)
(P_dec: forall a b, {P a b} + {~P a b}),
{forall a b, ~P a b} + {exists a b, P a b}.

Lemma All_In_dec_forall_notforall_2:
forall (P: A -> B -> Prop)
(P_dec: forall a b, {P a b} + {~P a b}),
{Proper fequiv P -> forall a b, P a b} +
{~(forall a b, P a b)}.

End All_In_2.

Unset Implicit Arguments.
Close Scope signature_scope.