File PCF.PCF

Programming Computable Functions (PCF)


Require Import PeanoNat Bool List Lia.
Import PeanoNat.Nat.

Types


Inductive type :=
  | ty_func : type → type → type

  | ty_unit : type
  | ty_nat : type

  | ty_prod : type → type → type
  | ty_sum : type → type → type.

More types


Definition ty_bool := ty_sum ty_unit ty_unit.

Contexts


Definition context := nat → option type.

Definition cempty : context := fun _ ⇒ None.

Definition cupdate (c : context) (x : nat) (ty : type) : context.
Proof.
  repeat red.
  repeat red in c.
  intros n.
  destruct (Nat.eqb x n).
  -
    exact (Some ty).
  -
    apply c; exact n.
Defined.

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 PeanoNat.Nat.eqb_neq in P2 as B2.
  rewrite B2.
  unfold clift.
  apply PeanoNat.Nat.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 PeanoNat.Nat.leb_le in P1 as B1.
  unfold cupdate.
  assert (P2 : k ≠ x + S i). { lia. }
  apply PeanoNat.Nat.eqb_neq in P2 as B2.
  rewrite B2.
  unfold clift.
  assert (P3 : ¬ x + S i < k). { lia. }
  apply PeanoNat.Nat.ltb_nlt in P3 as B3.
  rewrite B3.
  assert (P4 : ¬ x + S i < k + S i). { lia. }
  apply PeanoNat.Nat.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.

Formulas


Inductive form :=
  | f_var : nat → form
  | f_abs : form → form
  | f_app : form → form → form

  | f_star : form
  | f_nat : nat → form

  | f_pair : form → form → form
  | f_fst : form → form
  | f_snd : form → form

  | f_case : form → form → form → form
  | f_inl : form → form
  | f_inr : form → form

  | f_fix : type → form

  | f_eq : form → form → form
  | f_leq : form → form → form
  | f_mul : form → form → form
  | f_minus : form → form → form.

Operations and Properties


Fixpoint occ_list (f : form) : list nat :=
  match f with
  | f_var n ⇒ n :: nil
  | f_abs f1 ⇒ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f1))
  | f_app f1 f2 ⇒ occ_list f1 ++ occ_list f2

  | f_star ⇒ nil
  | f_nat n ⇒ nil

  | f_pair f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_fst f1 ⇒ occ_list f1
  | f_snd f1 ⇒ occ_list f1

  | f_case f1 f2 f3 ⇒ occ_list f1 ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f2)) ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f3))
  | f_inl f1 ⇒ occ_list f1
  | f_inr f1 ⇒ occ_list f1

  | f_fix a ⇒ nil

  | f_eq f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_leq f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_mul f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_minus f1 f2 ⇒ occ_list f1 ++ occ_list f2
  end.

Definition occ' (f : form) (x : nat) : Prop := In x (occ_list f).

Fixpoint occ (f : form) (x : nat) : Prop :=
  match f with
  | f_var n ⇒ n = x
  | f_abs f1 ⇒ occ f1 (S x)
  | f_app f1 f2 ⇒ occ f1 x ∨ occ f2 x

  | f_star ⇒ False
  | f_nat n ⇒ False

  | f_pair f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_fst f1 ⇒ occ f1 x
  | f_snd f1 ⇒ occ f1 x
      
  | f_case f1 f2 f3 ⇒ occ f1 x ∨ occ f2 (S x) ∨ occ f3 (S x)
  | f_inl f1 ⇒ occ f1 x
  | f_inr f1 ⇒ occ f1 x

  | f_fix a ⇒ False

  | f_eq f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_leq f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_mul f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_minus f1 f2 ⇒ occ f1 x ∨ occ f2 x
  end.

Lemma occ'_occ :
  ∀ f x,
    occ' f x →
    occ f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros x H1;
  try exact H1;
  try eauto;
  try (apply in_app_or in H1; destruct H1 as [H1|H1]; [left; eapply IH1 | right; eapply IH2]; easy).
  -
f_var
    destruct H1 as [H1|H1]; easy.
  -
