The Coq mailing list

[Seul Baek <seulkeebaek AT gmail.com>]

(* I'm learning about primitive recursive functions and trying to formalize some of the material in Coq. Specifically, I want to prove that any section of a primitive recursive function is also primitive recursive, because this property comes in handy for proving other theorems. *)   

(* Before getting to the problem, here are the definitions used to state the theorem. Everything from this point to PRF_proper is just definition of primitive recursive function in Coq. You can skip it if unnecessary. *)

Require Import NaryFunctions.

Definition nfun (n : nat) : Type :=

nat ^^ n --> nat.

(* Although not strictly necessary, I decided to have some fun with combinators... *)

(* \ a b c => a c b, the cardinal. *)

Definition cardinal {X Y Z : Type }

(f : X -> Y -> Z) : Y -> X -> Z :=

fun y x => f x y. 

(* \ a b => a b b, the warbler. *)

Definition warbler {X Y : Type }

(a : X -> X -> Y) (b : X ) : Y :=

a b b.

(* \ a b => b a, the thrush. *)

Definition thrush {X Y : Type }

(a : X) (b : X -> Y ) : Y := b a.

(* \ a b => b a, the kestrel. *)

Definition kestrel {X Y : Type }

(a : X) (b : Y ) : X := a.

(* Constants. *)

Fixpoint const (n m : nat) : nfun n

:= match n return nfun n with

| O    => m

| S n' => kestrel (const n' m)

end.

(* Projections. *)

Fixpoint proj (n m : nat) : nfun n 

:= match n return nfun n with

| O    => O

| S n' => 

  match m with

  | O    => const (S n') O

  | S O  => const n'   

  | S m' => kestrel (proj n' m')

  end  

end.

(* The following 2 definitions are used to define composition. *)

Fixpoint delay {X Y Z : Type} {n : nat} :

(Z -> X ^^ n --> (Z -> Y)) 

-> X ^^ n --> (Z -> Y) :=

match n return

(Z -> X ^^ n --> (Z -> Y)) 

-> X ^^ n --> (Z -> Y) 

with

| O    => warbler 

| S n' => fun f g 

       => delay (fun z => f z g)

end.

Fixpoint dist {X Y : Type} 

{Z : Type} {n : nat} :

(X ^^ n --> Y) -> (Z -> X) ^^ n --> (Z -> Y) :=

match n return 

(X ^^ n --> Y) -> (Z -> X) ^^ n --> (Z -> Y)

with

| O    => kestrel

| S n' => fun f g => delay (fun z 

       => dist (f (g z)))

end.

(* Composition. *)

Fixpoint comp {X Y Z : Type} (n m : nat) 

(f : X ^^ n --> Y) : 

(Z ^^ m --> X) ^^ n --> (Z ^^ m --> Y) :=

match m return

(Z ^^ m --> X) ^^ n --> (Z ^^ m --> Y) 

with 

| O    => f

| S m' => dist (comp n m' f)

end.

(* Used for defining primitive recursion. *)

Fixpoint stitch {X Y Z: Type} {n : nat} :

(X ^^ n --> Y) -> (Y -> X ^^ n --> Z)  

-> (X ^^ n --> Z) :=

match n return

(X ^^ n --> Y) -> (Y -> X ^^ n --> Z)  

-> (X ^^ n --> Z) 

with

| O    => thrush

| S n' => fun f g x 

       => stitch (f x) (cardinal g x) 

end.

(* Primitive recursion. *)

Fixpoint rec {n : nat} (g : nfun n)

(h : nfun (S (S n))) (m : nat) :

nfun n :=

match m with

| O    => g 

| S m' => stitch (rec g h m') (cardinal h m')   

end.

(* PRF, the predicate which asserts that a certain function over natural numbers is primitive recursive. It is indexed by an extra counter m due to limitations regarding strict positivity. An n-ary function f is primitive recursive in the usual sense if PRF 0 n f. If PRF m n f /\ m <> 0, it means that m more functions (which are n-ary and primitive recursive) need to be applied to f to make it properly primitive recursive. *)

Inductive PRF : forall (n m : nat), 

(nfun m ^^ n --> nfun m) -> Prop :=

| PRF_S : PRF 0 1 S

| PRF_cst : forall n m, PRF 0 n (const n m)

| PRF_prj : forall n m, 0 <> m 

  -> m <= n -> PRF 0 n (proj n m)

| PRF_cps : forall n m 

  (f: nfun m), 

  PRF 0 m f -> 

  PRF m n (comp m n f)

| PRF_app : forall n m f g,

  PRF (S m) n f -> PRF 0 n g

  -> PRF m n (f g) 

| PRF_rec : forall n f g,

  PRF 0 n f -> PRF 0 (S (S n)) g

  -> PRF 0 (S n) (rec f g).

Hint Constructors PRF.

(* A shorthand which hides the m index. *)

Definition PRF_proper {n : nat} 

(f : nfun n) : Prop :=

PRF 0 n f.

(* Now the problematic part. I want to prove that for any (n+1)-ary primitive recursive function f, its n-ary section (f x) is also primitive recursive, for all x. Intuitively this is obvious, because the composition f(x, proj^n_2, proj^n_3, ... proj^n_n) is equivalent to (f x) and clearly primitive recursive. But I want to prove this in Coq, and I found this to be unexpectedly difficult. *) 

Lemma PRF_section : forall (n x : nat )

(f : nfun (S n)),

PRF 0 (S n) f -> PRF 0 n (f x). 

(* I first tried proving this by induction on n, which didn't work out because having

forall x f, PRF 0 (S n) f -> PRF 0 n (f x). 

in the context is not very helpful for proving

forall x f, PRF 0 (S (S n)) f -> PRF 0 (S n) (f x). 

If there is a proof by induction on n, that would be the most straightforward solution (please let me know if you find one), but I couldn't see how to do it. The second idea I had was to perform an induction on the proposition PRF 0 (S n) f. So I tried *) 

intros. 

generalize dependent x.

induction H.

(* but Coq tells me that the induction is impossible because it is ill-typed. Is there any way around this? *)