Require Import Coq.Lists.List.
From PCF2.Autosubst Require Import unscoped pcf_2.
Require Import PCF2.pcf_2_system.
Set Default Goal Selector "!".

Inductive pctxt :=
| pctxtHole: pctxt
| pctxtTrny1: pctxt -> tm -> tm -> pctxt
| pctxtTrny2: tm -> pctxt -> tm -> pctxt
| pctxtTrny3: tm -> tm -> pctxt -> pctxt
| pctxtLam: pctxt -> pctxt
| pctxtAppL: pctxt -> tm -> pctxt
| pctxtAppR: tm -> pctxt -> pctxt.

Hint Constructors pctxt : core.

Fixpoint fill (ctxt: pctxt) (trm: tm) :=
match ctxt with
| pctxtHole => trm
| pctxtTrny1 ctxt trm2 trm3 => trny (fill ctxt trm) trm2 trm3
| pctxtTrny2 trm1 ctxt trm3 => trny trm1 (fill ctxt trm) trm3
| pctxtTrny3 trm1 trm2 ctxt => trny trm1 trm2 (fill ctxt trm)
| pctxtLam ctxt => lam (fill ctxt trm)
| pctxtAppL ctxt trm' => app (fill ctxt trm) trm'
| pctxtAppR trm' ctxt => app trm' (fill ctxt trm)
end.

Fixpoint comp c1 c2 :=
match c1 with
| pctxtHole => c2
| pctxtTrny1 ctxt trm2 trm3 => pctxtTrny1 (comp ctxt c2) trm2 trm3
| pctxtTrny2 trm1 ctxt trm3 => pctxtTrny2 trm1 (comp ctxt c2) trm3
| pctxtTrny3 trm1 trm2 ctxt => pctxtTrny3 trm1 trm2 (comp ctxt c2)
| pctxtLam ctxt => pctxtLam (comp ctxt c2)
| pctxtAppL ctxt trm' => pctxtAppL (comp ctxt c2) trm'
| pctxtAppR trm' ctxt => pctxtAppR trm' (comp ctxt c2)
end.

Inductive ctxt_typed: pctxt -> context -> ty -> context -> ty -> Prop :=
| pctxt_typed_Hole Γ A: ctxt_typed pctxtHole Γ A Γ A
| pctxt_typed_Trnry1 ctxt trm2 trm3 Γ A Γ': ctxt_typed ctxt Γ A Γ' Base -> typed Γ' trm2 Base -> typed Γ' trm3 Base -> ctxt_typed (pctxtTrny1 ctxt trm2 trm3) Γ A Γ' Base
| pctxt_typed_Trnry2 trm1 ctxt trm3 Γ A Γ': typed Γ' trm1 Base -> ctxt_typed ctxt Γ A Γ' Base -> typed Γ' trm3 Base -> ctxt_typed (pctxtTrny2 trm1 ctxt trm3) Γ A Γ' Base
| pctxt_typed_Trnry3 trm1 trm2 ctxt Γ A Γ': typed Γ' trm1 Base -> typed Γ' trm2 Base -> ctxt_typed ctxt Γ A Γ' Base -> ctxt_typed (pctxtTrny3 trm1 trm2 ctxt) Γ A Γ' Base
| pctxt_typed_Lam ctxt T Γ A Γ' A': ctxt_typed ctxt Γ A (cons T Γ') A' -> ctxt_typed (pctxtLam ctxt) Γ A Γ' (Fun T A')
| pctxt_typed_AppL ctxt trm Γ Γ' A B C: ctxt_typed ctxt Γ A Γ' (Fun B C) -> typed Γ' trm B -> ctxt_typed (pctxtAppL ctxt trm) Γ A Γ' C
| pctxt_typed_AppR trm ctxt Γ Γ' A B C: ctxt_typed ctxt Γ A Γ' B -> typed Γ' trm (Fun B C) -> ctxt_typed (pctxtAppR trm ctxt) Γ A Γ' C.

Notation "C [ Γ , A ] : Γ' , A' " := (ctxt_typed C Γ A Γ' A') (at level 50, Γ, A, Γ', A' at next level).

Hint Constructors ctxt_typed : core.

Lemma fill_type Γ A Γ' A' C e:
    Γ ⊢ e: A -> C [Γ, A] : Γ', A' -> typed Γ' (fill C e) A'.
Proof.
    intros typed_e typed_c. induction typed_c; cbn; firstorder.
    all: econstructor; eauto.
Qed.

Lemma ctxt_comp_typed Γ Γ' Γ'' A A' A'' C1 C2:
    C1 [ Γ, A ]: Γ', A' -> C2 [Γ'', A'']: Γ, A -> (comp C1 C2) [Γ'', A'']: Γ', A'.
Proof.
    intros typed_c1 typed_c2. induction typed_c1; cbn; firstorder.
    all: econstructor; eauto.
Qed.

Lemma ctxt_comp_fill C1 C2 s:
    fill (comp C1 C2) s = fill C1 (fill C2 s).
Proof.
    induction C1; cbn; firstorder.
    all: now rewrite IHC1.
Qed.

Lemma fill_step C s t:
    s ≻* t -> (fill C s) ≻* (fill C t).
Proof.
    intros steps. induction C; cbn; eauto.
    all: now rewrite IHC.
Qed.