Library SubstAux

Require Export Term.
Require Export AssociationList.
Set Implicit Arguments.
CatchFileBetweenTagsSSubstAuxStart

Definition SSubstitution {G} (vc : VarSym G):=
  list (vType vc × Term (gsymTN (vSubstType G vc))).

CatchFileBetweenTagsSSubstAuxEnd

Definition SubFilter {G} {vc : VarSym G}
  (sub: SSubstitution vc) (lv : list (vType vc))
    : SSubstitution vc
  := (ALFilter (DeqVtype vc) sub lv).

Definition SubKeepFirst {G} {vc : VarSym G}
  (sub: SSubstitution vc) (lv : list (vType vc))
    : SSubstitution vc
  := (ALKeepFirst (DeqVtype vc) sub lv).

Ltac dalfind :=
  match goal with
    | [ |- context[ALFind (DeqVtype ?vc) ?sub ?v] ] ⇒
      let o := fresh "o" in
      remember (ALFind (DeqVtype vc) sub v) as o;
        let h := fresh "h" in
        rename_last h;
          destruct o; symmetry in h;
          [ applydup ALFindSome in h
          | applydup ALFindNone in h
          ]
  end.

Fixpoint tSSubstAux {G : CFGV} {vc : VarSym G}
  (gs : (GSym G)) (pt : Term gs)
  (sub : SSubstitution vc) {struct pt} : Term gs :=
match pt in Term gs return Term gs with
| tleaf a b ⇒ tleaf a b
| vleaf vcc var ⇒ match DeqVarSym vc vcc with
                     | left eqq ⇒
                          ALFindDef
                            (DeqVtype vcc)
                            (transport eqq sub)
                            var
                            (vleaf vcc var)
                     | right _ ⇒ (vleaf vcc var)
                     end
| tnode p mix ⇒ tnode p (mSSubstAux mix (allBndngVars vc p mix) sub)
end
with pSSubstAux {G : CFGV} {vc : VarSym G}
  {gs : (GSym G)} (pt : Pattern gs)
  (sub : SSubstitution vc) {struct pt} : Pattern gs :=
match pt with
| ptleaf a v ⇒ ptleaf a v
| pvleaf vcc var ⇒ pvleaf vcc var

| pnode p lpt ⇒ pnode p (mSSubstAux lpt [] sub)
| embed p nt ⇒ embed p (tSSubstAux nt sub)
end
with mSSubstAux {G : CFGV} {vc : VarSym G}
  (lgs : list (bool × GSym G)) (pts : Mixture lgs)
  (lbvars : list (list (vType vc)))
  (sub : SSubstitution vc)
 {struct pts}
      : Mixture lgs :=
match pts in Mixture lgs return Mixture lgs with
| mnil ⇒ mnil
| mtcons _ _ ph ptl ⇒
              mtcons
                    (tSSubstAux ph (SubFilter sub (lhead lbvars)))
                    (mSSubstAux ptl (tail lbvars) sub)
| mpcons _ _ ph ptl ⇒
              mpcons
                    (pSSubstAux ph (SubFilter sub (lhead lbvars)))
                    (mSSubstAux ptl (tail lbvars) sub)
end.

Ltac DALFindC sn :=
  unfold ALFindDef;
  match goal with
    | [ |- context[ALFind ?d ?s ?v] ] ⇒
      let sns := fresh sn "s" in
      remember (ALFind d s v) as sn;
        let h := fresh "Heq" in
        rename_last h;
        destruct sn as [sns |];
          symmetry in h;
          [ applydup ALFindSome in h
          | applydup ALFindNone in h
          ]

  end.

Section GramVC.
Variable G : CFGV.
Variable vc : VarSym G.

Definition rangeFreeVars (sub : SSubstitution vc) :=
  flat_map (fun t ⇒ tfreevars vc t) (ALRange sub).

Lemma rangeFreeVars_cons :
  ∀ v t s, rangeFreeVars ((v,t)::s) = tfreevars vc t ++ rangeFreeVars s.
Proof.
  unfold rangeFreeVars; simpl; sp.
Qed.

Lemma rangeFreeVarsApp :
  ∀ sa sb,
    rangeFreeVars (sa++sb)
    = rangeFreeVars sa ++ rangeFreeVars sb.
Proof.
  intros.
  unfold rangeFreeVars.
  rewrite <- flat_map_app.
  unfold ALRange.
  rewrite <- map_app.
  refl.
Qed.

Lemma subtractv_subset :
  ∀ sub l,
    subset (subtractv (rangeFreeVars sub) l) (rangeFreeVars sub).
Proof.
  unfold subtractv; introv.
  apply subset_diff.
  apply subset_app_r; auto.
