Qcert.Basic.Util.RCompat

Section RCompat.


  Context {A B:Type} `{EqDec A eq} `{EqDec B eq}.

  Definition compatible_with {A B:Type} `{EqDec A eq} `{EqDec B eq}
             (a:A) (b:B) (l₂:list (A × B)) : bool
    := match assoc_lookupr equiv_dec l₂ a with
       | Some d' ⇒ if equiv_dec b d' then true else false
       | None ⇒ true
       end.

  Definition compatible {A B:Type} `{EqDec A eq} `{EqDec B eq} (l₁ l₂:list (A × B)) : bool
    := forallb (fun xy ⇒ compatible_with (fst xy) (snd xy) l₂) l₁.

  Lemma compatible_nil_l (l:list (A × B)) : compatible nil l = true.

  Lemma compatible_nil_r (l:list (A × B)) : compatible l nil = true.

  Lemma compatible_with_cons_inv {x:A} {y:B} {a l} :
    compatible_with x y (a :: l) = true →
    compatible_with x y l = true.

  Lemma compatible_cons_inv_r {a} {l1 l2:list (A×B)} :
    compatible l1 (a::l2) = true → compatible l1 l2 = true.


  Lemma compatible_middle (l1 l2 l3:list (A × B)) a :
    compatible (l1 ++ a :: l2) l3 = compatible (a::l1++l2) l3.

  Lemma compatible_cons_r (l l':list (A × B)) a :
    NoDup (domain l) →
    compatible l l' = true →
    compatible_with (fst a) (snd a) l = true →
    compatible l (a :: l') = true.

  Lemma compatible_perm_proper_l (l1 l2 l3:list (A × B)) :
    Permutation l1 l2 →
    NoDup (domain l3) →
    compatible l1 l3 = true →
    compatible l2 l3 = true.

  Lemma compatible_refl (l:list (A × B)) :
    NoDup (domain l) → compatible l l = true.

  Lemma compatible_single_nin (b:list (A×B)) x d :
    ¬ In x (domain b) →
    compatible b ((x, d) :: nil) = true.

  Lemma compatible_true_sym (l1 l2:list (A×B)) :
    NoDup (domain l2) → compatible l1 l2 = true →
    compatible l2 l1 = true.

  Lemma compatible_false_sym (l1 l2:list (A×B)) :
    NoDup (domain l1) → compatible l1 l2 = false →
    compatible l2 l1 = false.

  Lemma compatible_sym (l1 l2:list (A×B)) :
    NoDup (domain l1) → NoDup (domain l2) →
    compatible l1 l2 = compatible l2 l1.

  Lemma same_domain_compatible (l₁ l₂:list (A×B)) :
    NoDup (domain l₁) →
    domain l₁ = domain l₂ →
    compatible l₁ l₂ = true →
    l₁ = l₂.

End RCompat.