From PCF Require Export Requirements Types.

Definition context := nat → option type.

Definition cempty : context := fun _ ⇒ None.

Definition cupdate (c : context) (x : nat) (ty : type) : context := fun n ⇒ if x =? n then Some ty else c n.

Definition clift (k i : nat) (c : context) : context :=
  fun x ⇒
  if x <? k then c x
  else if x <? k + i then None
  else c (x - i).

Lemma cupdate_clift_bound :
  ∀ k i c T x,
    x < k →
    cupdate (clift k i c) k T x = c x.
Proof.
  intros k i c T x P1.
  unfold cupdate.
  assert (P2 : k ≠ x). { lia. }
  apply eqb_neq in P2 as B2.
  rewrite B2.
  unfold clift.
  apply ltb_lt in P1 as B1.
  rewrite B1.
  reflexivity.
Qed.

Lemma cupdate_clift_free :
  ∀ k i c T x,
    k ≤ x →
    cupdate (clift k (S i) c) k T (x + (S i)) = c x.
Proof.
  intros k i c T x P1.
  apply leb_le in P1 as B1.
  unfold cupdate.
  assert (P2 : k ≠ x + S i). { lia. }
  apply eqb_neq in P2 as B2.
  rewrite B2.
  unfold clift.
  assert (P3 : ¬ x + S i < k). { lia. }
  apply ltb_nlt in P3 as B3.
  rewrite B3.
  assert (P4 : ¬ x + S i < k + S i). { lia. }
  apply ltb_nlt in P4 as B4.
  rewrite B4.
  f_equal.
  lia.
Qed.

Lemma clift_cupdate :
  ∀ c k i T x,
    clift k i (cupdate c k T) x = cupdate (clift k i c) (k + i) T x.
Proof.
  intros c k i T x.
  unfold clift,cupdate.
  destruct (x <? k) eqn:B1.
  -
    apply ltb_lt in B1 as P1.
    assert (P2 : k ≠ x). lia.
    apply eqb_neq in P2 as B2.
    rewrite B2.
    assert (P3 : k + i ≠ x). lia.
    apply eqb_neq in P3 as B3.
    rewrite B3.
    reflexivity.
  -
    apply ltb_nlt in B1 as P1.
    destruct (x <? k + i) eqn:B2.
    +
      apply ltb_lt in B2 as P2.
      assert (P3 : k + i ≠ x). lia.
      apply eqb_neq in P3 as B3.
      rewrite B3.
      reflexivity.
    +
      apply ltb_nlt in B2 as P2.
      destruct (k =? x - i) eqn:B3.
      ×
        apply eqb_eq in B3 as P3.
        assert (P4 : k + i = x). lia.
        apply eqb_eq in P4 as B4.
        rewrite B4.
        reflexivity.
      ×
        apply eqb_neq in B3 as P3.
        assert (P4 : k + i ≠ x). lia.
        apply eqb_neq in P4 as B4.
        rewrite B4.
        reflexivity.
Qed.