headlines pcf

src/PCF.v

+(** * Programming Computable Functions (PCF) *)
+
 Require Import Nat Bool List.
 
+(** ** Types *)
+
 Inductive type :=
   | ty_nat : type
   | ty_bool : type
@@ -8,6 +12,8 @@ Inductive type :=
   | ty_sum : type -> type -> type
   | ty_func : type -> type -> type.
 
+(** ** Contexts *)
+
 Definition context := nat -> option type.
 
 Definition cempty : context := fun _ => None.
@@ -24,6 +30,8 @@ Proof.
     apply c; exact n.
 Defined.
 
+(** ** Formulas *)
+
 Inductive form :=
   | f_var : nat -> form
   | f_nat : nat -> form
@@ -45,6 +53,8 @@ Inductive form :=
   | f_mul : form -> form -> form
   | f_minus : form -> form -> form.
 
+(** *** Operations and Properties *)
+
 Fixpoint occ (f : form) : list nat :=
   match f with
   | f_var n => n :: nil
@@ -125,6 +135,8 @@ Fixpoint subst (f : form) (x : nat) (s : form) : form :=
   | f_minus f1 f2 => f_minus (subst f1 x s) (subst f2 x s)
   end.
 
+(** ** Derivable terms in context *)
+
 Inductive f_deriv : context -> form -> type -> Prop :=
   | f_deriv_var : 
       forall x A c,