File PCF.CBV
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_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_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 | deriv (cupdate cempty 0 ty_nat) pcf_fac ty}.
Proof.
eexists.
eapply funcE.
-
eapply funcE.
+
apply Fix.
+
apply funcI.
apply funcI.
apply If.
×
apply func_leq.
--
apply Var.
reflexivity.
--
apply const_nat.
×
apply const_nat.
×
apply func_mul.
--
apply Var.
reflexivity.
--
eapply funcE.
++
apply Var.
cbn.
reflexivity.
++
apply func_minus.
**
apply Var.
reflexivity.
**
apply const_nat.
-
apply 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.