lnr.v

Require Import Coq.Arith.PeanoNat.

Definition VarIndex := nat.
Parameter atom : Set.
Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}.


Section expr_ind.
  Inductive Expr : Type :=
  | BVar : VarIndex -> VarIndex -> Expr
  | FVar : atom -> Expr
  | LetB : list Expr -> Expr -> Expr.

  Variable P : Expr -> Prop.

  Hypothesis Expr_bvar :
    forall (i j: VarIndex), P (BVar i j).
  Hypothesis Expr_fvar :
    forall (i : atom), P (FVar i).
  Hypothesis Expr_let :
    forall e: Expr, P e -> forall vs : list Expr,
        Forall P vs -> P (LetB vs e).
  
  Fixpoint expr_ind (e: Expr) : P e :=
    match e with
    | BVar i j => Expr_bvar i j
    | FVar i => Expr_fvar i
    | LetB vs e' =>
      Expr_let e' (expr_ind e') vs
               ((fix list_varExpr_ind (vs: list Expr) :=
                   match vs with
                   | cons ve vses =>
                     Forall_cons
                       ve
                       (expr_ind ve)
                       (list_varExpr_ind vses)
                   | nil => Forall_nil P
                   end) vs)
    end.

End expr_ind.


  Section Util_Functions.

    Fixpoint open_rec (k: VarIndex) (u: list Expr) (e: Expr) :=
      match e with
      | BVar i j => if Nat.eq_dec k i then List.nth j u e else e
      | FVar x => e
      | LetB es e' => LetB (List.map (open_rec (S k) u) es) (open_rec (S k) u e')
      end.

    Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).

    Definition open e u := open_rec 0 u e.
        
    Lemma open_rec_lc_core : forall e (j: VarIndex) v (i: VarIndex) u,
        i <> j ->
        {j ~> v} e = {i ~> u} ({j ~> v} e) ->
        e = {i ~> u} e.
    Proof.
      induction e using expr_ind; intros k1 v k2 u Neq H0; simpl in *; try eauto.
      - destruct (Nat.eq_dec k2 i); destruct (Nat.eq_dec k1 i).
        + subst i; contradiction.
        + subst i. inversion H0; subst.
          destruct (Nat.eq_dec k2 k2).
          * apply H1.
          * contradict n0; reflexivity.
        + reflexivity.
        + reflexivity.
      - f_equal.
        + induction vs.
          * reflexivity.
          * simpl.
            f_equal.
            -- inversion H; subst.
               eapply H3.
               ++ eapply PeanoNat.Nat.succ_inj_wd_neg in Neq.
                  eapply Neq.
               ++ inversion H0; subst.
                  eapply H2.
            -- apply IHvs.
               ++ inversion H; subst.
                  apply H4.
               ++ inversion H0; subst.
                  reflexivity.
        + eapply IHe.
          * eapply PeanoNat.Nat.succ_inj_wd_neg in Neq.
            eapply Neq.
          * inversion H0; subst.
            apply H3.
    Qed.