File PCF.PCF
Inductive type :=
| ty_nat : type
| ty_bool : type
| ty_unit : type
| ty_prod : type → type → type
| ty_sum : type → type → type
| ty_func : type → type → type.
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.
Inductive form :=
| f_var : nat → form
| f_nat : nat → form
| f_bool : bool → form
| f_star : 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_abs : form → form
| f_app : form → form → form
| f_eq : form → form → form
| f_ite : form → form → form → form
| f_fix : type → form
| f_leq : form → form → form
| f_mul : form → form → form
| f_minus : form → form → form.
Fixpoint occ (f : form) : list nat :=
match f with
| f_var n ⇒ n :: nil
| f_nat n ⇒ nil
| f_bool b ⇒ nil
| f_star ⇒ nil
| f_pair f1 f2 ⇒ occ f1 ++ occ f2
| f_fst f1 ⇒ occ f1
| f_snd f1 ⇒ occ f1
| f_case f1 f2 f3 ⇒ occ f1 ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ f2)) ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ f3))
| f_inl f1 ⇒ occ f1
| f_inr f1 ⇒ occ f1
| f_abs f1 ⇒ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ f1))
| f_app f1 f2 ⇒ occ f1 ++ occ f2
| f_eq f1 f2 ⇒ occ f1 ++ occ f2
| f_ite f1 f2 f3 ⇒ occ f1 ++ occ f2 ++ occ f3
| f_fix a ⇒ nil
| f_leq f1 f2 ⇒ occ f1 ++ occ f2
| f_mul f1 f2 ⇒ occ f1 ++ occ f2
| f_minus f1 f2 ⇒ occ f1 ++ occ f2
end.
Definition is_closed (f : form) : Prop := occ f = nil.
Fixpoint lift (k i : nat) (t : form) : form :=
match t with
| f_var n ⇒ if Nat.ltb n k then f_var n else f_var (n + i)
| f_nat n ⇒ f_nat n
| f_bool b ⇒ f_bool b
| f_star ⇒ f_star
| 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_abs f1 ⇒ f_abs (lift (k + 1) i f1)
| f_app f1 f2 ⇒ f_app (lift k i f1) (lift k i f2)
| f_eq f1 f2 ⇒ f_eq (lift k i f1) (lift k i f2)
| f_ite f1 f2 f3 ⇒ f_ite (lift k i f1) (lift k i f2) (lift k i f3)
| f_fix a ⇒ f_fix a
| 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.
Definition clift (k i : nat) (c : context) : context :=
fun x ⇒
c (if Nat.ltb x k then x else x - i).
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_nat n ⇒ f_nat n
| f_bool b ⇒ f_bool b
| f_star ⇒ f_star
| 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_abs f1 ⇒ f_abs (subst f1 (S x) s)
| f_app f1 f2 ⇒ f_app (subst f1 x s) (subst f2 x s)
| f_eq f1 f2 ⇒ f_eq (subst f1 x s) (subst f2 x s)
| f_ite f1 f2 f3 ⇒ f_ite (subst f1 x s) (subst f2 x s) (subst f3 x s)
| f_fix a ⇒ f_fix a
| 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.
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_star :
∀ c,
f_deriv c f_star ty_unit
| 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_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_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_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_nat :
∀ c n,
f_deriv c (f_nat n) ty_nat
| f_deriv_bool :
∀ c b,
f_deriv c (f_bool b) ty_bool
| f_deriv_eq :
∀ c s A t,
f_deriv c s A →
f_deriv c t A →
(A = ty_nat ∨ A = ty_bool ∨ A = ty_unit) →
f_deriv c (f_eq s t) ty_bool
| 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
| f_deriv_fix :
∀ c A,
f_deriv c (f_fix A) (ty_func (ty_func A A) A)
| 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.
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.
×
left; reflexivity.
Unshelve.
constructor.
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.