Qed.
Hint Immediate subtractv_subset.

Lemma SSubstAuxTrivial :
     ( (∀ (s : GSym G) (t : Term s) (sub : SSubstitution vc),
            disjoint (tfreevars vc t) (ALDom sub)
            → tSSubstAux t sub = t)
         ×
        (∀ (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc),
            disjoint (pfreevars vc pt) (ALDom sub)
            → pSSubstAux pt sub = pt)
         ×
        (∀ (l : list (bool # GSym G)) (m : Mixture l)
            (sub : SSubstitution vc)
            (llva : list (list (vType vc))),
            disjoint (mfreevars vc m llva) (ALDom sub)
            → mSSubstAux m llva sub = m)).
Proof.
  intros.
  GInduction; auto;[| | | | |];
  try (intros; simpl; f_equal; f_equal; auto; fail); [| |].

  - Case "vleaf".
    introv Hdis. simpl. rename vc0 into vcc.
    destruct_head_match; auto;[].
    subst vcc.
    simpl. rw ALFindDef2Same.
    unfold ALFindDef2. destruct_head_match; auto;[].
    provefalse. destruct s; auto.
    allsimpl. rewrite DeqTrue in Hdis.
    allsimpl. disjoint_reasoning.
    apply Hdis.
    apply ALInEta in l.
    repnd; auto.

  - Case "mtcons".
    introv Hp Hm Hdis.
    allsimpl. unfold SubFilter.
    allsimpl;
    disjoint_reasoning; f_equal; auto.
    f_equal; auto; apply Hp;
    rewrite <- ALDomFilterCommute;
    unfold subtractv in Hdis0;
    apply disjoint_diff_l;
    auto.

  - Case "mpcons".
    introv Hp Hm Hdis.
    allsimpl. unfold SubFilter.
    allsimpl;
    disjoint_reasoning; f_equal; auto.
    f_equal; auto; apply Hp;
    rewrite <- ALDomFilterCommute;
    unfold subtractv in Hdis0;
    apply disjoint_diff_l;
    auto.
Qed.

Corollary SSubstAuxNilNoChange :
     ( (∀ (s : GSym G) (t : Term s),
            @tSSubstAux _ vc _ t [] = t)
         ×
        (∀ (s : GSym G) (pt : Pattern s),
             @pSSubstAux _ vc _ pt [] = pt)
         ×
        (∀ (l : list (bool # GSym G)) (m : Mixture l)
            (llva : list (list (vType vc))),
            mSSubstAux m llva [] = m)).
Proof.
  pose proof SSubstAuxTrivial. repnd.
  dands; intros; auto;
  apply_hyp; allsimpl; disjoint_reasoning.
Qed.

Lemma SSubstAuxSubFilter:
( (∀ (s : GSym G) (t : Term s) (sub : SSubstitution vc) lf,
      disjoint (tfreevars vc t) lf
      → tSSubstAux t sub
          = tSSubstAux t (SubFilter sub lf))
   ×
  (∀ (s : GSym G) (pt : Pattern s) lf (sub : SSubstitution vc),
      disjoint (pfreevars vc pt) lf
      → pSSubstAux pt sub
          = pSSubstAux pt (SubFilter sub lf))
   ×
  (∀ (l : list (bool # GSym G)) (m : Mixture l)
      (llva : list (list (vType vc))) lf (sub : SSubstitution vc),
      disjoint (mfreevars vc m llva) lf
      → mSSubstAux m llva sub
          = mSSubstAux m llva (SubFilter sub lf))).
Proof.
  intros.
  GInduction; auto;[| | | | |];
  try(intros; allsimpl; f_equal; apply H; auto);[ | | ].

- Case "vleaf".
  introv Hdis. simpl. rename vc0 into vcc.
  destruct_head_match; auto;[].
  subst vcc.
  simpl. allunfold ALFindDef.
  remember (ALFind (DeqVtype vc) (SubFilter sub lf) v) as alf.
  destruct alf as [als | aln].
  + applysym AssociationList.ALFindFilterSome in Heqalf.
    repnd. rw Heqalf0; auto.
  + applysym AssociationList.ALFindFilterNone in Heqalf.
    dorn Heqalf.
    × rw Heqalf; auto.
    × simpl in Hdis. rewrite DeqTrue in Hdis.
      simpl in Hdis. disjoint_reasoning.

- Case "mtcons".
  introv Hp Hm Hdis.
  allsimpl. unfold SubFilter.
  rw ALFilterSwap.
  rw <- ALFilterAppR.
  rw ALFilterAppAsDiff.
  disjoint_reasoning.
  rw ALFilterAppR; unfold subtractv in Hdis0.
  f_equal; try apply Hp; try apply Hm; auto.
  rw disjoint_diff_l in Hdis0; auto;fail.

- Case "mpcons".
  introv Hp Hm Hdis.
  allsimpl. unfold SubFilter.
  rw ALFilterSwap.
  rw <- ALFilterAppR.
  rw ALFilterAppAsDiff.
  disjoint_reasoning.
  rw ALFilterAppR; unfold subtractv in Hdis0.
  f_equal; try apply Hp; try apply Hm; auto.
  rw disjoint_diff_l in Hdis0; auto;fail.
Qed.

Lemma SSubstAuxBVarsDisjoint:
( (∀ (s : GSym G) (t : Term s) (sub : SSubstitution vc) lf,
      disjoint (tBndngVarsDeep vc t) lf
      → disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf
      → disjoint (tBndngVarsDeep vc (tSSubstAux t sub)) lf)
   ×
  (∀ (s : GSym G) (pt : Pattern s) lf (sub : SSubstitution vc),
      disjoint (pBndngVarsDeep vc pt) lf
      → disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf
      → disjoint (pBndngVarsDeep vc (pSSubstAux pt sub)) lf)
   ×
  (∀ (l : list (bool # GSym G)) (m : Mixture l)
      (llva : list (list (vType vc))) lf (sub : SSubstitution vc),
      disjoint (mBndngVarsDeep vc m) lf
      → disjoint (flat_map (tBndngVarsDeep vc) (ALRange sub)) lf
      → disjoint (mBndngVarsDeep vc (mSSubstAux m llva sub)) lf)
).
Proof.
  intros. GInduction; cpx.

- Case "vleaf". introv H1d H2d. allsimpl. ddeq; cpx.
  destruct e.
  simpl. unfold ALFindDef. dalfind; cpx.
  rw disjoint_flat_map_l in H2d.
  apply ALInEta in h0; cpx.

- Case "mtcons".
  introv Hypt Hypm H1d H2d. allsimpl. allsimpl; cpx;
  repeat(disjoint_reasoning).
  apply Hypt; repeat(disjoint_reasoning).
  clear H1d H1d0.
  unfold SubFilter. SetReasoning.

- Case "mpcons".
  introv Hypt Hypm H1d H2d. allsimpl. allsimpl; cpx;
  repeat(disjoint_reasoning).
  apply Hypt; repeat(disjoint_reasoning).
  clear H1d H1d0.
  unfold SubFilter. SetReasoning.
Qed.

Definition VarSubSym := gsymTN (vSubstType _ vc).
Ltac DALFind sn :=
  unfold ALFindDef;
  match goal with
    | [ |- context[ALFind ?d ?s ?v] ] ⇒
      let sns := fresh sn "s" in
      remember (ALFind d s v) as sn;
        destruct sn as [sns |]
    | [ H: context[ALFind ?d ?s ?v] |- _ ] ⇒
      let sns := fresh sn "s" in
      remember (ALFind d s v) as sn;
        destruct sn as [sns |]
  end.

Arguments pBndngVars {G} vc {gs} p : simpl nomatch.
Arguments mBndngVars {G} vc {lgs} pts : simpl nomatch.
Transparent pBndngVars.
Theorem bindersSSubstAuxNoCnange:
( ∀ (s : GSym G) (nt : Term s), True)
×
( ∀ (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc),
pBndngVars vc pt = pBndngVars vc (pSSubstAux pt sub)
)
×
( ∀ (l : list (bool # GSym G)) (m : Mixture l)
    (sub : SSubstitution vc) (lbv : list (list (vType vc)))
    (nn : nat),
    getBVarsNth vc m nn = @getBVarsNth
                            _ vc _ (mSSubstAux m lbv sub) nn
).
 GInduction; allsimpl; introns Hyp; intros; cpx;[ | | ].
  - Case "pnode". simpl. simpl pBndngVars.
    rewrite mBndngVarsAsNth.
    rewrite mBndngVarsAsNth.
    autorewrite with fast.
    apply eq_flat_maps.
    intros nn Hin. cpx.
  - simpl. destruct nn.
    + simpl. destruct lbv; cpx; simpl.
    + destruct lbv; simpl; cpx; simpl;
       eapply IHm; eauto.
  - simpl. destruct nn.
    + simpl. destruct lbv; cpx; simpl.
    + destruct lbv; simpl; cpx; simpl;
       eapply IHm; eauto.
Qed.

Lemma lBoundVarsSameSSubstAux : ∀
 (l : MixtureParam) (m : Mixture l)
 (sub: SSubstitution vc)
  (la : list (list nat))
  (lbv : list (list (vType vc))),
lBoundVars vc la m
=
lBoundVars vc la
 (mSSubstAux m
    lbv sub).
Proof.
  intros.
  apply lBoundVarsSameifNth.
  pose proof bindersSSubstAuxNoCnange.
  cpx.
Qed.

Lemma rangeFreeVarsKeepFirstAppL: ∀ sub va vb x,
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           va))
→
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           (va ++ vb))).
Proof.
  introv Hin.
  rw lin_flat_map in Hin. exrepnd.
  rw in_map_iff in Hin1. exrepnd.
  apply ALKeepFirstLin in Hin1.
  exrepnd.
  rw lin_flat_map. eexists; dands; eauto.
  rw in_map_iff; eexists; dands; eauto;[].
  allsimpl;
  apply ALKeepFirstLin.
  dands; allrw in_app_iff; cpx.
Qed.

Lemma rangeFreeVarsKeepFirstAppR: ∀ sub va vb x,
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           vb))
→
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           (va ++ vb))).
Proof.
  introv Hin.
  rw lin_flat_map in Hin. exrepnd.
  rw in_map_iff in Hin1. exrepnd.
  apply ALKeepFirstLin in Hin1.
  exrepnd.
  rw lin_flat_map. eexists; dands; eauto.
  rw in_map_iff; eexists; dands; eauto;[].
  allsimpl;
  apply ALKeepFirstLin.
  dands; allrw in_app_iff; cpx.
Qed.

Lemma rangeFreeVarsKeepFirstAppImplies: ∀ sub va vb x,
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           (va++vb)))
→
(LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           (va )))
[+]
LIn x (rangeFreeVars
        (ALKeepFirst (DeqVtype vc) sub
           (vb )))).
