Require Export Derivation.

Module Inlining.

  Import Base Lists Definitions Derivation Symbols.

  Section Inlining.

    Context {Tt Vt: Type}.
    Context {Tt_eqdec: eq_dec Tt}.
    Context {Vt_eqdec: eq_dec Vt}.


    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 substG (G: @grammar Tt Vt) s u := map (fun r ⇒ match r with R B v ⇒ R B (substL v s u) end) G.

    Lemma substG_split G1 G2 s u :
      substG (G1 ++ G2) s u = substG G1 s u ++ substG G2 s u.

    Lemma substG_skipRule G A s u v :
      ¬ s el u → substG (R A u :: G) s v = R A u :: (substG G s v).

    Lemma substG_skip G s u :
      ¬ s el symbs G → substG G s u = G.

    Lemma substG_undo G B s :
      @fresh Tt Vt TtToNat VtToNat G (Vs B) → substG (substG G s [Vs B]) (Vs B) [s] = G.

    Hint Constructors derT.

    Lemma substL_der (G: @grammar Tt Vt) B u v :
      R B v el G → derT G u (substL u (Vs B) v).

    Lemma substG_inG G A s u v :
      R A u el G → R A (substL u s v) el (substG G s v).

    Lemma substG_dom G s u :
      dom (substG G s u) = dom G.

    Lemma in_substG_der G A B u v :
      R A u el (substG G (Vs B) v) → der (R B v :: G) A u.

    Hint Constructors der derL.
    Lemma der_substG_G G A B u v :
      der (substG G (Vs B) v) A u → der (R B v :: G) A u.

    Lemma der_G_substG' G A B u v :
      A ≠ B → ¬ Vs B el dom G → ¬ Vs B el v → derL (R B v :: G) A u → derL (substG G (Vs B) v) A (substL u (Vs B) v).

    Lemma der_G_substG G A B u v :
      A ≠ B → ¬ Vs B el (dom G) → ¬ Vs B el v → ¬ Vs B el u → der (R B v :: G) A u → der (substG G (Vs B) v) A u.

    Lemma der_substG_G_equiv G u v A B :
      A ≠ B → ¬ Vs B el (dom G) → ¬ Vs B el v → ¬ Vs B el u → (der (R B v :: G) A u ↔ der (substG G (Vs B) v) A u).

    Lemma inl_language_equiv G A B u v :
      A ≠ B → ¬ Vs B el (dom G) → ¬ Vs B el v → (language (substG G (Vs B) v) A u ↔ language (R B v :: G) A u).

    Fixpoint inlL L G :=
      match L with
          [] ⇒ G
        | R A u :: Lr ⇒ substG (inlL Lr G) (Vs A) u
      end.

    Inductive inlinable (G : @grammar Tt Vt) : (@grammar Tt Vt) → Prop :=
    | inN : inlinable G nil
    | inR A u Gr :
        ¬ Vs A el u → ¬ Vs A el dom Gr → ¬ Vs A el dom G → disjoint u (dom Gr) →
        inlinable G Gr → inlinable G (R A u :: Gr).
    Hint Constructors inlinable.

    Lemma inlinable_cons M G A u :
      ¬ Vs A el dom M → inlinable G M → inlinable (R A u :: G) M.

    Search _ (derT).
    Lemma der_inlL_G' M G A u :
      R A u el (inlL M G) → der (M ++ G) A u.

    Lemma der_inlL_G M G A u :
      der (inlL M G) A u → der (M ++ G) A u.

    Lemma inlL_skip G Gr A u :
      disjoint u (dom G) → inlL G (R A u :: Gr) = R A u :: inlL G Gr.

    Lemma inlL_dom M G :
      dom (inlL M G) = dom G.

    Lemma der_G_inlL M G A u :
      inlinable G M → Vs A el dom G → disjoint u (dom M) → der (M ++ G) A u → der (inlL M G) A u.

    Lemma inlL_langauge_equiv G M A u :
      inlinable G M → Vs A el dom G → (language (M ++ G) A u ↔ language (inlL M G) A u).

  End Inlining.

End Inlining.