PADEC - Coq Library

Library Padec.Tools.All_In

A Framework for Certified Self-Stabilization
PADEC Coq Library

Sep 2017

Global imports

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

Local imports

From Padec Require Import SetoidUtil.
From Padec Require Import ZUtils.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Count.

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.