Recipes_neutralization.My_autosubst

Set Warnings "-notation-overridden, -notation-overriden".
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq zify.
From Coq Require Import ssrfun PeanoNat Lia Arith_base.
Set Warnings "notation-overridden, notation-overriden".

Require Import AutosubstSsr ARS My_tactics.
Require Import Recipes.

Section FPottierIdeas.

Definition fv (k: nat) (t: recipe) :=
  forall σ, t.[upn k σ] = t.

Definition fv_t (k: nat) (t: term) :=
  forall σ, t.[upn k σ] = t.

Definition fv_hsubst (k: nat) (t: recipe) :=
  forall σ, t.|[upn k σ] = t.

Definition fv_old (k: nat) (t: recipe) :=
  t.[upn k (ren (+1))] = t.

Definition fv_t_old (k: nat) (t: term) :=
  t.[upn k (ren (+1))] = t.

Definition fv_hsubst_old (k: nat) (t: recipe) :=
  t.|[upn k (ren (+1))] = t.

Lemma fv_to_fv_old k t :
  fv k t -> fv_old k t.
Proof.
  by apply.
Qed.

Lemma fvt_to_fvt_old k t :
  fv_t k t -> fv_t_old k t.
Proof.
  by apply.
Qed.

Lemma fv_hsubst_to_fv_hsubst_old k t :
  fv_hsubst k t -> fv_hsubst_old k t.
Proof.
  by apply.
Qed.

Lemma generalize_fv_subst_term (T: term) θ n :
 T.[upn n (ren (+1))] = T
 -> T.[upn n θ] = T.
Proof.
  elim: T=>//=.
  { move=> x h.
    case (boolP (x < n))=> [lt|ge].
    by rewrite upnPh ifT.
    have c: upn n (ren (+1)) x = TVar x.+1.
    { rewrite upnPh ifF=> /=.
      by have->: (n + (x - n).+1)%coq_nat = x.+1 by lia.
      by lia. }
    rewrite h in c.
    inversion c.
    by lia. }
  { move=> S hS T hT h.
    inversion h.
    rewrite H1.
    rewrite H0.
  by rewrite (hS H0) (hT H1). }
Qed.

Lemma generalize_fv_hsubst (s: recipe) θ n :
 s.|[upn n (ren (+1))] = s
 -> s.|[upn n θ] = s.
Proof.
  elim: s θ n=>//=.
  { move=> s hs t ht θ n h.
    injection h=> h1 h2.
    by rewrite (hs θ n h2) (ht θ n h1). }
  { move=> s hs t ht θ n h.
    injection h=> h1 h2.
    by rewrite (hs θ n h2) (ht θ n h1). }
  { move=> s hs S θ n h.
    injection h=> h1 h2.
    rewrite (hs θ n h2).
    f_equal.
    by apply generalize_fv_subst_term. }
  { move=> f t ht θ n h.
    injection h=> h1.
    by rewrite (ht θ n h1). }
  { move=> U t ht θ n h.
    injection h=> h1.
    by rewrite (ht θ n h1). }
  { move=> t ht θ n h.
    injection h=> h1.
    f_equal.
    asimpl.
    exact (ht θ n.+1 h1). }
  { move=> t ht θ n h.
    injection h=> h1.
    f_equal.
    asimpl.
    exact (ht θ n.+1 h1). }
Qed.

Lemma iterate_iterate {A} (f : A -> A) i j x :
  iterate f i (iterate f j x) = iterate f (i + j) x.
Proof.
  induction i; intros.
  { by rewrite iterate_0. }
  { have->: i.+1 + j = S (i + j) by lia.
    by rewrite iterate_S IHi. }
Qed.

Lemma upn_upn:
  forall i j σ,
  upn i (upn j σ) = upn (i + j) σ.
Proof using .
  eauto using iterate_iterate.
Qed.

Lemma upn_upn_t:
  forall i j (σ: var -> term),
  upn i (upn j σ) = upn (i + j) σ.
Proof using .
  eauto using iterate_iterate.
Qed.

End FPottierIdeas.

Section MyLemmas.

Lemma fv_hsubst_upto_ge s n m :
  n <= m ->
  fv_hsubst n s ->
  fv_hsubst m s.
Proof.
  rewrite /fv_hsubst=> h1 h2 σ.
  have[nn hnn]: exists nn, n + nn = m
    by exists (m-n); lia.
  rewrite -hnn.
  (* Search upn. *)
  rewrite -upn_upn_t.
  by apply generalize_fv_hsubst.
Qed.

Lemma fv_hsubst_upto_ge_term (T : term) n m :
  n <= m ->
  fv_t n T ->
  fv_t m T.
Proof.
  rewrite /fv_t=> h1 h2 σ.
  have[nn hnn]: exists nn, n + nn = m
    by exists (m-n); lia.
  rewrite -hnn.
  rewrite -upn_upn_t.
  by apply generalize_fv_subst_term.
