RIS.aeq_facts: lemmas about α-equivalence and the equivalence transducer.

Set Implicit Arguments.

Require Export transducer subword.
Section s.
  Context {atom X: Set}{𝐀 : Atom atom} {𝐗 : Alphabet 𝐀 X}.

  Global Instance subword_filter (A : Set) (f : A → bool) :
    Proper (subword ==> subword) (filter f).

  Lemma subword_incl (A : Set) (u v : list A) : u ⊑ v → u ⊆ v.

  Global Instance subword_map (A B: Set) (f: A→B) :
    Proper (subword ==> subword) (map f).
  Global Instance subword_app (A: Set) :
    Proper (subword ==> subword ==> subword) (@app A).

  Lemma absent_subword s a b s' : s ⊑ s' → absent s' a b → absent s a b.

  Lemma subword_dec_app (A:Set) (u v w :list A) : u ⊑ v++w → ∃ u1 u2, u = u1++u2 ∧ u1 ⊑ v ∧ u2 ⊑ w.

  Lemma stack_binding_subword u v s1 s2 :
    (s1 ⊣ u | v ⤅ s2) →
    ∃ s3 s4, s2 = s3++s4 ∧ s4 ⊑ s1
             ∧ (∀ a, nb a (prj1 s4) = nb a (prj1 s1) - d_binding (𝗙 a u)
                     ∧ nb a (prj1 s3) = c_binding (𝗙 a u)
                     ∧ nb a (prj2 s4) = nb a (prj2 s1) - d_binding (𝗙 a v)
                     ∧ nb a (prj2 s3) = c_binding (𝗙 a v)
                     ∧ d_binding (𝗙 a u) - nb a (prj1 s1) = d_binding (𝗙 a v) - nb a (prj2 s1)).

  Lemma exists_var_binding u a n :
    𝗙 a u = (0,true,n) → ∃ u1 u2 x, u = u1++var x::u2 ∧ a #α u1 ∧ a ∈ ⌊x⌋.

  Lemma decompose_app (A:Set) (u1 u2 v : list A) :
    ⎢u1++u2⎥ = ⎢v⎥ → ∃ v1 v2, ⎢u1⎥ = ⎢v1⎥ ∧ v = v1++v2.
  Lemma scope_binding u a n :
    𝗙 a u = (0,false,S n) → ∃ u1 u2, u = u1++open a::u2 ∧ a #α u1 ∧ a ◁ u2.



  Lemma path_init_pair u v a b s :
    a ≠ b → ([(a,b)] ⊣ u | v ⤅ s) →
    (a ◁ u ∧ b ◁ v ∧ ∃ s', s = s'++[(a,b)])
    ∨ (∃ u1 u2 v1 v2,
          u = u1++close a::u2
          ∧ v = v1++close b::v2
          ∧ a ⋄ u1
          ∧ b ⋄ v1
          ∧ ⎢u1⎥ = ⎢v1⎥
          ∧ ∃ n, 𝗙 b u1 = (0,false,n)).

  Lemma path_init_refl_pair u v s c :
    ([(c,c)] ⊣ u | v ⤅ s) →
    [] ⊣ u | v ⤅ s ∨ (∃ s', s = s'++[(c,c)] ∧ [] ⊣ u | v ⤅ s').

  Lemma find_matching_close a u n :
    n < d_binding (𝗙 a u) → ∃ u1 u2, u = u1++close a::u2 ∧ d_binding (𝗙 a u1) = n ∧ a ▷ u1.

  Lemma subword_not_In (A:Set)(x:A) l m n : l ⊑(m++x::n) → ¬ x ∈ l → l ⊑ m++n.

  Lemma aeq_first_letter_open u v a b :
    a≠b → open a::u ≡ open b::v →
    ∃ u1 u2, u = u1++close a::u2
             ∧ a ⋄ u1
             ∧ ((b #α u1 ∧ [(a,b)]∙u1++close b::u2 ≡ v)
                ∨ ∃ w1 w2 w3 w4, u1 = w1 ++ open b::w2
                                 ∧ u2 = w3 ++ close b::w4
                                 ∧ b #α w1
                                 ∧ b ⋄ (w2++w3)
                                 ∧ ∀ c, c # u →
                                        [(a,b)]∙w1++open c::[(a,b);(b,c)]∙w2
                                               ++close b::[(b,c)]∙w3++close c::w4 ≡ v).

  Lemma aeq_first_letter u v l m :
    l::u ≡ m::v → (l=m ∧ u ≡ v) ∨ (∃ a b, a≠b ∧ l=open a ∧ m=open b).
End s.