Library MetaCoq.PCUIC.PCUICPosition

Inductive choice :=
| app_l
| app_r
| case_c
| proj_c
| lam_ty
| lam_tm
| prod_l
| prod_r

| let_in.


Instance reflect_choice : ReflectEq choice :=
  let h := EqDec_ReflectEq choice in _.

Definition position := list choice.

Fixpoint validpos t (p : position) {struct p} :=
  match p with
  | [] ⇒ true
  | c :: p ⇒
    match c, t with
    | app_l, tApp u v ⇒ validpos u p
    | app_r, tApp u v ⇒ validpos v p
    | case_c, tCase indn pr c brs ⇒ validpos c p
    | proj_c, tProj pr c ⇒ validpos c p
    | lam_ty, tLambda na A t ⇒ validpos A p
    | lam_tm, tLambda na A t ⇒ validpos t p
    | prod_l, tProd na A B ⇒ validpos A p
    | prod_r, tProd na A B ⇒ validpos B p
    
    | let_in, tLetIn na A b t ⇒ validpos t p
    | _, _ ⇒ false
    end
  end.

Definition pos (t : term) := { p : position | validpos t p = true }.


Definition dapp_l u v (p : pos u) : pos (tApp u v) :=
  exist (app_l :: ` p) (proj2_sig p).

Definition dapp_r u v (p : pos v) : pos (tApp u v) :=
  exist (app_r :: ` p) (proj2_sig p).

Definition dcase_c indn pr c brs (p : pos c) : pos (tCase indn pr c brs) :=
  exist (case_c :: ` p) (proj2_sig p).

Definition dproj_c pr c (p : pos c) : pos (tProj pr c) :=
  exist (proj_c :: ` p) (proj2_sig p).

Definition dlam_ty na A t (p : pos A) : pos (tLambda na A t) :=
  exist (lam_ty :: ` p) (proj2_sig p).

Definition dlam_tm na A t (p : pos t) : pos (tLambda na A t) :=
  exist (lam_tm :: ` p) (proj2_sig p).

Definition dprod_l na A B (p : pos A) : pos (tProd na A B) :=
  exist (prod_l :: ` p) (proj2_sig p).

Definition dprod_r na A B (p : pos B) : pos (tProd na A B) :=
  exist (prod_r :: ` p) (proj2_sig p).

