Qcert.Basic.Data.RDomain

Section RDomain.



  Definition domains_included (ats1 ats2:list string):=
    Forall (fun x ⇒ In x ats2) ats1.

  Definition domains_included_alt (ats1 ats2:list string):=
    ∀ x, In x ats1 → In x ats2.

  Lemma domains_included_eq (ats1 ats2:list string) :
    domains_included ats1 ats2 ↔ domains_included_alt ats1 ats2.

  Definition domains_intersect (ats1 ats2 iats:list string):=
    ∀ x, In x iats → (In x ats1 ∧ In x ats2).

  Fixpoint domains_intersection (ats1 ats2:list string) : list string :=
    match ats1 with
      | nil ⇒ nil
      | a :: ats1' ⇒
        if (existsb (fun x ⇒ if string_dec x a then true else false) ats2)
        then a :: (domains_intersection ats1' ats2)
        else (domains_intersection ats1' ats2)
    end.

  Definition domains_disjoint (ats1 ats2:list string) :=
    domains_intersection ats1 ats2 = nil.

  Definition in_domain (ats1:list string) (x:string) :=
    In x ats1.

  Definition not_in_domain (ats1:list string) (x:string) :=
    In x ats1 → False.

  Lemma domains_intersection_nil_r (ats:list string) :
    domains_intersection ats nil = nil.

  Lemma not_so_in (x a:string) (l1 l2:list string) :
    x ≠ a → In x (domains_intersection l1 (a :: l2)) → In x (domains_intersection l1 l2).

  Lemma intersection_intersects (ats1 ats2:list string) :
    domains_intersect ats1 ats2 (domains_intersection ats1 ats2).

  Lemma self_domain (ats:list string) :
    domains_included ats ats.

  Lemma domains_included_nil_l l:
    domains_included nil l.

  Lemma domains_included_nil_r l:
    domains_included l nil → l = nil.

  Lemma domains_included_cons l1 l2 (a:string):
    domains_included (a::l1) l2 → domains_included l1 l2.

End RDomain.