f_abs
    apply IH1.
    apply in_map_iff in H1 as [n [H1 H2]].
    apply filter_In in H2 as [H2 H3].
    symmetry in H1; subst x.
    destruct n as [|n']; easy.
  -
f_case
    repeat apply in_app_or in H1 as [H1|H1].
    +
      left; eapply IH1; apply H1.
    +
      right; left; apply IH2.
      apply in_map_iff in H1 as [n [H1 H2]].
      apply filter_In in H2 as [H2 H3].
      symmetry in H1; subst x.
      destruct n as [|n']; easy.
    +
      right; right; apply IH3.
      apply in_map_iff in H1 as [n [H1 H2]].
      apply filter_In in H2 as [H2 H3].
      symmetry in H1; subst x.
      destruct n as [|n']; easy.
Qed.

Lemma occ_occ' :
  ∀ f x,
    occ f x →
    occ' f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros x H1;
  try eauto;
  try (apply in_or_app; destruct H1 as [H1|H1]; [left; apply IH1|right; apply IH2]; exact H1).
  -
f_var
    left; exact H1.
  -
f_abs
      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
  -
f_case
    cbn.
    apply in_or_app.
    repeat destruct H1 as [H1|H1].
    +
      left; apply IH1; exact H1.
    +
      right; apply in_or_app; left.
      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
    +
      right; apply in_or_app; right.
      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
Qed.

Definition is_closed (f : form) : Prop := occ_list f = nil.

Fixpoint lift (k i : nat) (t : form) : form :=
  match t with
  | f_var n ⇒ if n <? k then f_var n else f_var (n + i)
  | f_abs f1 ⇒ f_abs (lift (k + 1) i f1)
  | f_app f1 f2 ⇒ f_app (lift k i f1) (lift k i f2)

  | f_star ⇒ f_star
  | f_nat n ⇒ f_nat n

  | f_pair f1 f2 ⇒ f_pair (lift k i f1) (lift k i f2)
  | f_fst f1 ⇒ f_fst (lift k i f1)
  | f_snd f1 ⇒ f_snd (lift k i f1)

  | f_case f1 f2 f3 ⇒ f_case (lift k i f1) (lift (k + 1) i f2) (lift (k + 1) i f3)
  | f_inl f1 ⇒ f_inl (lift k i f1)
  | f_inr f1 ⇒ f_inr (lift k i f1)

  | f_fix a ⇒ f_fix a

  | f_eq f1 f2 ⇒ f_eq (lift k i f1) (lift k i f2)
  | f_leq f1 f2 ⇒ f_leq (lift k i f1) (lift k i f2)
  | f_mul f1 f2 ⇒ f_mul (lift k i f1) (lift k i f2)
  | f_minus f1 f2 ⇒ f_minus (lift k i f1) (lift k i f2)
  end.

Example lift_k_0 :
  ∀ f k,
    lift k 0 f = f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intro k;
  cbn;
  f_equal;
  eauto.
  -
f_var
    destruct k as [|k].
    f_equal; lia.
    destruct (n <=? k);
    f_equal;
    lia.
Qed.

Lemma lift_additive :
  ∀ f k i1 i2,
  lift k i1 (lift k i2 f) = lift k (i1 + i2) f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k i1 i2;
  cbn;
  try (f_equal; try rewrite IH1; try rewrite IH2; try rewrite IH3; reflexivity).
  -
    destruct k as [|k].
    cbn.
    f_equal; lia.
    destruct (n <=? k) eqn:H1.
    cbn.
    rewrite H1.
    reflexivity.
    cbn.
    destruct (n + i2 <=? k) eqn:H2.
    apply PeanoNat.Nat.leb_le in H2.
    apply PeanoNat.Nat.leb_nle in H1.
    lia.
    f_equal; lia.
Qed.

Lemma lift_comp :
  ∀ f k1 k2 i,
  lift (k1 + k2) i (lift k2 k1 f) = lift k2 (k1 + i) f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k1 k2 i;
  eauto;
  try (cbn; try rewrite <- PeanoNat.Nat.add_assoc; try rewrite IH1; try rewrite IH2; try rewrite IH3; try lia; reflexivity).
  -
f_var
    simpl lift.
    destruct (n <? k2) eqn:B1.
    +
      apply PeanoNat.Nat.ltb_lt in B1 as P1.
      simpl lift.
      assert (P2 : n < k1 + k2). { lia. }
      apply PeanoNat.Nat.ltb_lt in P2 as B2.
      rewrite B2.
      reflexivity.
    +
      apply PeanoNat.Nat.ltb_nlt in B1 as P1.
      simpl lift.
      assert (P2 : ¬ n + k1 < k1 + k2). { lia. }
      apply PeanoNat.Nat.ltb_nlt in P2 as B2.
      rewrite B2.
      f_equal; lia.
Qed.

Lemma occ_lift_k_1 :
  ∀ f k x,
    k ≤ x →
    occ (lift k 1 f) (S x) →
    occ f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x H1 H2;
  eauto;
  try (destruct H2; [left; apply (IH1 k)|right; apply (IH2 k)]; easy).
  -
f_var
    cbn in ×.
    destruct k as [|k].
    +
      cbn in H2.
      lia.
    +
      destruct (n <=? k) eqn:H3.
      ×
        cbn in H2.
        Search ((_ <=? _) = true).
        apply PeanoNat.Nat.leb_le in H3.
        lia.
      ×
        cbn in H2.
        lia.
  -
f_abs
    apply (IH1 (k + 1)); [lia|exact H2].
  -
f_case
    repeat destruct H2 as [H2|H2].
    +
      left; apply (IH1 k); assumption.
    +
      right; left; apply (IH2 (k + 1)); [lia|exact H2].
    +
      right; right; apply (IH3 (k + 1)); [lia|exact H2].
Qed.

Lemma occ_lift_reverse_k_1 :
  ∀ f k x,
  k ≤ x →
  occ f x →
  occ (lift k 1 f) (S x).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x H1 H2;
  try exact H2;
  try (apply IH1; assumption);
  try (destruct H2; [left; apply IH1 | right; apply IH2]; easy).
  -
f_var
    cbn in ×.
    subst n.
    destruct k as [|k].
    +
      cbn; lia.
    +
      destruct (x <=? k) eqn:H2.
      ×
        apply PeanoNat.Nat.leb_le in H2.
        lia.
      ×
        cbn; lia.
  -
f_abs
    apply IH1; [lia|exact H2].
  -
f_case
    repeat destruct H2 as [H2|H2].
    +
      left; apply IH1; assumption.
    +
      right; left; apply IH2; [lia|exact H2].
    +
      right; right; apply IH3; [lia|exact H2].
Qed.

Lemma negative_occ_lift :
  ∀ f k i x,
  k ≤ x →
  x < k + i →
  ¬ (occ (lift k i f) x).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k i x H1 H2 H3;
  try exact H3;
  try (apply (IH1 k i x); assumption);
  try (destruct H3 as [H3|H3]; [apply (IH1 k i x) | apply (IH2 k i x)]; easy).
  -
f_var
    unfold lift in H3.
    destruct (n <? k) eqn:H4;
    cbn in H3.
    +
      apply PeanoNat.Nat.ltb_lt in H4.
      lia.
    +
      Search ((_ <? _) = false).
      apply PeanoNat.Nat.ltb_nlt in H4.
      symmetry in H3.
      lia.
  -
f_abs
    apply (IH1 (k + 1) i (S x)); try lia; easy.
  -
f_case
    repeat destruct H3 as [H3|H3].
    +
      apply (IH1 k i x); assumption.
    +
      apply (IH2 (k + 1) i (S x)); try lia; easy.
    +
      apply (IH3 (k + 1) i (S x)); try lia; easy.
Qed.

Fixpoint subst (f : form) (x : nat) (s : form) : form :=
  match f with
  | f_var n ⇒
      if n <? x
      then f_var n
      else if x <? n
      then f_var (n - 1)
      else lift 0 x s
  | f_abs f1 ⇒ f_abs (subst f1 (S x) s)
  | f_app f1 f2 ⇒ f_app (subst f1 x s) (subst f2 x s)

  | f_star ⇒ f_star
  | f_nat n ⇒ f_nat n

  | f_pair f1 f2 ⇒ f_pair (subst f1 x s) (subst f2 x s)
  | f_fst f1 ⇒ f_fst (subst f1 x s)
  | f_snd f1 ⇒ f_snd (subst f1 x s)

  | f_case f1 f2 f3 ⇒ f_case (subst f1 x s) (subst f2 (S x) s) (subst f3 (S x) s)
  | f_inl f1 ⇒ f_inl (subst f1 x s)
  | f_inr f1 ⇒ f_inr (subst f1 x s)

  | f_fix a ⇒ f_fix a

  | f_eq f1 f2 ⇒ f_eq (subst f1 x s) (subst f2 x s)
  | f_leq f1 f2 ⇒ f_leq (subst f1 x s) (subst f2 x s)
  | f_mul f1 f2 ⇒ f_mul (subst f1 x s) (subst f2 x s)
  | f_minus f1 f2 ⇒ f_minus (subst f1 x s) (subst f2 x s)
  end.

More formulas

f_bool
Definition f_bool b :=
  match b with
  | true ⇒ f_inl
  | false ⇒ f_inr
  end f_star.

Theorem occ_f_bool :
  ∀ b x,
    ¬ occ (f_bool b) x.
Proof.
  intros b x H1;
  destruct b;
  contradiction.
Qed.

Theorem lift_f_bool :
  ∀ k i b,
    lift k i (f_bool b) = f_bool b.
Proof.
  intros ? ? b;
  destruct b;
  reflexivity.
Qed.

Theorem subst_f_bool :
  ∀ x s b,
    subst (f_bool b) x s = f_bool b.
Proof.
  intros ? ? b;
  destruct b;
  reflexivity.
Qed.

f_ite

Definition f_ite f1 f2 f3 :=
  f_case f1 (lift 0 1 f2) (lift 0 1 f3).

Theorem occ_f_ite :
  ∀ f1 f2 f3 x,
  occ (f_ite f1 f2 f3) x ↔ occ f1 x ∨ occ f2 x ∨ occ f3 x.
Proof.
  intros f1 f2 f3 x.
  split;
  intros H1;
  repeat destruct H1 as [H1|H1].
  -
    left; exact H1.
  -
    right; left; apply occ_lift_k_1 in H1; [exact H1|lia].
  -
    right; right; apply occ_lift_k_1 in H1; [exact H1|lia].
  -
    left; exact H1.
  -
    right; left; apply occ_lift_reverse_k_1 with (k := 0); [lia|exact H1].
  -
    right; right; apply occ_lift_reverse_k_1 with (k := 0); [lia|exact H1].
Qed.

Lemma lift_f_ite_helper :
  ∀ f k1 k2 i,
    k2 ≤ k1 →
    lift (k1 + 1) i (lift k2 1 f) = lift k2 1 (lift k1 i f).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k1 k2 i H0;
  try (cbn; try rewrite (IH1 _ _ _ H0); try rewrite (IH2 _ _ _ H0); reflexivity).
  -
f_var
    cbn.
    destruct k2 as [|k2],k1 as [|k1].
    cbn.
    destruct (n + 1 <=? 0) eqn:H1.
    apply PeanoNat.Nat.leb_le in H1.
    lia.
    f_equal; lia.
    destruct (n <=? k1) eqn:H1.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H2.
    reflexivity.
    apply PeanoNat.Nat.leb_le in H1.
    apply PeanoNat.Nat.leb_nle in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H2.
    apply PeanoNat.Nat.leb_nle in H1.
    apply PeanoNat.Nat.leb_le in H2.
    lia.
    f_equal; lia.
    destruct (n <=? k2) eqn:H1.
    cbn.
    destruct (n <=? 0) eqn:H2, (n + i <=? k2) eqn:H3.
    apply PeanoNat.Nat.leb_le in H1,H2,H3.
    lia.
    apply PeanoNat.Nat.leb_le in H1,H2.
    apply PeanoNat.Nat.leb_nle in H3.
    lia.
    apply PeanoNat.Nat.leb_le in H1,H3.
    apply PeanoNat.Nat.leb_nle in H2.
    lia.
    apply PeanoNat.Nat.leb_le in H1.
    apply PeanoNat.Nat.leb_nle in H2,H3.
    lia.
    lia.
    destruct (n <=? k2) eqn:H1, (n <=? k1) eqn:H2.
    cbn.
    destruct (n <=? k1 + 1) eqn:H3, (n <=? k2) eqn:H4.
    reflexivity.
    discriminate.
    apply PeanoNat.Nat.leb_le in H2.
    apply PeanoNat.Nat.leb_nle in H3.
    lia.
    discriminate.
    apply PeanoNat.Nat.leb_le in H1.
    apply PeanoNat.Nat.leb_nle in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H3, (n <=? k2) eqn:H4.
    discriminate.
    reflexivity.
    discriminate.
    apply PeanoNat.Nat.leb_nle in H4,H3.
    apply PeanoNat.Nat.leb_le in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H3;
    destruct (n + i <=? k2) eqn:H4.
    apply PeanoNat.Nat.leb_le in H3,H4.
    apply PeanoNat.Nat.leb_nle in H1,H2.
    lia.
    apply PeanoNat.Nat.leb_le in H3.
    apply PeanoNat.Nat.leb_nle in H1,H2,H4.
    lia.
    apply PeanoNat.Nat.leb_le in H4.
    apply PeanoNat.Nat.leb_nle in H1,H2,H3.
    lia.
    f_equal; lia.
  -
f_abs
    cbn.
    f_equal.
    apply IH1.
    lia.
  -
f_case
    cbn.
    f_equal.
    +
      apply IH1.
      exact H0.
    +
      apply IH2.
      lia.
    +
      apply IH3.
      lia.
Qed.

Theorem lift_f_ite :
  ∀ k i f1 f2 f3,
    lift k i (f_ite f1 f2 f3) = f_ite (lift k i f1) (lift k i f2) (lift k i f3).
Proof.
  intros k i f1 f2 f3.
  cbn.
  unfold f_ite.
  f_equal; apply lift_f_ite_helper; lia.
Qed.

Lemma subst_f_ite_helper :
  ∀ f k x s,
    k ≤ x →
    subst (lift k 1 f) (S x) s = lift k 1 (subst f x s).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x s H1;
  try (cbn; try rewrite IH1; try rewrite IH2; try rewrite IH3; try reflexivity; lia).
  -
f_var
    simpl lift at 1.
    simpl subst at 2.
    destruct (n <? k) eqn:B1;
    destruct (n <? x) eqn:B2.
    +
      apply PeanoNat.Nat.ltb_lt in B1 as P1,B2 as P2.
      simpl subst.
      simpl lift at 2.
      rewrite B1.
      destruct (n <? S x) eqn:B3.
      ×
        reflexivity.
      ×
        apply PeanoNat.Nat.ltb_nlt in B3; lia.
    +
      apply PeanoNat.Nat.ltb_lt in B1 as P1.
      apply PeanoNat.Nat.ltb_nlt in B2 as P2.
      lia.
    +
      apply PeanoNat.Nat.ltb_nlt in B1 as P1.
      apply PeanoNat.Nat.ltb_lt in B2 as P2.
      simpl subst.
      assert (P3 : n + 1 < S x). { lia. }
      apply PeanoNat.Nat.ltb_lt in P3 as B3.
      rewrite B3.
      simpl lift.
      rewrite B1.
      reflexivity.
    +
      apply PeanoNat.Nat.ltb_nlt in B1 as P1,B2 as P2.
      destruct (x <? n) eqn:B3.
      ×
        simpl subst.
        assert (P4 : ¬ n + 1 < S x). { lia. }
        apply PeanoNat.Nat.ltb_nlt in P4 as B4.
        rewrite B4.

        apply PeanoNat.Nat.ltb_lt in B3 as P3.
        assert (P5 : S x < n + 1). { lia. }
        apply PeanoNat.Nat.ltb_lt in P5 as B5.
        rewrite B5.
        simpl lift.
        assert (P6 : ¬ n - 1 < k). { lia. }
        apply PeanoNat.Nat.ltb_nlt in P6 as B6.
        rewrite B6.
        f_equal.
        lia.
      ×
        apply PeanoNat.Nat.ltb_nlt in B3 as P3.
        assert (H2 : x = n). { lia. }
        subst x.
        clear B2 P2 B3 P3.
        clear H1.
        simpl subst.
        assert (P2 : ¬ n + 1 < S n). { lia. }
        apply PeanoNat.Nat.ltb_nlt in P2 as B2.
        rewrite B2.
        assert (P3 : ¬ S n < n + 1). { lia. }
        apply PeanoNat.Nat.ltb_nlt in P3 as B3.
        rewrite B3.

        clear P2 B2 P3 B3.
        assert (P2 : k ≤ n). { lia. }
        clear B1 P1.

        assert (H1 : ∃ n', k + n' = n).
        {
          ∃ (n - k).
          lia.
        }
        destruct H1 as [n' H1].
        rewrite <- H1 at 2.
        rewrite <- lift_additive.
        rewrite <- (PeanoNat.Nat.add_0_r k) at 1.
        rewrite lift_comp.
        rewrite lift_additive.
        f_equal; lia.
Qed.

Theorem subst_f_ite :
  ∀ f1 f2 f3 x s,
    subst (f_ite f1 f2 f3) x s = f_ite (subst f1 x s) (subst f2 x s) (subst f3 x s).
Proof.
  intros f1 f2 f3 x s.
  cbn.
  unfold f_ite.
  f_equal; apply subst_f_ite_helper; lia.
Qed.

Derivable terms in context


Inductive f_deriv : context → form → type → Prop :=
  | f_deriv_var :
      ∀ x A c,
        c x = Some A →
        f_deriv c (f_var x) A
  | f_deriv_abs :
      ∀ c A t B,
        f_deriv (cupdate (clift 0 1 c) 0 A) t B →
        f_deriv c (f_abs t) (ty_func A B)
  | f_deriv_app :
      ∀ c s A B t,
        f_deriv c s (ty_func A B) →
        f_deriv c t A →
        f_deriv c (f_app s t) B

  | f_deriv_star :
      ∀ c,
        f_deriv c f_star ty_unit
  | f_deriv_nat :
      ∀ c n,
        f_deriv c (f_nat n) ty_nat

  | f_deriv_pair :
      ∀ c t A s B,
        f_deriv c t A →
        f_deriv c s B →
        f_deriv c (f_pair t s) (ty_prod A B)
  | f_deriv_fst :
      ∀ c t A B,
        f_deriv c t (ty_prod A B) →
        f_deriv c (f_fst t) A
  | f_deriv_snd :
      ∀ c t A B,
        f_deriv c t (ty_prod A B) →
        f_deriv c (f_snd t) B

  | f_deriv_case :
      ∀ c b A B p C q,
        f_deriv c b (ty_sum A B) →
        f_deriv (cupdate (clift 0 1 c) 0 A) p C →
        f_deriv (cupdate (clift 0 1 c) 0 B) q C →
        f_deriv c (f_case b p q) C
  | f_deriv_inl :
      ∀ c t A B,
        f_deriv c t A →
        f_deriv c (f_inl t) (ty_sum A B)
  | f_deriv_inr :
      ∀ c t A B,
        f_deriv c t B →
        f_deriv c (f_inr t) (ty_sum A B)

  | f_deriv_fix :
      ∀ c A,
        f_deriv c (f_fix A) (ty_func (ty_func A A) A)

  | f_deriv_eq :
      ∀ c s A t,
        f_deriv c s A →
        f_deriv c t A →
        (A = ty_unit ∨ A = ty_nat) →
        f_deriv c (f_eq s t) ty_bool
  | f_deriv_leq :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_leq t s) ty_bool
  | f_deriv_mul :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_mul t s) ty_nat
  | f_deriv_minus :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_minus t s) ty_nat.

Theorem f_deriv_bool :
  ∀ c b,
    f_deriv c (f_bool b) ty_bool.
Proof.
  intros c [|];
      do 2 constructor.
Qed.

Lemma f_deriv_weakening :
  ∀ c1 f T1,
    f_deriv c1 f T1 →
    ∀ c2,
      (∀ x T1, c1 x = Some T1 → c2 x = Some T1) →
      f_deriv c2 f T1.
Proof.
  induction 1 as
  [x1 T1 c1 H1
  |c1 T1 t T2 H1 IH1
  |c1 s T1 T2 t H1 IH1 H2 IH2

  |c1
  |c1 n

  |c1 t T1 s T2 H1 IH1 H2 IH2
  |c1 t T1 T2 H1 IH1
  |c1 t T1 T2 H1 IH1

  |c1 b T1 T2 p T3 q H1 IH1 H2 IH2 H3 IH3
  |c1 t T1 T2 H1 IH1
  |c1 t T1 T2 H1 IH1

  |c1 T1
  
  |c1 s T1 t H1 IH1 H2 IH2 H3
  |c1 t s H1 IH1 H2 IH2
  |c1 t s H1 IH1 H2 IH2
  |c1 t s H1 IH1 H2 IH2
  ];
  intros c2 H4;
  eauto using f_deriv.
  -
f_deriv_abs
    constructor.
    apply IH1.
    intros x T3 H5.
    destruct x as [|x].
    +
      exact H5.
    +
      assert (H6 : S x = x + 1). lia.
      rewrite H6.
      erewrite <- H4.
      specialize cupdate_clift_free with (k := 0) (i := 0) (c := c2) (T := T1) (x := x) as H7.
      apply H7.
      lia.
      cbn in H5.
      rewrite sub_0_r in H5.
      exact H5.
  -
f_deriv_case
    econstructor.
    +
      apply IH1.
      exact H4.
    +
      apply IH2.
      intros x T4 H5.
      destruct x as [|x].
      ×
        exact H5.
      ×
        assert (H6 : S x = x + 1). lia.
        rewrite H6.
        erewrite <- H4.
        specialize cupdate_clift_free with (k := 0) (i := 0) (c := c2) (T := T1) (x := x) as H7.
        apply H7.
        lia.
        cbn in H5.
        rewrite sub_0_r in H5.
        exact H5.
    +
      apply IH3.
      intros x T4 H5.
      destruct x as [|x].
      ×
        exact H5.
      ×
        assert (H6 : S x = x + 1). lia.
        rewrite H6.
        erewrite <- H4.
        specialize cupdate_clift_free with (k := 0) (i := 0) (c := c2) (T := T2) (x := x) as H7.
        apply H7.
        lia.
        cbn in H5.
        rewrite sub_0_r in H5.
        exact H5.
Qed.

Lemma f_deriv_cupdate :
  ∀ c f T1,
    f_deriv c f T1 →
    ∀ v T2,
      c v = None →
      f_deriv (cupdate c v T2) f T1.
Proof.
  intros c f T1 H1 v T2 H2.
  apply f_deriv_weakening with (c1 := c).
  -
    exact H1.
  -
    intros x T3 H3.
    unfold cupdate.
    destruct (v =? x) eqn:B1.
    +
      apply eqb_eq in B1 as P1.
      subst v.
      rewrite H2 in H3.
      discriminate.
    +
      exact H3.
Qed.

Lemma f_deriv_lift :
  ∀ c f T,
    f_deriv c f T →
    ∀ k i,
      f_deriv (clift k i c) (lift k i f) T.
Proof.
  induction 1 as
  [x T1 c H1
  |c T1 t T2 H1 IH1
  |c s T1 T2 t H1 IH1 H2 IH2

  |c
  |c n

  |c t T1 s T2 H1 IH1 H2 IH2
  |c t T1 T2 H1 IH1
  |c t T1 T2 H1 IH1

  |c b T1 T2 p T3 q H1 IH1 H2 IH2 H3 IH3
  |c t T1 T2 H1 IH1
  |c t T1 T2 H1 IH1

  |c T1
  
  |c s T1 t H1 IH1 H2 IH2 H3
  |c t s H1 IH1 H2 IH2
  |c t s H1 IH1 H2 IH2
  |c t s H1 IH1 H2 IH2
  ];
  intros k i;
  eauto using f_deriv.
  -
f_deriv_var
    unfold lift.
    destruct (x <? k) eqn:B1; constructor.
    +
      unfold clift.
      rewrite B1.
      exact H1.
    +
      unfold clift.
      apply ltb_nlt in B1 as P1.
      assert (P2 : ¬ x + i < k). lia.
      apply ltb_nlt in P2 as B2.
      rewrite B2.
      assert (P3 : ¬ x + i < k + i). lia.
      apply ltb_nlt in P3 as B3.
      rewrite B3.
      rewrite <- H1.
      f_equal; lia.
  -
f_deriv_abs
    cbn.
    constructor.
    cbn.
    eapply f_deriv_weakening.
    +
      apply IH1.
    +
      intros x T3 H2.
      clear IH1 H1.
      unfold cupdate.
      destruct x as [|x].
      ×
        cbn.
        unfold clift in H2.
        assert (P1 : 0 < k + 1). lia.
        apply ltb_lt in P1 as B1.
        rewrite B1 in H2.
        clear P1 B1.
        unfold cupdate in H2.
        cbn in H2.
        exact H2.
      ×
        cbn.
        rewrite sub_0_r.
        unfold clift in H2.
        unfold clift.
        destruct (x <? k) eqn:B1.
        --
           apply ltb_lt in B1 as P1.
           assert (P2 : S x < k + 1). lia.
           apply ltb_lt in P2 as B2.
           rewrite B2 in H2.
           unfold cupdate in H2.
           cbn in H2.
           rewrite sub_0_r in H2.
           exact H2.
        --
           apply ltb_nlt in B1 as P1.
           assert (P2 : ¬ S x < k + 1). lia.
           apply ltb_nlt in P2 as B2.
           rewrite B2 in H2.
           clear P2 B2.

           destruct (x <? k + i) eqn:B2.
           ++
              apply ltb_lt in B2 as P2.
              assert (P3 : S x < k + 1 + i). lia.
              apply ltb_lt in P3 as B3.
              rewrite B3 in H2.
              exact H2.
           ++
              apply ltb_nlt in B2 as P2.
              assert (P3 : ¬ S x < k + 1 + i). lia.
              apply ltb_nlt in P3 as B3.
              rewrite B3 in H2.
              clear B3 P3.

              unfold cupdate in H2.
              destruct (0 =? S x - i) eqn:B3.
              **
                 apply eqb_eq in B3 as P3.
                 lia.
              **
                 apply eqb_neq in B3 as P3.
                 assert (P4 : ¬ S x - i < 0). lia.
                 apply ltb_nlt in P4 as B4.
                 rewrite B4 in H2.
                 assert (P5 : ¬ S x - i < 0 + 1). lia.
                 apply ltb_nlt in P5 as B5.
                 rewrite B5 in H2.
                 rewrite <- H2.
                 f_equal; lia.
  -
f_deriv_case
    cbn.
    econstructor.
    +
      apply IH1.
    +
      cbn.
      eapply f_deriv_weakening.
      ×
        apply IH2.
      ×
        intros x T4 H4.
        clear IH1 H1.
        unfold cupdate.
        destruct x as [|x].
        --
           cbn.
           unfold clift in H4.
           assert (P1 : 0 < k + 1). lia.
           apply ltb_lt in P1 as B1.
           rewrite B1 in H4.
           clear P1 B1.
           unfold cupdate in H4.
           cbn in H4.
           exact H4.
        --
           cbn.
           rewrite sub_0_r.
           unfold clift in H4.
           unfold clift.
           destruct (x <? k) eqn:B1.
           ++
              apply ltb_lt in B1 as P1.
              assert (P2 : S x < k + 1). lia.
              apply ltb_lt in P2 as B2.
              rewrite B2 in H4.
              unfold cupdate in H4.
              cbn in H4.
              rewrite sub_0_r in H4.
              exact H4.
           ++
              apply ltb_nlt in B1 as P1.
              assert (P2 : ¬ S x < k + 1). lia.
              apply ltb_nlt in P2 as B2.
              rewrite B2 in H4.
              clear P2 B2.

              destruct (x <? k + i) eqn:B2.
              **
                 apply ltb_lt in B2 as P2.
                 assert (P3 : S x < k + 1 + i). lia.
                 apply ltb_lt in P3 as B3.
                 rewrite B3 in H4.
                 exact H4.
              **
                 apply ltb_nlt in B2 as P2.
                 assert (P3 : ¬ S x < k + 1 + i). lia.
                 apply ltb_nlt in P3 as B3.
                 rewrite B3 in H4.
                 clear B3 P3.

                 unfold cupdate in H4.
                 destruct (0 =? S x - i) eqn:B3.
                 ---
                     apply eqb_eq in B3 as P3.
                     lia.
                 ---
                     apply eqb_neq in B3 as P3.
                     assert (P4 : ¬ S x - i < 0). lia.
                     apply ltb_nlt in P4 as B4.
                     rewrite B4 in H4.
                     assert (P5 : ¬ S x - i < 0 + 1). lia.
                     apply ltb_nlt in P5 as B5.
                     rewrite B5 in H4.
                     rewrite <- H4.
                     f_equal; lia.
    +
      cbn.
      eapply f_deriv_weakening.
      ×
        apply IH3.
      ×
        intros x T4 H4.
        clear IH1 H1.
        unfold cupdate.
        destruct x as [|x].
        --
           cbn.
           unfold clift in H4.
           assert (P1 : 0 < k + 1). lia.
           apply ltb_lt in P1 as B1.
           rewrite B1 in H4.
           clear P1 B1.
           unfold cupdate in H4.
           cbn in H4.
           exact H4.
        --
           cbn.
           rewrite sub_0_r.
           unfold clift in H4.
           unfold clift.
           destruct (x <? k) eqn:B1.
           ++
              apply ltb_lt in B1 as P1.
              assert (P2 : S x < k + 1). lia.
              apply ltb_lt in P2 as B2.
              rewrite B2 in H4.
              unfold cupdate in H4.
              cbn in H4.
              rewrite sub_0_r in H4.
              exact H4.
           ++
              apply ltb_nlt in B1 as P1.
              assert (P2 : ¬ S x < k + 1). lia.
              apply ltb_nlt in P2 as B2.
              rewrite B2 in H4.
              clear P2 B2.

              destruct (x <? k + i) eqn:B2.
              **
                 apply ltb_lt in B2 as P2.
                 assert (P3 : S x < k + 1 + i). lia.
                 apply ltb_lt in P3 as B3.
                 rewrite B3 in H4.
                 exact H4.
              **
                 apply ltb_nlt in B2 as P2.
                 assert (P3 : ¬ S x < k + 1 + i). lia.
                 apply ltb_nlt in P3 as B3.
                 rewrite B3 in H4.
                 clear B3 P3.

                 unfold cupdate in H4.
                 destruct (0 =? S x - i) eqn:B3.
                 ---
                     apply eqb_eq in B3 as P3.
                     lia.
                 ---
                     apply eqb_neq in B3 as P3.
                     assert (P4 : ¬ S x - i < 0). lia.
                     apply ltb_nlt in P4 as B4.
                     rewrite B4 in H4.
                     assert (P5 : ¬ S x - i < 0 + 1). lia.
                     apply ltb_nlt in P5 as B5.
                     rewrite B5 in H4.
                     rewrite <- H4.
                     f_equal; lia.
Qed.

Theorem f_deriv_ite :
  ∀ c b s A t,
    f_deriv c b ty_bool →
    f_deriv c s A →
    f_deriv c t A →
    f_deriv c (f_ite b s t) A.
Proof.
  econstructor;
  eauto using f_deriv_cupdate, f_deriv_lift.
Qed.

Example f_deriv_ex_1 :
  ∀ c,
    ∃ A,
      let f :=
        f_pair
        (f_abs (f_app (f_var 0) (f_nat 3)))
        (f_app (f_abs (f_ite (f_var 0) (f_nat 0) (f_nat 1))) (f_eq (f_nat 3) (f_nat 3)))
      in
      f_deriv c f A.
Proof.
  intros c;
  eexists;
  apply f_deriv_pair.
  -
    apply f_deriv_abs.
    eapply f_deriv_app.
    +
      apply f_deriv_var.
      reflexivity.
    +
      apply f_deriv_nat.
  -
    eapply f_deriv_app.
    +
      apply f_deriv_abs.
      apply f_deriv_ite.
      ×
        apply f_deriv_var.
        reflexivity.
      ×
        apply f_deriv_nat.
      ×
        apply f_deriv_nat.
    +
      eapply f_deriv_eq.
      ×
        apply f_deriv_nat.
      ×
        apply f_deriv_nat.
      ×
        right; reflexivity.
  Unshelve.
  auto using type.
Qed.

Example deriv_ex_2 :
  let c := cempty in
  let f1 := f_abs (f_case (f_var 0) (f_nat 42) (f_nat 43)) in
  let f2 := f_inl (f_nat 642) in
  let f := f_app f1 f2 in
  let ty := ty_nat in
  f_deriv c f ty.
Proof.
  eapply f_deriv_app.
  -
    apply f_deriv_abs.
    eapply f_deriv_case.
    +
      apply f_deriv_var.
      reflexivity.
    +
      apply f_deriv_nat.
    +
      apply f_deriv_nat.
  -
    apply f_deriv_inl.
    apply f_deriv_nat.
  Unshelve.
  exact ty_unit.
Qed.

Definition is_term (f : form) := ∃ c A, f_deriv c f A.

Module MaybeMonad.

  Let M := fun ty ⇒ ty_sum ty ty_unit.

  Definition f_return := f_inl.

  Definition f_do p q := f_case p q (f_inr (f_var 0)).

  Theorem ret :
    ∀ c t A,
      f_deriv c t A →
      f_deriv c (f_return t) (M A).
  Proof.
    eauto using f_deriv.
  Qed.

  Theorem bind :
    ∀ c p B q C,
      f_deriv c p (M B) →
      f_deriv (cupdate (clift 0 1 c) 0 B) q (M C) →
      f_deriv c (f_do p q) (M C).
  Proof.
    intros c p B q C H1 H2.
    unfold f_do.
    eapply f_deriv_case.
    -
      exact H1.
    -
      exact H2.
    -
      apply f_deriv_inr.
      apply f_deriv_var.
      unfold cupdate.
      reflexivity.
  Qed.

  Print Assumptions bind.
End MaybeMonad.