Definition dlet_in na A b t (p : pos t) : pos (tLetIn na A b t) :=
  exist (let_in :: ` p) (proj2_sig p).

Lemma eq_term_upto_valid_pos :
  ∀ {u v p Re Rle},
    validpos u p →
    eq_term_upto_univ Re Rle u v →
    validpos v p.

Lemma eq_term_valid_pos :
  ∀ `{cf : checker_flags} {G u v p},
    validpos u p →
    eq_term G u v →
    validpos v p.

Inductive positionR : position → position → Prop :=
| positionR_app_lr p q : positionR (app_r :: p) (app_l :: q)
| positionR_deep c p q : positionR p q → positionR (c :: p) (c :: q)
| positionR_root c p : positionR (c :: p) [].


Definition posR {t} (p q : pos t) : Prop :=
  positionR (` p) (` q).

Lemma posR_Acc :
  ∀ t p, Acc (@posR t) p.

Fixpoint atpos t (p : position) {struct p} : term :=
  match p with
  | [] ⇒ t
  | c :: p ⇒
    match c, t with
    | app_l, tApp u v ⇒ atpos u p
    | app_r, tApp u v ⇒ atpos v p
    | case_c, tCase indn pr c brs ⇒ atpos c p
    | proj_c, tProj pr c ⇒ atpos c p
    | lam_ty, tLambda na A t ⇒ atpos A p
    | lam_tm, tLambda na A t ⇒ atpos t p
    | prod_l, tProd na A B ⇒ atpos A p
    | prod_r, tProd na A B ⇒ atpos B p
    | let_in, tLetIn na A b t ⇒ atpos t p
    | _, _ ⇒ tRel 0
    end
  end.

Lemma poscat_atpos :
  ∀ t p q, atpos t (p ++ q) = atpos (atpos t p) q.

Lemma poscat_valid :
  ∀ t p q,
    validpos t p →
    validpos (atpos t p) q →
    validpos t (p ++ q).

Lemma positionR_poscat :
  ∀ p q1 q2,
    positionR q1 q2 →
    positionR (p ++ q1) (p ++ q2).

Lemma atpos_assoc :
  ∀ t p q,
    atpos (atpos t p) q = atpos t (p ++ q).

Definition transitive {A} (R : A → A → Prop) :=
  ∀ u v w, R u v → R v w → R u w.

Lemma positionR_trans : transitive positionR.

Lemma posR_trans :
  ∀ t, transitive (@posR t).

Lemma positionR_poscat_nonil :
  ∀ p q, q ≠ [] → positionR (p ++ q) p.

Inductive stack : Type :=
| Empty
| App (t : term) (π : stack)
| Fix (f : mfixpoint term) (n : nat) (args : list term) (π : stack)
| CoFix (f : mfixpoint term) (n : nat) (args : list term) (π : stack)
| Case (indn : inductive × nat) (p : term) (brs : list (nat × term)) (π : stack)
| Proj (p : projection) (π : stack)
| Prod_l (na : name) (B : term) (π : stack)
| Prod_r (na : name) (A : term) (π : stack)
| Lambda_ty (na : name) (b : term) (π : stack)
| Lambda_tm (na : name) (A : term) (π : stack)
| coApp (t : term) (π : stack).

Notation "'ε'" := (Empty).


Instance reflect_stack : ReflectEq stack :=
  let h := EqDec_ReflectEq stack in _.

Fixpoint zipc t stack :=
  match stack with
  | ε ⇒ t
  | App u π ⇒ zipc (tApp t u) π
  | Fix f n args π ⇒ zipc (tApp (mkApps (tFix f n) args) t) π
  | CoFix f n args π ⇒ zipc (tApp (mkApps (tCoFix f n) args) t) π
  | Case indn pred brs π ⇒ zipc (tCase indn pred t brs) π
  | Proj p π ⇒ zipc (tProj p t) π
  | Prod_l na B π ⇒ zipc (tProd na t B) π
  | Prod_r na A π ⇒ zipc (tProd na A t) π
  | Lambda_ty na b π ⇒ zipc (tLambda na t b) π
  | Lambda_tm na A π ⇒ zipc (tLambda na A t) π
  | coApp u π ⇒ zipc (tApp u t) π
  end.

Definition zip (t : term × stack) := zipc (fst t) (snd t).

Tactic Notation "zip" "fold" "in" hyp(h) :=
  lazymatch type of h with
  | context C[ zipc ?t ?π ] ⇒
    let C' := context C[ zip (t,π) ] in
    change C' in h
  end.

Tactic Notation "zip" "fold" :=
  lazymatch goal with
  | |- context C[ zipc ?t ?π ] ⇒
    let C' := context C[ zip (t,π) ] in
    change C'
  end.

Fixpoint decompose_stack π :=
  match π with
  | App u π ⇒ let '(l,π) := decompose_stack π in (u :: l, π)
  | _ ⇒ ([], π)
  end.

Fixpoint appstack l π :=
  match l with
  | u :: l ⇒ App u (appstack l π)
  | [] ⇒ π
  end.

Lemma decompose_stack_eq :
  ∀ π l ρ,
    decompose_stack π = (l, ρ) →
    π = appstack l ρ.

Lemma decompose_stack_not_app :
  ∀ π l u ρ,
    decompose_stack π = (l, App u ρ) → False.

Lemma zipc_appstack :
  ∀ {t args ρ},
    zipc t (appstack args ρ) = zipc (mkApps t args) ρ.

Lemma decompose_stack_appstack :
  ∀ l ρ,
    decompose_stack (appstack l ρ) =
    (l ++ fst (decompose_stack ρ), snd (decompose_stack ρ)).

Fixpoint decompose_stack_at π n : option (list term × term × stack) :=
  match π with
  | App u π ⇒
    match n with
    | 0 ⇒ ret ([], u, π)
    | S n ⇒
      r <- decompose_stack_at π n ;;
        let '(l, v, π) := r in
        ret (u :: l, v, π)
    end
  | _ ⇒ None
  end.

Lemma decompose_stack_at_eq :
  ∀ π n l u ρ,
    decompose_stack_at π n = Some (l,u,ρ) →
    π = appstack l (App u ρ).

Lemma decompose_stack_at_length :
  ∀ π n l u ρ,
    decompose_stack_at π n = Some (l,u,ρ) →
    #|l| = n.

Fixpoint stack_context π : context :=
  match π with
  | ε ⇒ []
  | App u π ⇒ stack_context π
  | Fix f n args π ⇒ stack_context π
  | CoFix f n args π ⇒ stack_context π
  | Case indn pred brs π ⇒ stack_context π
  | Proj p π ⇒ stack_context π
  | Prod_l na B π ⇒ stack_context π
  | Prod_r na A π ⇒ stack_context π ,, vass na A
  | Lambda_ty na u π ⇒ stack_context π
  | Lambda_tm na A π ⇒ stack_context π ,, vass na A
  | coApp u π ⇒ stack_context π
  end.

Lemma stack_context_appstack :
  ∀ {π args},
    stack_context (appstack args π) = stack_context π.

Fixpoint stack_position π : position :=
  match π with
  | ε ⇒ []
  | App u ρ ⇒ stack_position ρ ++ [ app_l ]
  | Fix f n args ρ ⇒ stack_position ρ ++ [ app_r ]
  | CoFix f n args ρ ⇒ stack_position ρ ++ [ app_r ]
  | Case indn pred brs ρ ⇒ stack_position ρ ++ [ case_c ]
  | Proj pr ρ ⇒ stack_position ρ ++ [ proj_c ]
  | Prod_l na B ρ ⇒ stack_position ρ ++ [ prod_l ]
  | Prod_r na A ρ ⇒ stack_position ρ ++ [ prod_r ]
  | Lambda_ty na u ρ ⇒ stack_position ρ ++ [ lam_ty ]
  | Lambda_tm na A ρ ⇒ stack_position ρ ++ [ lam_tm ]
  | coApp u ρ ⇒ stack_position ρ ++ [ app_r ]
  end.

Lemma stack_position_atpos :
  ∀ t π, atpos (zipc t π) (stack_position π) = t.

Lemma stack_position_valid :
  ∀ t π, validpos (zipc t π) (stack_position π).

Definition stack_pos t π : pos (zipc t π) :=
  exist (stack_position π) (stack_position_valid t π).

Fixpoint list_make {A} n x : list A :=
  match n with
  | 0 ⇒ []
  | S n ⇒ x :: list_make n x
  end.

Lemma list_make_app_r :
  ∀ A n (x : A),
    x :: list_make n x = list_make n x ++ [x].

Lemma stack_position_appstack :
  ∀ args ρ,
    stack_position (appstack args ρ) =
    stack_position ρ ++ list_make #|args| app_l.

Section Stacks.

  Context (Σ : global_env_ext).
  Context `{checker_flags}.

  Lemma red1_context :
    ∀ Γ t u π,
      red1 Σ (Γ ,,, stack_context π) t u →
      red1 Σ Γ (zip (t, π)) (zip (u, π)).

  Corollary red_context :
    ∀ Γ t u π,
      red Σ (Γ ,,, stack_context π) t u →
      red Σ Γ (zip (t, π)) (zip (u, π)).

  Lemma zipc_inj :
    ∀ u v π, zipc u π = zipc v π → u = v.

  Definition isStackApp π :=
    match π with
    | App _ _ ⇒ true
    | _ ⇒ false
    end.

  Lemma isStackApp_false_appstack :
    ∀ l π,
      isStackApp (appstack l π) = false →
      l = [].

  Definition zipx (Γ : context) (t : term) (π : stack) : term :=
    it_mkLambda_or_LetIn Γ (zipc t π).

  Fixpoint context_position Γ : position :=
    match Γ with
    | [] ⇒ []
    | {| decl_name := na ; decl_body := None ; decl_type := A |} :: Γ ⇒
      context_position Γ ++ [ lam_tm ]
    | {| decl_name := na ; decl_body := Some b ; decl_type := A |} :: Γ ⇒
      context_position Γ ++ [ let_in ]
    end.

  Lemma context_position_atpos :
    ∀ Γ t, atpos (it_mkLambda_or_LetIn Γ t) (context_position Γ) = t.

  Lemma context_position_valid :
    ∀ Γ t, validpos (it_mkLambda_or_LetIn Γ t) (context_position Γ).

  Lemma positionR_context_position_inv :
    ∀ Γ p q,
      positionR (context_position Γ ++ p) (context_position Γ ++ q) →
      positionR p q.

  Definition xposition Γ π : position :=
    context_position Γ ++ stack_position π.

  Lemma xposition_atpos :
    ∀ Γ t π, atpos (zipx Γ t π) (xposition Γ π) = t.

  Lemma xposition_valid :
    ∀ Γ t π, validpos (zipx Γ t π) (xposition Γ π).

  Lemma positionR_xposition_inv :
    ∀ Γ ρ1 ρ2,
      positionR (xposition Γ ρ1) (xposition Γ ρ2) →
      positionR (stack_position ρ1) (stack_position ρ2).

  Definition xpos Γ t π : pos (zipx Γ t π) :=
    exist (xposition Γ π) (xposition_valid Γ t π).

  Lemma positionR_stack_pos_xpos :
    ∀ Γ π1 π2,
      positionR (stack_position π1) (stack_position π2) →
      positionR (xposition Γ π1) (xposition Γ π2).

  Definition zipp t π :=
    let '(args, ρ) := decompose_stack π in
    mkApps t args.

  Fixpoint stack_cat (ρ θ : stack) : stack :=
    match ρ with
    | Empty ⇒ θ
    | App u ρ ⇒ App u (stack_cat ρ θ)
    | Fix f n args ρ ⇒ Fix f n args (stack_cat ρ θ)
    | CoFix f n args ρ ⇒ CoFix f n args (stack_cat ρ θ)
    | Case indn p brs ρ ⇒ Case indn p brs (stack_cat ρ θ)
    | Proj p ρ ⇒ Proj p (stack_cat ρ θ)
    | Prod_l na B ρ ⇒ Prod_l na B (stack_cat ρ θ)
    | Prod_r na A ρ ⇒ Prod_r na A (stack_cat ρ θ)
    | Lambda_ty na u ρ ⇒ Lambda_ty na u (stack_cat ρ θ)
    | Lambda_tm na A ρ ⇒ Lambda_tm na A (stack_cat ρ θ)
    | coApp u ρ ⇒ coApp u (stack_cat ρ θ)
    end.

  Notation "ρ +++ θ" := (stack_cat ρ θ) (at level 20).

  Lemma stack_cat_appstack :
    ∀ args ρ,
      appstack args ε +++ ρ = appstack args ρ.

  Lemma decompose_stack_twice :
    ∀ π args ρ,
      decompose_stack π = (args, ρ) →
      decompose_stack ρ = ([], ρ).

  Lemma zipc_stack_cat :
    ∀ t π ρ,
      zipc t (π +++ ρ) = zipc (zipc t π) ρ.

  Lemma stack_cat_empty :
    ∀ ρ, ρ +++ ε = ρ.

  Lemma stack_position_stack_cat :
    ∀ π ρ,
      stack_position (ρ +++ π) =
      stack_position π ++ stack_position ρ.

  Lemma stack_context_stack_cat :
    ∀ π ρ,
      stack_context (ρ +++ π) = stack_context π ,,, stack_context ρ.

  Lemma red1_zipp :
    ∀ Γ t u π,
      red1 Σ Γ t u →
      red1 Σ Γ (zipp t π) (zipp u π).

  Lemma red_zipp :
    ∀ Γ t u π,
      red Σ Γ t u →
      red Σ Γ (zipp t π) (zipp u π).

  Definition zippx t π :=
    let '(args, ρ) := decompose_stack π in
    it_mkLambda_or_LetIn (stack_context ρ) (mkApps t args).


  Lemma red1_zippx :
    ∀ Γ t u π,
      red1 Σ (Γ ,,, stack_context π) t u →
      red1 Σ Γ (zippx t π) (zippx u π).

  Corollary red_zippx :
    ∀ Γ t u π,
      red Σ (Γ ,,, stack_context π) t u →
      red Σ Γ (zippx t π) (zippx u π).

End Stacks.

Notation "ρ +++ θ" := (stack_cat ρ θ) (at level 20).