Library Maplists

Require Import BinNat.
Require Import Ndigits.
Require Import Ndec.
Require Import Map.
Require Import Fset.
Require Import Mapaxioms.
Require Import Mapsubset.
Require Import Mapcard.
Require Import Mapcanon.
Require Import Mapc.
Require Import Bool.
Require Import Sumbool.
Require Import List.
Require Import Arith.
Require Import Mapiter.
Require Import Mapfold.

Section MapLists.

  Fixpoint ad_in_list (a:ad) (l:list ad) {struct l} : bool :=
    match l with
    | nil => false
    | a' :: l' => orb (Neqb a a') (ad_in_list a l')
    end.

  Fixpoint ad_list_stutters (l:list ad) : bool :=
    match l with
    | nil => false
    | a :: l' => orb (ad_in_list a l') (ad_list_stutters l')
    end.

  Lemma ad_in_list_forms_circuit :
   forall (x:ad) (l:list ad),
     ad_in_list x l = true ->
     {l1 : list ad & {l2 : list ad | l = l1 ++ x :: l2}}.

  Lemma ad_list_stutters_has_circuit :
   forall l:list ad,
     ad_list_stutters l = true ->
     {x : ad &
     {l0 : list ad &
     {l1 : list ad & {l2 : list ad | l = l0 ++ x :: l1 ++ x :: l2}}}}.

  Fixpoint Elems (l:list ad) : FSet :=
    match l with
    | nil => M0 unit
    | a :: l' => MapPut _ (Elems l') a tt
    end.

  Lemma Elems_canon : forall l:list ad, mapcanon _ (Elems l).

  Lemma Elems_app :
   forall l l':list ad, Elems (l ++ l') = FSetUnion (Elems l) (Elems l').

  Lemma Elems_rev : forall l:list ad, Elems (rev l) = Elems l.

  Lemma ad_in_elems_in_list :
   forall (l:list ad) (a:ad), in_FSet a (Elems l) = ad_in_list a l.

  Lemma ad_list_not_stutters_card :
   forall l:list ad,
     ad_list_stutters l = false -> length l = MapCard _ (Elems l).

  Lemma ad_list_card : forall l:list ad, MapCard _ (Elems l) <= length l.

  Lemma ad_list_stutters_card :
   forall l:list ad,
     ad_list_stutters l = true -> MapCard _ (Elems l) < length l.

  Lemma ad_list_not_stutters_card_conv :
   forall l:list ad,
     length l = MapCard _ (Elems l) -> ad_list_stutters l = false.

  Lemma ad_list_stutters_card_conv :
   forall l:list ad,
     MapCard _ (Elems l) < length l -> ad_list_stutters l = true.

  Lemma ad_in_list_l :
   forall (l l':list ad) (a:ad),
     ad_in_list a l = true -> ad_in_list a (l ++ l') = true.

  Lemma ad_list_stutters_app_l :
   forall l l':list ad,
     ad_list_stutters l = true -> ad_list_stutters (l ++ l') = true.

  Lemma ad_in_list_r :
   forall (l l':list ad) (a:ad),
     ad_in_list a l' = true -> ad_in_list a (l ++ l') = true.

  Lemma ad_list_stutters_app_r :
   forall l l':list ad,
     ad_list_stutters l' = true -> ad_list_stutters (l ++ l') = true.

  Lemma ad_list_stutters_app_conv_l :
   forall l l':list ad,
     ad_list_stutters (l ++ l') = false -> ad_list_stutters l = false.

  Lemma ad_list_stutters_app_conv_r :
   forall l l':list ad,
     ad_list_stutters (l ++ l') = false -> ad_list_stutters l' = false.

  Lemma ad_in_list_app_1 :
   forall (l l':list ad) (x:ad), ad_in_list x (l ++ x :: l') = true.

  Lemma ad_in_list_app :
   forall (l l':list ad) (x:ad),
     ad_in_list x (l ++ l') = orb (ad_in_list x l) (ad_in_list x l').

  Lemma ad_in_list_rev :
   forall (l:list ad) (x:ad), ad_in_list x (rev l) = ad_in_list x l.

  Lemma ad_list_has_circuit_stutters :
   forall (l0 l1 l2:list ad) (x:ad),
     ad_list_stutters (l0 ++ x :: l1 ++ x :: l2) = true.

  Lemma ad_list_stutters_prev_l :
   forall (l l':list ad) (x:ad),
     ad_in_list x l = true -> ad_list_stutters (l ++ x :: l') = true.

  Lemma ad_list_stutters_prev_conv_l :
   forall (l l':list ad) (x:ad),
     ad_list_stutters (l ++ x :: l') = false -> ad_in_list x l = false.

  Lemma ad_list_stutters_prev_r :
   forall (l l':list ad) (x:ad),
     ad_in_list x l' = true -> ad_list_stutters (l ++ x :: l') = true.

  Lemma ad_list_stutters_prev_conv_r :
   forall (l l':list ad) (x:ad),
     ad_list_stutters (l ++ x :: l') = false -> ad_in_list x l' = false.

  Lemma ad_list_Elems :
   forall l l':list ad,
     MapCard _ (Elems l) = MapCard _ (Elems l') ->
     length l = length l' -> ad_list_stutters l = ad_list_stutters l'.

  Lemma ad_list_app_length :
   forall l l':list ad, length (l ++ l') = length l + length l'.

  Lemma ad_list_stutters_permute :
   forall l l':list ad,
     ad_list_stutters (l ++ l') = ad_list_stutters (l' ++ l).

  Lemma ad_list_rev_length : forall l:list ad, length (rev l) = length l.

  Lemma ad_list_stutters_rev :
   forall l:list ad, ad_list_stutters (rev l) = ad_list_stutters l.

  Lemma ad_list_app_rev :
   forall (l l':list ad) (x:ad), rev l ++ x :: l' = rev (x :: l) ++ l'.

  Section ListOfDomDef.

  Variable A : Type.

  Definition ad_list_of_dom :=
    MapFold A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil).

  Lemma ad_in_list_of_dom_in_dom :
   forall (m:Map A) (a:ad), ad_in_list a (ad_list_of_dom m) = in_dom A a m.

  Lemma Elems_of_list_of_dom :
   forall m:Map A, eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m).

  Lemma Elems_of_list_of_dom_c :
   forall m:Map A, mapcanon A m -> Elems (ad_list_of_dom m) = MapDom A m.

  Lemma ad_list_of_dom_card_1 :
   forall (m:Map A) (pf:ad -> ad),
     length
       (MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil)
          pf m) = MapCard A m.

  Lemma ad_list_of_dom_card :
   forall m:Map A, length (ad_list_of_dom m) = MapCard A m.

  Lemma ad_list_of_dom_not_stutters :
   forall m:Map A, ad_list_stutters (ad_list_of_dom m) = false.

  End ListOfDomDef.

  Lemma ad_list_of_dom_Dom_1 :
   forall (A:Type) (m:Map A) (pf:ad -> ad),
     MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) pf
       m =
     MapFold1 unit (list ad) nil (app (A:=ad))
       (fun (a:ad) (_:unit) => a :: nil) pf (MapDom A m).

  Lemma ad_list_of_dom_Dom :
   forall (A:Type) (m:Map A),
     ad_list_of_dom A m = ad_list_of_dom unit (MapDom A m).

End MapLists.