Proof.
  introv Hin.
  rw lin_flat_map in Hin. exrepnd.
  rw in_map_iff in Hin1. exrepnd.
  apply ALKeepFirstAppLin in Hin1.
  dorn Hin1;[left | right];
  rw lin_flat_map; eexists; dands; eauto;
  rw in_map_iff; eexists; dands; eauto.
Qed.

Hint Resolve subset_app_l subset_app_r
rangeFreeVarsKeepFirstAppL rangeFreeVarsKeepFirstAppR:
 slow.

Theorem SSubstAuxAppAwap:
( ∀ (s : GSym G) (nt : Term s)
    (suba subb : SSubstitution vc)
    (Hdis : disjoint (ALDom suba) (ALDom subb)),
      (tSSubstAux nt (suba ++ subb))
        = (tSSubstAux nt (subb ++ suba))
)
×
( ∀ (s : GSym G) (pt : Pattern s) (suba subb : SSubstitution vc)
    (Hdis : disjoint (ALDom suba) (ALDom subb)),
       (pSSubstAux pt (suba ++ subb))
          = (pSSubstAux pt (subb ++ suba))
)
×
( ∀ (l : list (bool # GSym G)) (m : Mixture l)
  (lln : list (list (vType vc)))
  (suba subb : SSubstitution vc)
  (Hdis : disjoint (ALDom suba) (ALDom subb)),
     (mSSubstAux m lln (suba ++ subb))
        = (mSSubstAux m lln (subb ++ suba))
).
Proof.
GInduction; allsimpl; introns Hyp; intros; allsimpl; cpx;
try (f_equal; auto; fail);[| |].

- Case "vleaf".
  simpl. rename vc0 into vcc.
  destruct_head_match; auto;[].
  subst vcc.
  simpl.
  allunfold ALFindDef.
  allrw ALFindApp.
  DALFind a1l; DALFind a2l; cpx;[].
  allapplysym ALFindSome.
  allapply ALInEta; exrepnd.
  disjoint_lin_contra.
- Case "mtcons".
  allsimpl; f_equal; cpx.
  unfold SubFilter. allrw ALFilterAppSub.
  apply Hyp; cpx.
  apply (subset_disjointLR Hyp1);
  SetReasoning.
again, exactly same as the mtcons case
- Case "mpcons".
  allsimpl; f_equal; cpx.
  unfold SubFilter.
  allrw ALFilterAppSub.
  apply Hyp; cpx.
  apply (subset_disjointLR Hyp1);
  SetReasoning.
Qed.

Hint Resolve lBoundVarsmBndngVars
  (snd bindersSubsetDeep)
  (snd (fst bindersSubsetDeep))
  (mcase bindersAllvarsSubset)
  (tcase bindersAllvarsSubset)
: SetReasoning.

Hint Unfold rangeFreeVars
 ALRange : SetReasoning.

This operation applies the substitution subb to each element of the range of the substitution suba. It is useful in defining the result of nested substitutions
Definition tSSubstAux_sub (suba subb : SSubstitution vc):=
  ALMapRange (fun t ⇒ tSSubstAux t subb) suba.

Lemma tSSubstAuxSubUnfold :
  ∀ (suba subb : SSubstitution vc),
  tSSubstAux_sub suba subb
  = ALMapRange (fun t ⇒ tSSubstAux t subb) suba.
Proof.
  auto.
Qed.

Lemma tSSubstAuxSubFilter:
  ∀
  (suba subb: SSubstitution vc)
  (lv : list (vType vc)),
  disjoint lv (rangeFreeVars suba)
    → tSSubstAux_sub suba
          (SubFilter subb lv)
       = tSSubstAux_sub suba subb.
Proof.
  induction suba as [|(v,t) suba Hind];
  introv Hdis ; cpx;[].
  simpl.
  unfold rangeFreeVars in Hdis.
  simpl in Hdis.
  repeat(disjoint_reasoning).
  f_equal; cpx;[].
  f_equal. symmetry.
  apply SSubstAuxSubFilter. disjoint_reasoning.
Qed.


Lemma tail_subset : ∀ {A: Type} (l: list A),
  subset (List.tl l) l.
Proof.
  (destruct l; auto; simpl; SetReasoning; apply subset_cons1; auto;fail).
Qed.
Hint Resolve tail_subset : SetReasoning.

Theorem SSubstAuxNestAsApp:
( ∀ (s : GSym G) (nt : Term s)
  (suba subb : SSubstitution vc)
  (Hdis: disjoint (tBndngVarsDeep vc nt)
                  (rangeFreeVars suba)),
  tSSubstAux (tSSubstAux nt suba) subb
  = tSSubstAux nt
          (tSSubstAux_sub suba subb ++ subb)
)
×
( ∀ (s : GSym G) (pt : Pattern s)
  (suba subb : SSubstitution vc)
  (Hdis: disjoint (pBndngVarsDeep vc pt)
                  (rangeFreeVars suba)),
  pSSubstAux (pSSubstAux pt suba) subb
      = pSSubstAux pt
          (tSSubstAux_sub suba subb ++ subb)
)
×
( ∀ (l : list (bool # GSym G)) (m : Mixture l)
  (suba subb : SSubstitution vc)
  (llm : list (list (vType vc)))
  (Hdis: disjoint (mBndngVarsDeep vc m ++ (flatten llm))
                  (rangeFreeVars suba)),
     mSSubstAux (mSSubstAux m llm suba) llm subb
      = mSSubstAux m llm
          ((tSSubstAux_sub suba subb) ++ subb)
).
Proof.
GInduction; allsimpl; introns Hyp; intros; allsimpl; cpx;
  try (f_equal;cpx;fail); allsimpl; repeat (disjoint_reasoning);
 [| | | |].
- Case "vleaf".
  simpl. rename vc0 into vcc; allsimpl;
  destruct_head_match; auto;simpl;
    [|destruct_head_match;cpx; fail].
  rename e into Heq.
  revert v. rw <- Heq.
  intros. simpl.
  DALFind a1l;[|];symmetry in Heqa1l.
  + apply ALFindRangeMapSome with
      (f:=(fun t ⇒ tSSubstAux t subb)) in Heqa1l.
    rw ALFindApp.
    unfold tSSubstAux_sub.
    rw Heqa1l; cpx.
  + apply ALFindRangeMapNone with
      (f:=(fun t ⇒ tSSubstAux t subb)) in Heqa1l.
    rw ALFindApp.
    unfold tSSubstAux_sub.
    rw Heqa1l; simpl; cpx.
    rewrite DeqTrue.
    cpx.

- Case "tnode".
  f_equal. unfold allBndngVars.
  rw <- lBoundVarsSameSSubstAux.
  apply Hyp.
  repeat(disjoint_reasoning);[].
  SetReasoning.

- Case "pnode".
  f_equal.
  apply Hyp.
  repeat(disjoint_reasoning);[].
  SetReasoning.

- Case "mtcons".
  allsimpl;f_equal;
  try apply Hyp;
  try apply Hyp0;
  repeat(disjoint_reasoning);
  SetReasoning;[].
  unfold SubFilter.
  rw ALFilterAppSub.
  unfold tSSubstAux_sub.
  rw ALMapRangeFilterCommute.
  rw <- tSSubstAuxSubUnfold.
  rewrite <- tSSubstAuxSubFilter with (lv:=lhead llm);
  [| destruct llm; allsimpl; repeat(disjoint_reasoning); auto; SetReasoning].
  apply Hyp.
  repeat(disjoint_reasoning);
  SetReasoning.

- Case "mpcons".
  allsimpl;f_equal;
  try apply Hyp;
  try apply Hyp0;
  repeat(disjoint_reasoning);
  SetReasoning;[].
  unfold SubFilter.
  rw ALFilterAppSub.
  unfold tSSubstAux_sub.
  rw ALMapRangeFilterCommute.
  rw <- tSSubstAuxSubUnfold.
  rewrite <- tSSubstAuxSubFilter with (lv:=lhead llm);
  [| destruct llm; allsimpl; repeat(disjoint_reasoning); auto; SetReasoning].
  apply Hyp.
  repeat(disjoint_reasoning);
  SetReasoning.
Qed.

Lemma tSSubstAux_sub_trivial:
∀ (suba subb : SSubstitution vc)
(Hdis: disjoint (rangeFreeVars suba) (ALDom subb)),
tSSubstAux_sub suba subb = suba.
Proof.
  induction suba; intros; cpx;[].
  unfold rangeFreeVars in Hdis.
  simpl in Hdis. disjoint_reasoning.
  allsimpl.
  simpl. f_equal; auto;[].
  f_equal.
  apply SSubstAuxTrivial.
  trivial.
Qed.

Theorem SSubstAuxNestSwap:
( ∀ (s : GSym G) (nt : Term s)
  (suba subb : SSubstitution vc)
  (H1dis: disjoint (tBndngVarsDeep vc nt)
                  (rangeFreeVars suba
                    ++ rangeFreeVars subb))
  (H2dis: disjoint (rangeFreeVars suba)
                   (ALDom subb))
  (H3dis: disjoint (rangeFreeVars subb)
                   (ALDom suba))
  (H4dis: disjoint (ALDom suba)
                   (ALDom subb)),
  tSSubstAux (tSSubstAux nt suba) subb
  = tSSubstAux (tSSubstAux nt subb) suba
)
×
( ∀ (s : GSym G) (nt : Pattern s)
  (suba subb : SSubstitution vc)
  (H1dis: disjoint (pBndngVarsDeep vc nt)
                  (rangeFreeVars suba
                    ++ rangeFreeVars subb))
  (H2dis: disjoint (rangeFreeVars suba)
                   (ALDom subb))
  (H3dis: disjoint (rangeFreeVars subb)
                   (ALDom suba))
  (H4dis: disjoint (ALDom suba)
                   (ALDom subb)),
  pSSubstAux (pSSubstAux nt suba) subb
  = pSSubstAux (pSSubstAux nt subb) suba
)
×
( ∀ (mp : MixtureParam) (nt : Mixture mp)
  (suba subb : SSubstitution vc)
  (llm : list (list (vType vc)))
  (H1dis: disjoint (mBndngVarsDeep vc nt ++ flatten llm)
                  (rangeFreeVars suba
                    ++ rangeFreeVars subb))
  (H2dis: disjoint (rangeFreeVars suba)
                   (ALDom subb))
  (H3dis: disjoint (rangeFreeVars subb)
                   (ALDom suba))
  (H4dis: disjoint (ALDom suba)
                   (ALDom subb)),
  mSSubstAux (mSSubstAux nt llm suba) llm subb
  = mSSubstAux (mSSubstAux nt llm subb) llm suba
).
Proof.
  dands; intros;
  try disjoint_reasoning;
  allrw (tcase SSubstAuxNestAsApp);
  allrw (pcase SSubstAuxNestAsApp);
  allrw (mcase SSubstAuxNestAsApp);
  repeat disjoint_reasoning;[| |];

  repeat (rw tSSubstAux_sub_trivial;
              try disjoint_reasoning);
  apply SSubstAuxAppAwap; trivial.
Qed.

Lemma disjoint_flatten_tl: ∀ {A : Type} (la : list (list A)) (lb : list A),
  disjoint (flatten (la)) lb
  → disjoint (flatten (List.tl la)) lb.
Proof.
  intros.
  SetReasoning.
Qed.

Theorem free_vars_SSubstAux:
( ∀ (s : GSym G) (nt : Term s)
    (sub : SSubstitution vc),
    disjoint (tBndngVarsDeep vc nt)
             (rangeFreeVars sub)
    → eqset
          (tfreevars vc (tSSubstAux nt sub))
          ( (diff (DeqVtype vc) (ALDom sub)
                          (tfreevars vc nt))
              ++
              (rangeFreeVars
                    (SubKeepFirst sub (tfreevars vc nt)))
          )
)
×
( ∀ (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc),
  disjoint (pBndngVarsDeep vc pt)
           (rangeFreeVars sub)
  → eqset
        (pfreevars vc (pSSubstAux pt sub))
        ( (diff (DeqVtype vc) (ALDom sub) (pfreevars vc pt))
          ++
              (rangeFreeVars
                  (SubKeepFirst sub (pfreevars vc pt)))
         )
)
×
( ∀ (l : list (bool # GSym G)) (m : Mixture l)
  (llva : list (list (vType vc)))
  (sub : SSubstitution vc),
  disjoint (mBndngVarsDeep vc m ++ (flatten llva))
           (rangeFreeVars sub)
  → eqset
        (mfreevars vc (mSSubstAux m llva sub) llva)
        ( (diff (DeqVtype vc) (ALDom sub) (mfreevars vc m llva))
           ++
              (rangeFreeVars
                  (SubKeepFirst sub (mfreevars vc m llva)))
         )
).
Proof.
unfold SubKeepFirst.
  GInduction; allsimpl; introns Hyp; intros; cpx;
  try (simpl; rw diff_nil; rw ALKeepFirstNil; simpl;
      unfold rangeFreeVars, ALRange, ALKeepFirst; simpl;
      split;cpx);[| | | | ].
- Case "vleaf".
    rename vc0 into vcc. rewrite DeqSym.
    destructr (DeqVarSym vc vcc) as [dd|dd]; auto.
    + destruct dd. allsimpl. rewrite DeqTrue.
      allunfold ALFindDef.
    allsimpl. rw diff_cons_r.
    DALFind Hd;symmetry in HeqHd.
    × applydup ALFindSome in HeqHd.
      apply ALInEta in HeqHd0. repnd.
      apply ALFindSomeKeepFirstSingleton in HeqHd.
      rw HeqHd. unfold rangeFreeVars; auto.
      simpl. rw app_nil_r. rw memberb_din.
      cases_ifd Hd; cpx;[].
      rw diff_nil. simpl.
      unfold eqset. cpx.
    × applydup ALFindNone in HeqHd. simpl. rewrite DeqTrue.
      apply ALFindNoneKeepFirstSingleton in HeqHd.
      rw HeqHd. unfold rangeFreeVars; auto.
      simpl. rw app_nil_r. rw memberb_din.
      cases_ifd Hd; cpx;[].
      rw diff_nil.
      unfold eqset. cpx.
  + rewrite DeqSym. rw <- HeqHdeq. allsimpl.
    rewrite DeqSym. rw <- HeqHdeq.
    autorewrite with fast. unfold eqset; cpx.
- Case "tnode".
  unfold allBndngVars.
  rw <- lBoundVarsSameSSubstAux.
  apply Hyp. disjoint_reasoning; cpx;[].
  SetReasoning.

- Case "pnode".
  apply Hyp.
  simpl. autorewrite with fast.
  cpx.
- Case "mtcons".
   cpx; unfold subtractv;
   allrw diff_app_r; allsimpl.
  + split.
    × introv Hin. allrw in_app_iff.

      dorn Hin;[ | apply Hyp0 in Hin;[|];
                    repeat (disjoint_reasoning);
                    [| apply disjoint_flatten_tl; trivial];
                    (rw in_app_iff in Hin;
                    dorn Hin; cpx;[];
                    right; apply rangeFreeVarsKeepFirstAppR; cpx)].

      rw in_diff in Hin; exrepnd.
      apply Hyp in Hin0;
      allrw in_app_iff; exrepnd;
      allrw in_app_iff;allsimpl; autorewrite with fast;
      repeat (disjoint_reasoning);
      unfold SubFilter; try SetReasoning;[| ].

      rename l into Hin0.
      left. left. allrw in_diff; exrepnd; dands; cpx.
      introv Hc. unfold SubFilter in Hin0.
      rw <- ALDomFilterCommute in Hin0.
      allrw in_diff. apply Hin0.
      dands; cpx.

      rename l into Hin0.
      right. apply rangeFreeVarsKeepFirstAppL.
      SetReasoning.
      rw ALKeepFirstFilterDiff;
      auto.

    × introv Hin. allrw in_app_iff.
      dorn Hin;[dorn Hin|];[ | | ].

      left. allrw in_diff. exrepnd.
      dands; cpx;[]. unfold SubFilter.
      apply Hyp.

      repeat(disjoint_reasoning); SetReasoning.

      allrw in_app_iff.
      left. allrw in_diff. exrepnd.
      dands; cpx;[].
      rw <- ALDomFilterCommute.
      rw in_diff. introv Hc.
      apply Hin. exrepnd. cpx; fail.

      allrw in_diff. right.
      exrepnd; cpx.
      apply Hyp0;repeat(disjoint_reasoning);
                    [apply disjoint_flatten_tl; trivial|];
      allrw in_diff. allrw in_app_iff.
      allrw in_diff.
      left; cpx; fail.

      apply rangeFreeVarsKeepFirstAppImplies in Hin.
      dorn Hin;[left|right].

      allrw in_diff.
      dands; cpx.
      apply Hyp;[repeat(disjoint_reasoning);
      unfold SubFilter; SetReasoning; fail|].

      allrw in_app_iff.
      allrw in_diff.
      right. SetReasoning.
      rw ALKeepFirstFilterDiff.
      eauto.

      destruct llva; allsimpl; repeat(disjoint_reasoning).
      apply Hyp3 in X.
      apply X. SetReasoning; fail.

      apply Hyp0;repeat(disjoint_reasoning);[apply disjoint_flatten_tl; trivial|].
      allrw in_app_iff.
      allrw in_diff.
      right.
      auto.

- Case "mpcons".
exactly same as the mtcons case
   cpx; unfold subtractv;
   allrw diff_app_r; allsimpl.
  + split.
    × introv Hin. allrw in_app_iff.

      dorn Hin;[ | apply Hyp0 in Hin;[|];
                    repeat (disjoint_reasoning);
                    [| apply disjoint_flatten_tl; trivial];
                    (rw in_app_iff in Hin;
                    dorn Hin; cpx;[];
                    right; apply rangeFreeVarsKeepFirstAppR; cpx)].

      rw in_diff in Hin; exrepnd.
      apply Hyp in Hin0;
      allrw in_app_iff; exrepnd;
      allrw in_app_iff;allsimpl; autorewrite with fast;
      repeat (disjoint_reasoning);
      unfold SubFilter; try SetReasoning;[| ].

      rename l into Hin0.
      left. left. allrw in_diff; exrepnd; dands; cpx.
      introv Hc. unfold SubFilter in Hin0.
      rw <- ALDomFilterCommute in Hin0.
      allrw in_diff. apply Hin0.
      dands; cpx.

      rename l into Hin0.
      right. apply rangeFreeVarsKeepFirstAppL.
      SetReasoning.
      rw ALKeepFirstFilterDiff;
      auto.

    × introv Hin. allrw in_app_iff.
      dorn Hin;[dorn Hin|];[ | | ].

      left. allrw in_diff. exrepnd.
      dands; cpx;[]. unfold SubFilter.
      apply Hyp.

      repeat(disjoint_reasoning); SetReasoning.

      allrw in_app_iff.
      left. allrw in_diff. exrepnd.
      dands; cpx;[].
      rw <- ALDomFilterCommute.
      rw in_diff. introv Hc.
      apply Hin. exrepnd. cpx; fail.

      allrw in_diff. right.
      exrepnd; cpx.
      apply Hyp0;repeat(disjoint_reasoning);
                    [apply disjoint_flatten_tl; trivial|];
      allrw in_diff. allrw in_app_iff.
      allrw in_diff.
      left; cpx; fail.

      apply rangeFreeVarsKeepFirstAppImplies in Hin.
      dorn Hin;[left|right].

      allrw in_diff.
      dands; cpx.
      apply Hyp;[repeat(disjoint_reasoning);
      unfold SubFilter; SetReasoning; fail|].

      allrw in_app_iff.
      allrw in_diff.
      right. SetReasoning.
      rw ALKeepFirstFilterDiff.
      eauto.

      destruct llva; allsimpl; repeat(disjoint_reasoning).
      apply Hyp3 in X.
      apply X. SetReasoning; fail.

      apply Hyp0;repeat(disjoint_reasoning);[apply disjoint_flatten_tl; trivial|].
      allrw in_app_iff.
      allrw in_diff.
      right.
      auto.
Qed.

Lemma in_ALRange_ALFilter_implies :
  ∀ (sub : SSubstitution vc) l,
    subset
      (ALRange (SubFilter sub l))
      (ALRange sub).
Proof.
  unfold SubFilter.
  unfold subset, ALRange; introv i.
  allrw in_map_iff; exrepnd; allsimpl; subst.
  ∃ (a0,a); simpl; sp.
  allapply ALFilterLIn; sp.
Qed.

Lemma rangeFreeVars_ALFilter_subset :
  ∀ (sub : SSubstitution vc) l,
    subset (rangeFreeVars (SubFilter sub l))
           (rangeFreeVars sub).
Proof.
  introv i.
  allunfold rangeFreeVars.
  allrw lin_flat_map; exrepnd.
  ∃ x0; sp.
  allapply in_ALRange_ALFilter_implies; sp.
Qed.

End GramVC.