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 : 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 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_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_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 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 A t B,
deriv (cupdate (clift 0 1 c) 0 A) t B →
deriv c (f_abs 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 (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
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 : 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 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_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_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 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 A t B,
deriv (cupdate (clift 0 1 c) 0 A) t B →
deriv c (f_abs 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 (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
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.