Require Export Definitions.

Module Symbols.

  Import Base Lists Definitions.

  Section DomainAndRange.

    Context {Tt Vt: Type}.

    Fixpoint dom (G : @grammar Tt Vt) : list (@symbol Tt Vt):=
      match G with
        |[] ⇒ []
        |R A u :: Gr ⇒ (Vs A) :: dom Gr
      end.

    Fixpoint ran G: list (@phrase Tt Vt) :=
      match G with
          [] ⇒ []
        | R A u :: Gr ⇒ u :: ran Gr
      end.

    Lemma rule_domG G A u :
      R A u el G → Vs A el dom G.

    Lemma domG_rule G s :
      s el (dom G) → ∃ A u, s = Vs A ∧ R A u el G.

    Lemma dom_subset G G' :
      G <<= G' → dom G <<= dom G'.

    Lemma rule_ranG G A u :
      R A u el G → u el ran G.

    Lemma ranG_rule G u :
      u el ran G → ∃ A, R A u el G.

  End DomainAndRange.

  Section Symbols.

    Context {Tt Vt: Type}.

    Fixpoint symbs G: list (@symbol Tt Vt) :=
      match G with
          [] ⇒ []
        | R A u :: Gr ⇒ Vs A :: u ++ symbs Gr
      end.

    Lemma symbs_dom G s :
      s el dom G → s el symbs G.

    Lemma symbs_inv G s :
      s el symbs G ↔ ∃ A u, R A u el G ∧ (s = (Vs A) ∨ s el u).

    Lemma symbs_subset G G' s :
      G <<= G' → s el symbs G → s el symbs G'.

  End Symbols.

  Section FreshVariables.

    Context {Tt Vt: Type}.

    Context {TtToNat: Tt → nat}.
    Context {VtToNat: Vt → nat}.
    Context {NatToTt: nat → Tt }.
    Context {NatToVt: nat → Vt}.

    Hypothesis Id1: ∀ x, TtToNat (NatToTt x) = x.
    Hypothesis Id2: ∀ x, NatToTt (TtToNat x) = x.
    Hypothesis Id3: ∀ x, VtToNat (NatToVt x) = x.
    Hypothesis Id4: ∀ x, NatToVt (VtToNat x) = x.

    Definition getNat s :=
      match s with
          Vs (V i) ⇒ VtToNat i
        | Ts (T i) ⇒ TtToNat i
      end.

    Definition sless n s := getNat s ≤ n.
    Definition sless' s s' := getNat s < getNat s'.

    Instance sless_dec n s : dec (sless n s).

    Lemma sless_monotone m n s :
      m ≤ n → sless m s → sless n s.

    Fixpoint maxSymbRule (sl : list symbol) :=
      match sl with
        | [] ⇒ 0
        | s :: u ⇒ let
            n := maxSymbRule u
          in if decision (sless n s) then n else getNat s
      end.

    Fixpoint maxSymb (G : grammar) n :=
      match G with
        | [] ⇒ n
        | R A u :: Gr ⇒ let
            (m0, m1) := (maxSymbRule (Vs A :: u), maxSymb Gr n)
          in if decision (m0 < m1) then m1 else m0
      end.

    Lemma maxSymbRule_corr u s :
      s el u → sless (maxSymbRule u) s.

    Lemma maxSymb_corr G s n :
      s el symbs G → sless (maxSymb G n) s.

    Definition fresh G s := ∀ s', s' el symbs G → sless' s' s.

    Lemma pickFresh G :
      { A | fresh G (Vs A) }.

    Lemma fresh_symbs G s :
      fresh G s → ¬ s el symbs G.

  End FreshVariables.

End Symbols.