File PCF.CBV
Require Import Nat Bool List.
From PCF Require Import PCF.
Inductive value : form → Prop :=
| v_bool :
∀ b,
value (f_bool b)
| v_nat :
∀ n,
value (f_nat n)
| v_star :
value (f_star)
| v_pair : ∀ t s,
is_term t →
is_term s →
value t →
value s →
value (f_pair t s)
| v_inl : ∀ t,
is_term t →
value t →
value (f_inl t)
| v_inr : ∀ t,
is_term t →
value t →
value (f_inr t)
| v_func :
∀ t,
is_term t →
is_closed (f_abs t) →
value (f_abs t).
Inductive bigCBV : form → form → Prop :=
| bigCBV_refl_nat :
∀ n,
bigCBV (f_nat n) (f_nat n)
| bigCBV_refl_bool :
∀ b,
bigCBV (f_bool b) (f_bool b)
| bigCBV_refl_star :
bigCBV f_star f_star
| bigCBV_refl_pair :
∀ t s,
bigCBV (f_pair t s) (f_pair t s)
| bigCBV_refl_abs :
∀ p,
bigCBV (f_abs p) (f_abs p)
| bigCBV_beta :
∀ 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_sum_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_sum_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_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_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
| bigCBV_leq :
∀ n1 n2 m p q,
bigCBV p (f_nat n1) →
bigCBV q (f_nat n2) →
m = Nat.leb n1 n2 →
bigCBV (f_leq p q) (f_bool 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_minus :
∀ n1 n2 m p q,
bigCBV p (f_nat n1) →
bigCBV q (f_nat n2) →
m = n1 - n2 →
bigCBV (f_minus p q) (f_nat m).
Definition pcf_fac : form :=
let b := f_leq (f_var 0) (f_nat 1) in
let m := f_mul (f_var 0) (f_app (f_var 1) (f_minus (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_leq.
--
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_minus.
**
apply f_deriv_var.
reflexivity.
**
apply f_deriv_nat.
-
apply f_deriv_var.
reflexivity.
Defined.
Compute proj1_sig pcf_fac_type.
Fixpoint fac (n : nat) :=
match n with
| O ⇒ 1
| S n' ⇒ n × fac n'
end.
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_beta.
-
apply bigCBV_refl_abs.
-
apply bigCBV_refl_nat.
-
induction n as [|n' IH].
+
eapply bigCBV_beta.
×
eapply bigCBV_fix.
--
apply bigCBV_refl_abs.
--
apply bigCBV_refl_abs.
×
cbn.
apply bigCBV_refl_nat.
×
apply bigCBV_ite_true.
--
eapply bigCBV_leq.
++
apply bigCBV_refl_nat.
++
apply bigCBV_refl_nat.
++
reflexivity.
--
apply bigCBV_refl_nat.
+
eapply bigCBV_beta.
×
eapply bigCBV_fix.
--
apply bigCBV_refl_abs.
--
apply bigCBV_refl_abs.
×
apply bigCBV_refl_nat.
×
simpl in ×.
destruct n' as [|n''].
--
apply bigCBV_ite_true.
++
eapply bigCBV_leq.
**
apply bigCBV_refl_nat.
**
apply bigCBV_refl_nat.
**
reflexivity.
++
apply bigCBV_refl_nat.
--
apply bigCBV_ite_false.
++
eapply bigCBV_leq.
**
apply bigCBV_refl_nat.
**
apply bigCBV_refl_nat.
**
reflexivity.
++
eapply bigCBV_mul.
**
apply bigCBV_refl_nat.
**
simpl in ×.
eapply bigCBV_beta.
---
apply bigCBV_refl_abs.
---
eapply bigCBV_minus.
+++
apply bigCBV_refl_nat.
+++
apply bigCBV_refl_nat.
+++
reflexivity.
---
apply IH.
**
reflexivity.
Qed.