File PCF.Terms

From PCF Require Export Contexts Formulas.

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_le :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_le t s) ty_bool
  | f_deriv_lt :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_lt t s) ty_bool

  | f_deriv_add :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_add t s) ty_nat
  | f_deriv_sub :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_sub t s) ty_nat
  | 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_div :
      ∀ c t s,
        f_deriv c t ty_nat →
        f_deriv c s ty_nat →
        f_deriv c (f_div t s) ty_nat.

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

Properties of type derivation


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
  |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
  |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.

Derivation of defined formulas


Theorem f_deriv_bool :
  ∀ c b,
    f_deriv c (f_bool b) ty_bool.
Proof.
  intros c [|];
      do 2 constructor.
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.

Some Examples


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.

The Faculty function in PCF


Module Faculty.

  Fixpoint fac (n : nat) :=
    match n with
    | O ⇒ 1
    | S n' ⇒ n × fac n'
    end.

  Definition pcf_fac : form :=
    let b := f_le (f_var 0) (f_nat 1) in
    let m := f_mul (f_var 0) (f_app (f_var 1) (f_sub (f_var 0) (f_nat 1))) in
    let g := f_abs (f_abs (f_ite b (f_nat 1) m)) in
    let fixer := f_fix (ty_func ty_nat ty_nat) in
    f_app (f_app fixer g) (f_var 0).

  Theorem pcf_fac_type :
    {ty : type | f_deriv (cupdate cempty 0 ty_nat) pcf_fac ty}.
  Proof.
    eexists.
    eapply f_deriv_app.
    -
      eapply f_deriv_app.
      +
        apply f_deriv_fix.
      +
        apply f_deriv_abs.
        apply f_deriv_abs.
        apply f_deriv_ite.
        ×
          apply f_deriv_le.
          --
             apply f_deriv_var.
             reflexivity.
          --
             apply f_deriv_nat.
        ×
          apply f_deriv_nat.
        ×
          apply f_deriv_mul.
          --
             apply f_deriv_var.
             reflexivity.
          --
             eapply f_deriv_app.
             ++
                apply f_deriv_var.
                cbn.
                reflexivity.
             ++
                apply f_deriv_sub.
                **
                   apply f_deriv_var.
                   reflexivity.
                **
                   apply f_deriv_nat.
    -
      apply f_deriv_var.
      reflexivity.
  Defined.

  Compute proj1_sig pcf_fac_type.

End Faculty.

The Maybe Monad: FX = X + 1


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.