File PCF.PCF
Require Import Nat Bool List.
Inductive type :=
| ty_nat : type
| ty_bool : type
| ty_unit : type
| ty_prod : 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_abs : nat → 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_abs n f1 ⇒ filter (fun x ⇒ negb (Nat.eqb x n)) (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 subst (f : form) (x : nat) (s : form) : form :=
match f with
| f_var n ⇒ if (Nat.eqb x n) then s else (f_var n)
| 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_abs n f1 ⇒ if (Nat.eqb x n) then f_abs n f1 else f_abs n (subst f1 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 deriv : context → form → type → Prop :=
| Var :
∀ x A c,
c x = Some A →
deriv c (f_var x) A
| ttI :
∀ c,
deriv c f_star ty_unit
| prodI :
∀ c t A s B,
deriv c t A →
deriv c s B →
deriv c (f_pair t s) (ty_prod A B)
| prodE1 :
∀ c t A B,
deriv c t (ty_prod A B) →
deriv c (f_fst t) A
| prodE2 :
∀ c t A B,
deriv c t (ty_prod A B) →
deriv c (f_snd t) B
| funcI :
∀ c x A t B,
deriv (cupdate c x A) t B →
deriv c (f_abs x t) (ty_func A B)
| funcE :
∀ c s A B t,
deriv c s (ty_func A B) →
deriv c t A →
deriv c (f_app s t) B
| const_nat :
∀ c n,
deriv c (f_nat n) ty_nat
| const_bool :
∀ c b,
deriv c (f_bool b) ty_bool
| Eq :
∀ c s A t,
deriv c s A →
deriv c t A →
(A = ty_nat ∨ A = ty_bool ∨ A = ty_unit) →
deriv c (f_eq s t) ty_bool
| If :
∀ c b s A t,
deriv c b ty_bool →
deriv c s A →
deriv c t A →
deriv c (f_ite b s t) A
| Fix :
∀ c A,
deriv c (f_fix A) (ty_func (ty_func A A) A)
| func_leq :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_leq t s) ty_bool
| func_mul :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_mul t s) ty_nat
| func_minus :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_minus t s) ty_nat.
Example deriv_ex_1 :
∀ c,
∃ A,
let f := f_pair (f_abs 0 (f_app (f_var 0) (f_nat 3))) (f_app (f_abs 42 (f_ite (f_var 42) (f_nat 42) (f_nat 1))) (f_eq (f_nat 3) (f_nat 3))) in
deriv c f A.
Proof.
intros c;
eexists;
apply prodI.
-
apply funcI.
eapply funcE.
+
apply Var.
reflexivity.
+
apply const_nat.
-
eapply funcE.
+
apply funcI.
apply If.
×
apply Var.
reflexivity.
×
apply const_nat.
×
apply const_nat.
+
eapply Eq.
×
apply const_nat.
×
apply const_nat.
×
left; reflexivity.
Unshelve.
constructor.
Qed.
Definition is_term (f : form) := ∃ c A, deriv c f A.
Inductive type :=
| ty_nat : type
| ty_bool : type
| ty_unit : type
| ty_prod : 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_abs : nat → 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_abs n f1 ⇒ filter (fun x ⇒ negb (Nat.eqb x n)) (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 subst (f : form) (x : nat) (s : form) : form :=
match f with
| f_var n ⇒ if (Nat.eqb x n) then s else (f_var n)
| 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_abs n f1 ⇒ if (Nat.eqb x n) then f_abs n f1 else f_abs n (subst f1 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 deriv : context → form → type → Prop :=
| Var :
∀ x A c,
c x = Some A →
deriv c (f_var x) A
| ttI :
∀ c,
deriv c f_star ty_unit
| prodI :
∀ c t A s B,
deriv c t A →
deriv c s B →
deriv c (f_pair t s) (ty_prod A B)
| prodE1 :
∀ c t A B,
deriv c t (ty_prod A B) →
deriv c (f_fst t) A
| prodE2 :
∀ c t A B,
deriv c t (ty_prod A B) →
deriv c (f_snd t) B
| funcI :
∀ c x A t B,
deriv (cupdate c x A) t B →
deriv c (f_abs x t) (ty_func A B)
| funcE :
∀ c s A B t,
deriv c s (ty_func A B) →
deriv c t A →
deriv c (f_app s t) B
| const_nat :
∀ c n,
deriv c (f_nat n) ty_nat
| const_bool :
∀ c b,
deriv c (f_bool b) ty_bool
| Eq :
∀ c s A t,
deriv c s A →
deriv c t A →
(A = ty_nat ∨ A = ty_bool ∨ A = ty_unit) →
deriv c (f_eq s t) ty_bool
| If :
∀ c b s A t,
deriv c b ty_bool →
deriv c s A →
deriv c t A →
deriv c (f_ite b s t) A
| Fix :
∀ c A,
deriv c (f_fix A) (ty_func (ty_func A A) A)
| func_leq :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_leq t s) ty_bool
| func_mul :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_mul t s) ty_nat
| func_minus :
∀ c t s,
deriv c t ty_nat →
deriv c s ty_nat →
deriv c (f_minus t s) ty_nat.
Example deriv_ex_1 :
∀ c,
∃ A,
let f := f_pair (f_abs 0 (f_app (f_var 0) (f_nat 3))) (f_app (f_abs 42 (f_ite (f_var 42) (f_nat 42) (f_nat 1))) (f_eq (f_nat 3) (f_nat 3))) in
deriv c f A.
Proof.
intros c;
eexists;
apply prodI.
-
apply funcI.
eapply funcE.
+
apply Var.
reflexivity.
+
apply const_nat.
-
eapply funcE.
+
apply funcI.
apply If.
×
apply Var.
reflexivity.
×
apply const_nat.
×
apply const_nat.
+
eapply Eq.
×
apply const_nat.
×
apply const_nat.
×
left; reflexivity.
Unshelve.
constructor.
Qed.
Definition is_term (f : form) := ∃ c A, deriv c f A.