Qed.

Lemma choose_last_n_subst (T: term) :
  exists n, fv_t n T.
Proof.
  elim: T.
  { move=> x. exists x.+1. rewrite /fv_t =>//= σ.
    by rewrite upnPh ifT. }
  { exists 1. by rewrite /fv_t =>//=. }
  { move=> S [ns hs] T [nt ht].
    rewrite /fv_t=>/= .
    exists (max ns nt)=>σ.
    f_equal.
    apply fv_hsubst_upto_ge_term with ns=>//. by lia.
    apply fv_hsubst_upto_ge_term with nt=>//. by lia. }
Qed.

Lemma choose_last_n_hsubst (s: recipe) :
  exists n, fv_hsubst n s.
Proof.
  elim: s.
  { by exists 1=>/=; rewrite /fv_hsubst; asimpl. }
  { by exists 1=>/=; rewrite /fv_hsubst; asimpl. }
  { rewrite /fv_hsubst=> s [ns h1] t [nt h2].
    have ges: max ns nt >= ns by lia.
    have get: max ns nt >= nt by lia.
    exists (max ns nt)=>/= σ.
    f_equal.
    apply (fv_hsubst_upto_ge s ns (max ns nt) ges h1).
    apply (fv_hsubst_upto_ge t nt (max ns nt) get h2). }
  { rewrite /fv_hsubst=> s [ns h1] t [nt h2].
    have ges: max ns nt >= ns by lia.
    have get: max ns nt >= nt by lia.
    exists (max ns nt)=>/= σ.
    f_equal.
    apply (fv_hsubst_upto_ge s ns (max ns nt) ges h1).
    apply (fv_hsubst_upto_ge t nt (max ns nt) get h2). }
  { rewrite /fv_hsubst=> s [ns h1] S /=.
    destruct (choose_last_n_subst S) as [m h2].
    exists (max ns m)=> σ.
    have ges: max ns m >= ns by lia.
    have gem: max ns m >= m by lia.
    f_equal.
    apply (fv_hsubst_upto_ge s ns (max ns m) ges h1).
    apply (fv_hsubst_upto_ge_term S m (max ns m) gem h2). }
  { rewrite /fv_hsubst=> f s [ns h1] /=.
    exists ns=>σ.
    by rewrite h1. }
  { rewrite /fv_hsubst=> U s [ns h1] /=.
    exists ns=>σ.
    by rewrite h1. }
  { rewrite /fv_hsubst=> s [ns h1] /=.
    exists (ns.-1)=>σ.
    asimpl.
    f_equal.
    case: ns h1=>//= h.
    by apply fv_hsubst_upto_ge with 0. }
  { rewrite /fv_hsubst=> s [ns h1] /=.
    exists (ns.-1)=>σ.
    asimpl.
    f_equal.
    case: ns h1=>//= h.
    by apply fv_hsubst_upto_ge with 0. }
Qed.

Lemma free_above_n_t (T : term) (θ : var -> term) n :
   fv_t n T ->
   T.[fun i : nat => if i < n then θ i else TVar (i - n)] = T.[θ].
Proof.
  elim: T θ=>//=.
  { move=> x θ h.
    specialize (h (ren (+1))).
    rewrite /= upnPh in h.
    case (boolP (x < n))=>// h1.
    rewrite ifF in h=>//=.
    have: x = x.+1.
    { have e: (ren (+1) (x - n)).[ren (+n)] = TVar x.+1.
        simpl.
        have H: forall x, ids x = TVar x by autosubst.
        rewrite H.
        f_equal.
        by lia.
      rewrite e in h.
      by injection h. }
    by lia.
    by lia. }
  { move=> S hS T hT θ h.
    rewrite /fv_t/= in h.
    (* specialize (h (ren (+1))). *)
    (* injection h => h1 h2. *)
    have h1: forall σ, S.[upn n σ] = S.
    { move=> σ.
      specialize (h σ).
      congruence. }
    have h2: forall σ, T.[upn n σ] = T.
    { move=> σ.
      specialize (h σ).
      congruence. }
    f_equal.
    by rewrite (hS _ h1).
    by rewrite (hT _ h2). }
Qed.

Lemma free_above_n_t_old (T : term) (θ : var -> term) n :
   fv_t_old n T ->
   T.[fun i : nat => if i < n then θ i else TVar (i - n)] = T.[θ].
Proof.
  elim: T θ=>//=.
  { move=> x θ h.
    rewrite /fv_t_old/= upnPh in h.
    case (boolP (x < n))=>// h1.
    rewrite ifF in h=>//=.
    have: x = x.+1.
    { have e: (ren (+1) (x - n)).[ren (+n)] = TVar x.+1.
        simpl.
        have H: forall x, ids x = TVar x by autosubst.
        rewrite H.
        f_equal.
        by lia.
      rewrite e in h.
      by injection h. }
    by lia.
    by lia. }
  { move=> S hS T hT θ h.
    rewrite /fv_t/= in h.
    injection h => h1 h2.
    f_equal.
    by rewrite (hS _ h2).
    by rewrite (hT _ h1). }
Qed.

Lemma free_above_n (s : recipe) (θ : var -> term) n :
   fv_hsubst n s ->
   s.|[fun i : nat => if i < n then θ i else TVar (i - n)] = s.|[θ].
Proof.
  move/fv_hsubst_to_fv_hsubst_old.
  elim: s θ n=>//=.
  { move=> s hs t ht θ n h.
    injection h=> h1 h2.
    by rewrite (hs θ n h2) (ht θ n h1). }
  { move=> s hs t ht θ n h.
    injection h=> h1 h2.
    by rewrite (hs θ n h2) (ht θ n h1). }
  { move=> s hs S θ n h.
    rewrite /fv_hsubst_old/= in h.
    injection h=> h1 h2.
    rewrite (hs θ n h2).
    f_equal.
    by apply free_above_n_t_old. }
  { move=> f s hs θ n h.
    rewrite /fv_hsubst/= in h.
    injection h=> h1.
    by rewrite (hs θ n h1). }
  { move=> U s hs θ n h.
    rewrite /fv_hsubst/= in h.
    injection h=> h1.
    by rewrite (hs θ n h1). }
  { move=> s hs θ n h.
    rewrite /up=>/=.
    have h2: fv_hsubst_old n.+1 s by injection h.
    f_equal.
    have->:
        ids 0 .: (fun i : nat => if i < n then θ i else TVar (i - n)) >>> rename (+1)
      = (fun i : nat => if i < n.+1 then up θ i else TVar (i - n)).
    { unfold ".:".
      f_ext.
      case=>//= x.
      have->: x.+1 < n.+1 = (x < n) by lia.
      case (boolP (x < n))=> [lt|ge]//=.
      f_equal.
      by lia. }
    rewrite -(hs (up θ) n.+1 h2).
    set θθ := fun i : nat => if i < n.+1 then up θ i else TVar (i - n).
    specialize (hs θθ n.+1 h2).
    rewrite -hs.
    f_equal.
    f_ext=>x.
    case (boolP (x < n.+1))=>//= cmp.
    rewrite /θθ ifT=>//. }
  { move=> s hs θ n h.
    rewrite /up=>/=.
    have h2: fv_hsubst_old n.+1 s by injection h.
    f_equal.
    have->:
        ids 0 .: (fun i : nat => if i < n then θ i else TVar (i - n)) >>> rename (+1)
      = (fun i : nat => if i < n.+1 then up θ i else TVar (i - n)).
    { unfold ".:".
      f_ext.
      case=>//= x.
      have->: x.+1 < n.+1 = (x < n) by lia.
      case (boolP (x < n))=> [lt|ge]//=.
      f_equal.
      by lia. }
    rewrite -(hs (up θ) n.+1 h2).
    set θθ := fun i : nat => if i < n.+1 then up θ i else TVar (i - n).
    specialize (hs θθ n.+1 h2).
    rewrite -hs.
    f_equal.
    f_ext=>x.
    case (boolP (x < n.+1))=>//= cmp.
    rewrite /θθ ifT=>//. }
Qed.

Definition closed := fv 0.

(* Lemma closed_subst_n s n :
  fv n s -> forall σ, s = s.upn n σ.
Proof.
  elim: s n=>//=.
  { rewrite/closed/fv.
    asimpl=> h |n contra.
    + have e: upn 0 (ren (+1)) h = Var h.+1 by autosubst.
      rewrite e in contra.
      injection contra => hhh.
      by lia.
    + rewrite upnP in contra.
      case (boolP (h < n.+1))=> lt|ge σ.
      * by rewrite upnP ifT.
      * have ltb: (h < n.+1) = false by lia.
        rewrite upnP ifF=>//.
        rewrite ifF in contra=>//.
        have e: (ren (+1) (h - n.+1)) = Var (h - n.+1).+1 by autosubst.
        rewrite e in contra.
        have {}e: Var (h - n.+1).+1 = Var (h - n) by f_equal; lia.
        rewrite e in contra.
        simpl in contra.
        have {}e: ids (n + (h - n))coq_nat.+1 by autosubst.
        rewrite e in contra.
        have {}e: Var (n + (h - n))*)
    (* rewrite e. *)
    rewrite -{1}h2.
    f_equal.
    f_ext=>x.
    f_equal. admit. }
    (* by apply hs. } *)
  admit.
Admitted. *)

Lemma closed_subst s :
  closed s -> forall σ, s = s.[σ].
Proof.
  move=> h σ.
  by rewrite (h σ).
Qed.

End MyLemmas.