File IndexManipulation

From MatchingLogic Require Export Substitution
                                  Freshness.

Import MatchingLogic.Substitution.Notations.

Section index_manipulation.
  Context {Σ : Signature}.
  Open Scope ml_scope.

  Fixpoint nest_ex_aux level more ϕ {struct ϕ} : Pattern :=
    match ϕ with
    | patt_free_evar _ ⇒ ϕ
    | patt_free_svar _ ⇒ ϕ
    | patt_bound_evar n ⇒ patt_bound_evar (if decide (n < level) is left _ then n else n + more)
    | patt_bound_svar _ ⇒ ϕ
    | patt_sym _ ⇒ ϕ
    | patt_bott ⇒ ϕ
    | patt_app ϕ₁ ϕ₂ ⇒ patt_app (nest_ex_aux level more ϕ₁) (nest_ex_aux level more ϕ₂)
    | patt_imp ϕ₁ ϕ₂ ⇒ patt_imp (nest_ex_aux level more ϕ₁) (nest_ex_aux level more ϕ₂)
    | patt_exists ϕ' ⇒ patt_exists (nest_ex_aux (S level) more ϕ')
    | patt_mu ϕ' ⇒ patt_mu (nest_ex_aux level more ϕ')
    end.

  Fixpoint nest_mu_aux level more ϕ {struct ϕ} : Pattern :=
    match ϕ with
    | patt_free_evar _ ⇒ ϕ
    | patt_free_svar _ ⇒ ϕ
    | patt_bound_evar _ ⇒ ϕ
    | patt_bound_svar n ⇒ patt_bound_svar (if decide (n < level) is left _ then n else n + more)
    | patt_sym _ ⇒ ϕ
    | patt_bott ⇒ ϕ
    | patt_app ϕ₁ ϕ₂ ⇒ patt_app (nest_mu_aux level more ϕ₁) (nest_mu_aux level more ϕ₂)
    | patt_imp ϕ₁ ϕ₂ ⇒ patt_imp (nest_mu_aux level more ϕ₁) (nest_mu_aux level more ϕ₂)
    | patt_exists ϕ' ⇒ patt_exists (nest_mu_aux level more ϕ')
    | patt_mu ϕ' ⇒ patt_mu (nest_mu_aux (S level) more ϕ')
    end.

  Definition nest_ex ϕ := nest_ex_aux 0 1 ϕ.
  Definition nest_mu ϕ := nest_mu_aux 0 1 ϕ.

  Lemma bevar_occur_nest_ex dbi more φ:
    ∀ x, x ≥ dbi → x < dbi + more → bevar_occur (nest_ex_aux dbi more φ) x = false.

  Lemma bsvar_occur_nest_mu dbi more φ:
    ∀ x, x ≥ dbi → x < dbi + more → bsvar_occur (nest_mu_aux dbi more φ) x = false.

  Corollary not_bevar_occur_level_nest_ex_aux level more ϕ :
    more > 0 →
    bevar_occur (nest_ex_aux level more ϕ) level = false.

  Corollary not_bsvar_occur_level_nest_mu_aux level more ϕ :
    more > 0 →
    bsvar_occur (nest_mu_aux level more ϕ) level = false.

  Corollary not_bevar_occur_0_nest_ex ϕ :
    bevar_occur (nest_ex ϕ) 0 = false.

  Corollary not_bsvar_occur_0_nest_mu ϕ :
    bsvar_occur (nest_mu ϕ) 0 = false.

  Lemma nest_ex_aux_wfcex level more ϕ:
    well_formed_closed_ex_aux ϕ level →
    nest_ex_aux level more ϕ = ϕ.

  Lemma nest_mu_aux_wfcmu level more ϕ:
    well_formed_closed_mu_aux ϕ level →
    nest_mu_aux level more ϕ = ϕ.

  Lemma nest_ex_gt : ∀ φ dbi dbi2 ψ more, dbi2 ≥ dbi → well_formed_closed ψ →
     (nest_ex_aux dbi more φ)^[evar: (dbi2 + more) ↦ ψ] = nest_ex_aux dbi more (φ^[evar: dbi2 ↦ ψ]).

  Lemma nest_mu_gt : ∀ φ dbi dbi2 ψ more, dbi2 ≥ dbi → well_formed_closed ψ →
     (nest_mu_aux dbi more φ)^[svar: (dbi2 + more) ↦ ψ] = nest_mu_aux dbi more (φ^[svar: dbi2 ↦ ψ]).

  Lemma nest_ex_gt_evar_quantify : ∀ φ dbi dbi2 x more, dbi ≥ dbi2 →
     (nest_ex_aux dbi2 more φ)^{{evar: x ↦ dbi + more}} =
     nest_ex_aux dbi2 more (φ^{{evar: x ↦ dbi}}).

  Lemma nest_mu_gt_svar_quantify : ∀ φ dbi dbi2 x more, dbi ≥ dbi2 →
     (nest_mu_aux dbi2 more φ)^{{svar: x ↦ dbi + more}} =
     nest_mu_aux dbi2 more (φ^{{svar: x ↦ dbi}}).

  Lemma nest_mu_evar_quantify : ∀ φ dbi dbi2 x more,
     (nest_mu_aux dbi2 more φ)^{{evar: x ↦ dbi}} = nest_mu_aux dbi2 more (φ^{{evar: x ↦ dbi}}).

  Lemma nest_ex_svar_quantify : ∀ φ dbi dbi2 x more,
     (nest_ex_aux dbi2 more φ)^{{svar: x ↦ dbi}} = nest_ex_aux dbi2 more (φ^{{svar: x ↦ dbi}}).

  Lemma nest_ex_free_evar_subst : ∀ φ dbi x more ψ,
     well_formed_closed_ex_aux ψ dbi →
     (nest_ex_aux dbi more φ)^[[evar: x ↦ ψ]] =
     nest_ex_aux dbi more (φ^[[evar: x ↦ ψ]]).

  Lemma nest_mu_free_evar_subst : ∀ φ dbi x more ψ,
     well_formed_closed_mu_aux ψ dbi →
     (nest_mu_aux dbi more φ)^[[evar: x ↦ ψ]] =
     nest_mu_aux dbi more (φ^[[evar: x ↦ ψ]]).

  Lemma nest_ex_free_svar_subst : ∀ φ dbi X more ψ,
     well_formed_closed_ex_aux ψ dbi →
     (nest_ex_aux dbi more φ)^[[svar: X ↦ ψ]] =
     nest_ex_aux dbi more (φ^[[svar: X ↦ ψ]]).

  Lemma nest_mu_free_svar_subst : ∀ φ dbi X more ψ,
     well_formed_closed_mu_aux ψ dbi →
     (nest_mu_aux dbi more φ)^[[svar: X ↦ ψ]] =
     nest_mu_aux dbi more (φ^[[svar: X ↦ ψ]]).

  Lemma nest_ex_same_general : ∀ φ dbi ψ more,
     ∀ x, x ≥ dbi → x < dbi + more →
     (nest_ex_aux dbi more φ)^[evar: x ↦ ψ] = nest_ex_aux dbi (pred more) φ.

  Lemma nest_mu_same_general : ∀ φ dbi ψ more,
     ∀ x, x ≥ dbi → x < dbi + more →
     (nest_mu_aux dbi more φ)^[svar: x ↦ ψ] = nest_mu_aux dbi (pred more) φ.

  Lemma nest_mu_aux_0 level p:
    nest_mu_aux level 0 p = p.

  Lemma nest_ex_aux_0 level p:
    nest_ex_aux level 0 p = p.

  Corollary nest_ex_same : ∀ φ dbi ψ,
     (nest_ex_aux dbi 1 φ)^[evar: dbi ↦ ψ] = φ.

  Corollary nest_mu_same : ∀ φ dbi ψ,
     (nest_mu_aux dbi 1 φ)^[svar: dbi ↦ ψ] = φ.

  Lemma fuse_nest_ex n more more' p:
    ∀ x, x ≤ more → nest_ex_aux (n + x) more' (nest_ex_aux n more p) = nest_ex_aux n (more + more') p.

  Lemma fuse_nest_mu n more more' p:
    ∀ x, x ≤ more → nest_mu_aux (n + x) more' (nest_mu_aux n more p) = nest_mu_aux n (more + more') p.

  Corollary fuse_nest_ex_same n more more' p:
    nest_ex_aux n more' (nest_ex_aux n more p) = nest_ex_aux n (more + more') p.

  Corollary fuse_nest_mu_same n more more' p:
    nest_mu_aux n more' (nest_mu_aux n more p) = nest_mu_aux n (more + more') p.

 Lemma bsvar_subst_nest_ex_aux_comm level more ϕ dbi ψ:
    well_formed_closed_ex_aux ψ level →
    (nest_ex_aux level more ϕ)^[svar: dbi ↦ ψ] = nest_ex_aux level more (ϕ^[svar: dbi ↦ ψ]).

  Lemma svar_open_nest_ex_aux_comm level more ϕ dbi X:
    (nest_ex_aux level more ϕ)^{svar: dbi ↦ X} =
    nest_ex_aux level more (ϕ^{svar: dbi ↦ X}).

  Lemma bevar_subst_nest_mu_aux_comm level more ϕ dbi ψ:
    well_formed_closed_mu_aux ψ level →
    (nest_mu_aux level more ϕ)^[evar: dbi ↦ ψ] = nest_mu_aux level more (ϕ^[evar: dbi ↦ ψ]).

  Lemma evar_open_nest_mu_aux_comm level more ϕ dbi X:
    (nest_mu_aux level more ϕ)^{evar: dbi ↦ X} =
    nest_mu_aux level more (ϕ^{evar: dbi ↦ X}).

  Lemma free_svars_nest_ex_aux dbi more ϕ:
    free_svars (nest_ex_aux dbi more ϕ) = free_svars ϕ.

  Lemma free_evars_nest_mu_aux dbi more ϕ:
    free_evars (nest_mu_aux dbi more ϕ) = free_evars ϕ.

  Lemma free_evars_nest_ex_aux dbi more ϕ:
    free_evars (nest_ex_aux dbi more ϕ) = free_evars ϕ.

  Corollary free_evars_nest_ex ϕ:
    free_evars (nest_ex ϕ) = free_evars ϕ.

  Lemma free_svars_nest_mu_aux dbi more ϕ:
    free_svars (nest_mu_aux dbi more ϕ) = free_svars ϕ.

  Corollary free_svars_nest_mu ϕ:
    free_svars (nest_mu ϕ) = free_svars ϕ.

  Corollary fresh_svar_nest_ex_aux dbi more ϕ:
    fresh_svar (nest_ex_aux dbi more ϕ) = fresh_svar ϕ.

  Corollary fresh_evar_nest_mu_aux dbi more ϕ:
    fresh_evar (nest_mu_aux dbi more ϕ) = fresh_evar ϕ.

  Corollary fresh_evar_nest_ex_aux dbi more ϕ:
    fresh_evar (nest_ex_aux dbi more ϕ) = fresh_evar ϕ.

  Corollary fresh_svar_nest_mu_aux dbi more ϕ:
    fresh_svar (nest_mu_aux dbi more ϕ) = fresh_svar ϕ.

  Corollary svar_open_nest_ex_comm ϕ dbi X:
    (nest_ex ϕ)^{svar: dbi ↦ X} = nest_ex (ϕ^{svar: dbi ↦ X}).

  Corollary evar_open_nest_mu_comm ϕ dbi X:
    (nest_mu ϕ)^{evar: dbi ↦ X} = nest_mu (ϕ^{evar: dbi ↦ X}).

  Lemma wfc_mu_nest_mu psi level level' more:
    well_formed_closed_mu_aux psi level →
    well_formed_closed_mu_aux (nest_mu_aux level' more psi) (level+more).

  Lemma wfc_mu_nest_mu' psi level level' less:
    level ≥ less →
    well_formed_closed_mu_aux psi (level - less) →
    well_formed_closed_mu_aux (nest_mu_aux level' less psi) level.

  Lemma wfc_ex_nest_ex psi level level' more:
    well_formed_closed_ex_aux psi level →
    well_formed_closed_ex_aux (nest_ex_aux level' more psi) (level+more).

  Lemma wfc_ex_nest_ex' psi level level' less:
    level ≥ less →
    well_formed_closed_ex_aux psi (level - less) →
    well_formed_closed_ex_aux (nest_ex_aux level' less psi) level.

  Lemma wfc_ex_nest_mu dbi level more ϕ:
    well_formed_closed_ex_aux (nest_mu_aux level more ϕ) dbi
    = well_formed_closed_ex_aux ϕ dbi
  .

  Lemma wfc_mu_nest_ex dbi level more ϕ:
    well_formed_closed_mu_aux (nest_ex_aux level more ϕ) dbi
    = well_formed_closed_mu_aux ϕ dbi
  .

  Lemma impl_wfc_mu_nest_ex dbi level more ϕ:
    well_formed_closed_mu_aux ϕ dbi = true →
    well_formed_closed_mu_aux (nest_ex_aux level more ϕ) dbi = true
  .

  Lemma Private_positive_negative_occurrence_db_nest_mu_aux dbi level more ϕ:
    (no_negative_occurrence_db_b dbi (nest_mu_aux level more ϕ)
     = if decide (dbi < level) is left _ then no_negative_occurrence_db_b dbi ϕ
       else if decide (dbi < level + more) is left _ then true
            else no_negative_occurrence_db_b (dbi-more) ϕ
    ) ∧ (
      no_positive_occurrence_db_b dbi (nest_mu_aux level more ϕ)
     = if decide (dbi < level) is left _ then no_positive_occurrence_db_b dbi ϕ
       else if decide (dbi < level + more) is left _ then true
            else no_positive_occurrence_db_b (dbi-more) ϕ
    ).

  Lemma no_negative_occurrence_db_nest_mu_aux dbi level more ϕ:
    no_negative_occurrence_db_b dbi (nest_mu_aux level more ϕ)
     = if decide (dbi < level) is left _ then no_negative_occurrence_db_b dbi ϕ
       else if decide (dbi < level + more) is left _ then true
            else no_negative_occurrence_db_b (dbi-more) ϕ.

  Lemma no_positive_occurrence_db_nest_mu_aux dbi level more ϕ:
    no_positive_occurrence_db_b dbi (nest_mu_aux level more ϕ)
     = if decide (dbi < level) is left _ then no_positive_occurrence_db_b dbi ϕ
       else if decide (dbi < level + more) is left _ then true
            else no_positive_occurrence_db_b (dbi-more) ϕ.

  Lemma well_formed_positive_nest_mu_aux level more ϕ:
    well_formed_positive (nest_mu_aux level more ϕ) = well_formed_positive ϕ.

  Lemma no_negative_occurrence_db_nest_ex_aux level more dbi ϕ:
    no_negative_occurrence_db_b dbi (nest_ex_aux level more ϕ)
    = no_negative_occurrence_db_b dbi ϕ
  with no_positive_occurrence_db_nest_ex_aux level more dbi ϕ:
    no_positive_occurrence_db_b dbi (nest_ex_aux level more ϕ)
    = no_positive_occurrence_db_b dbi ϕ
  .

  Lemma well_formed_positive_nest_ex_aux level more ϕ:
    well_formed_positive (nest_ex_aux level more ϕ) = well_formed_positive ϕ.

  Lemma impl_well_formed_positive_nest_ex_aux level more ϕ:
    well_formed_positive ϕ = true →
    well_formed_positive (nest_ex_aux level more ϕ) = true.

  Definition simpl_free_evars :=
    (
      (@left_id_L EVarSet ∅ (@union _ _)),
      (@right_id_L EVarSet ∅ (@union _ _)),
      @free_evars_nest_ex_aux,
      @nest_ex_same,
      @free_evars_nest_ex
    ).
  Definition simpl_free_svars :=
    (
      (@left_id_L SVarSet ∅ (@union _ _)),
      (@right_id_L SVarSet ∅ (@union _ _)),
      @free_svars_nest_mu_aux,
      @nest_mu_same,
      @free_svars_nest_mu
    ).

End index_manipulation.

Tactic Notation "solve_free_evars_inclusion" int_or_var(depth) :=
  simpl;
  (do ? [rewrite simpl_free_evars/=]);
  auto;
  clear;
  set_solver.

Ltac unify_free_evar_conditions :=
  match goal with
  | |- context C [free_evars (foldr _ _ _)] ⇒
      rewrite free_evars_of_list_foldr
  | |- context C [free_evars_of_list _] ⇒ unfold free_evars_of_list
  | [H : context C [free_evars (foldr _ _ _)] |- _] ⇒
      rewrite free_evars_of_list_foldr in H
  | [H: context C [free_evars_of_list _] |- _] ⇒ unfold free_evars_of_list in H
  end.
Ltac simplify_map_app_union :=
  match goal with
  | |- context C [map _ (_ ++ _)] ⇒ rewrite map_app
  | [H : context C [map _ (_ ++ _)] |- _] ⇒ rewrite map_app in H
  | |- context C [union_list (_ ++ _)] ⇒ rewrite union_list_app
  | [H : context C [union_list (_ ++ _)] |- _] ⇒ rewrite union_list_app in H
  end.
(* same as the previous "solve_free_evars_inclusion", but without clearing,
   and support for list of free evars *)
Tactic Notation "solve_free_evars" int_or_var(depth) :=
  unfold evar_is_fresh_in in *;
  repeat unify_free_evar_conditions;
  repeat simplify_map_app_union;
  simpl in *;
  repeat rewrite free_evars_evar_quantify;
  (do ? [rewrite simpl_free_evars/=]);
  auto;
  set_solver.

Tactic Notation "solve_free_svars_inclusion" int_or_var(depth) :=
  simpl;
  (do ? [rewrite simpl_free_svars/=]) ;
  auto;
  clear;
  set_solver.