File PCF.CBV

Require Import Nat Bool List.

From PCF Require Export Terms.

Values


Inductive value : form → Prop :=
  | v_abs :
      ∀ t,
        is_closed (f_abs t) →
        value (f_abs t)

  | v_star :
      value (f_star)
  | v_nat :
      ∀ n,
        value (f_nat n)

  | v_pair : ∀ t s,
      value t →
      value s →
      value (f_pair t s)

  | v_inl : ∀ t,
        value t →
        value (f_inl t)
  | v_inr : ∀ t,
        value t →
        value (f_inr t).

Big-Step Call-by-Value


Inductive bigCBV : form → form → Prop :=
  | bigCBV_value :
      ∀ v,
        value v →
        bigCBV v v
  
Beta reduction
  | bigCBV_app :
      ∀ p p' q q' r,
        bigCBV p (f_abs p') →
        bigCBV q q' →
        bigCBV (subst p' 0 q') r →
        bigCBV (f_app p q) r

  | bigCBV_pair :
      ∀ p r1 q r2,
        bigCBV p r1 →
        bigCBV q r2 →
        bigCBV (f_pair p q) (f_pair r1 r2)
  | bigCBV_fst :
      ∀ p r1 r2,
        bigCBV p (f_pair r1 r2) →
        bigCBV (f_fst p) r1
  | bigCBV_snd :
      ∀ p r1 r2,
        bigCBV p (f_pair r1 r2) →
        bigCBV (f_snd p) r2

  | bigCBV_case_inl :
      ∀ b b' p r q,
        bigCBV b (f_inl b') →
        bigCBV (subst p 0 b') r →
        bigCBV (f_case b p q) r
  | bigCBV_case_inr :
      ∀ b b' p r q,
        bigCBV b (f_inr b') →
        bigCBV (subst q 0 b') r →
        bigCBV (f_case b p q) r

  | bigCBV_fix :
      ∀ f g A B r,
        bigCBV f (f_abs g) →
        bigCBV (subst g 0 (f_abs (f_app (f_app (f_fix (ty_func A B)) f) (f_var 0)))) r →
        bigCBV (f_app (f_fix (ty_func A B)) f) r

  
I wanted to remove the following two rules, but I wasn't able to proove them with the other rules. In addition, I'm currently not convinced, that they are solvable because of binding issues.
  | bigCBV_ite_true :
      ∀ b p r q,
        bigCBV b (f_bool true) →
        bigCBV p r →
        bigCBV (f_ite b p q) r
  | bigCBV_ite_false :
      ∀ b p r q,
        bigCBV b (f_bool false) →
        bigCBV q r →
        bigCBV (f_ite b p q) r

  | bigCBV_le :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = (n1 <=? n2) →
        bigCBV (f_le p q) (f_bool m)
  | bigCBV_lt :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = (n1 <? n2) →
        bigCBV (f_lt p q) (f_bool m)

  | bigCBV_add :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = n1 + n2 →
        bigCBV (f_add p q) (f_nat m)
  | bigCBV_sub :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = n1 - n2 →
        bigCBV (f_sub p q) (f_nat m)
  | bigCBV_mul :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = n1 × n2 →
        bigCBV (f_mul p q) (f_nat m)
  | bigCBV_div :
      ∀ n1 n2 m p q,
        bigCBV p (f_nat n1) →
        bigCBV q (f_nat n2) →
        m = n1 / n2 →
        bigCBV (f_div p q) (f_nat m).

Theorem bigCBV_reduces_to_value :
  ∀ p v,
    bigCBV p v →
    value v.
Proof.
  induction 1 as
  [v H1
  |p p' q q' r H1 IH1 H2 IH2 H3 IH3

  |p r1 q r2 H1 IH1 H2 IH2
  |p r1 r2 H1 IH1
  |p r1 r2 H1 IH1

  |b b' p r q H1 IH1 H2 IH2
  |b b' p r q H1 IH1 H2 IH2

  |f g A B r H1 IH1 H2 IH2

  |b p r q H1 IH1 H2 IH2
  |b p r q H1 IH1 H2 IH2

  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3

  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3
  ];
  eauto using bigCBV, value; inversion IH1; eauto; destruct m; constructor; constructor.
Qed.

Theorem bigCBV_refl_bool :
  ∀ b,
    bigCBV (f_bool b) (f_bool b).
Proof.
  intros [|]; do 3 constructor.
Qed.

Module Faculty.

  Import Terms.Faculty.

  Theorem pcf_fac_reduces_to_fac :
    ∀ n,
      bigCBV (f_app (f_abs pcf_fac) (f_nat n)) (f_nat (fac n)).
  Proof.
    intros n.
    eapply bigCBV_app.
    -
      apply bigCBV_value; constructor; reflexivity.
    -
      apply bigCBV_value; constructor; reflexivity.
    -
      induction n as [|n' IH].
      +
        eapply bigCBV_app.
        ×
          fold subst.
          eapply bigCBV_fix.
          --
             apply bigCBV_value; constructor; reflexivity.
          --
             apply bigCBV_value; constructor; reflexivity.
        ×
          cbn.
          apply bigCBV_value; constructor; reflexivity.
        ×
          fold subst.
          repeat rewrite subst_f_ite.
          apply bigCBV_ite_true.
          --
             eapply bigCBV_le.
             ++
                apply bigCBV_value; constructor; reflexivity.
             ++
                apply bigCBV_value; constructor; reflexivity.
             ++
                reflexivity.
          --
             apply bigCBV_value; constructor; reflexivity.
      +
        eapply bigCBV_app.
        ×
          eapply bigCBV_fix.
          --
             apply bigCBV_value; constructor; reflexivity.
          --
             apply bigCBV_value; constructor; reflexivity.
        ×
          apply bigCBV_value; constructor; reflexivity.
        ×
          destruct n' as [|n''].
          --
             repeat rewrite subst_f_ite.
             apply bigCBV_ite_true.
             ++
                eapply bigCBV_le.
                **
                   apply bigCBV_value; constructor; reflexivity.
                **
                   apply bigCBV_value; constructor; reflexivity.
                **
                   reflexivity.
             ++
                apply bigCBV_value; constructor; reflexivity.
          --
             repeat rewrite subst_f_ite.
             apply bigCBV_ite_false.
             ++
                eapply bigCBV_le.
                **
                   apply bigCBV_value; constructor; reflexivity.
                **
                   apply bigCBV_value; constructor; reflexivity.
                **
                   reflexivity.
            ++
               eapply bigCBV_mul.
                **
                   apply bigCBV_value; constructor; reflexivity.
                **
                   eapply bigCBV_app.
                   ---
                       apply bigCBV_value; constructor; reflexivity.
                   ---
                       eapply bigCBV_sub.
                       +++
                           apply bigCBV_value; constructor; reflexivity.
                       +++
                           apply bigCBV_value; constructor; reflexivity.
                       +++
                           reflexivity.
                   ---
                       apply IH.
                **
                   reflexivity.
  Qed.

End Faculty.