Project

Namespaces

Public Vars

latte-nats.rec

The recursion theorem for natural numbers, together with its complete (somewhat non-trivial) formal proof.

nat-fixpoint-elem

(nat-fixpoint-elem [x T] [f (==> T T)])
(prel/rel-elem (nat-fixpoint-rel x f) (nat-recur-prop-rel x f))

Theorem: The least (relational) fixpoint is … least.

nat-fixpoint-fun

(nat-fixpoint-fun [x T] [f (==> T T)])
(rel/relfun (nat-fixpoint-rel x f) (nat-fixpoint-functional x f))

Definition: The (type-theoretic) function corresponding to the least (relational) fixpoint.

nat-fixpoint-fun-prop

(nat-fixpoint-fun-prop [x T] [f (==> T T)])
((nat-recur-prop x f) (nat-fixpoint-fun x f))

Theorem: The least relational fixpoint as a total function satisfies the recursion theorem.

nat-fixpoint-functional

(nat-fixpoint-functional [x T] [f (==> T T)])
(rel/functional (nat-fixpoint-rel x f))

Theorem: The least (relational) fixpoint is functional, which is one important ingredient of the proof of the recursion theorem.

nat-fixpoint-prop

(nat-fixpoint-prop [x T] [f (==> T T)])
(forall
 [R (rel nat T)]
 (==>
  (prel/rel-elem R (nat-recur-prop-rel x f))
  (rel/subrel (nat-fixpoint-rel x f) R)))

Theorem: The main property of the least (relational) fixpoint nat-fixpoint-rel.

nat-fixpoint-rel

(nat-fixpoint-rel [x T] [f (==> T T)])
(prel/rintersections (nat-recur-prop-rel x f))

Definition: The relational definition of the least fixed-point for (primitive) recursive functions on natural numbers.

nat-fixpoint-rel-ex

(nat-fixpoint-rel-ex [x T] [f (==> T T)])
(forall [n nat] (exists [y T] ((nat-fixpoint-rel x f) n y)))

Lemma: The existential part of the relational recursion theorem for natural numbers.

nat-fixpoint-rel-sing

(nat-fixpoint-rel-sing [x T] [f (==> T T)])
(forall [n nat] (q/single (lambda [y T] ((nat-fixpoint-rel x f) n y))))

Lemma: The singleness part of the relational recursion theorem for natural numbers.

nat-fixpoint-rel-sing-succ-aux

(nat-fixpoint-rel-sing-succ-aux [x T] [f (==> T T)])
(forall
 [n nat]
 (==>
  (forall
   [y1 y2 T]
   (==>
    ((nat-fixpoint-rel x f) n y1)
    ((nat-fixpoint-rel x f) n y2)
    (equal y1 y2)))
  (forall
   [y fy T]
   (==>
    ((nat-fixpoint-rel x f) n y)
    ((nat-fixpoint-rel x f) (succ n) fy)
    (equal fy (f y))))))

Lemma:

nat-fixpoint-rel-sing-zero-aux

(nat-fixpoint-rel-sing-zero-aux [x T] [f (==> T T)])
(forall [y T] (==> ((nat-fixpoint-rel x f) zero y) (equal x y)))

Lemma:

nat-fixpoint-rel-uniq

(nat-fixpoint-rel-uniq [x T] [f (==> T T)])
(forall [n nat] (q/unique (lambda [y T] ((nat-fixpoint-rel x f) n y))))

Lemma: The (relational) fixpoint characterization of recursion is unique. This is the core of the proof for the recursion theorem for natural integers.

nat-fixpoint-succ

(nat-fixpoint-succ [x T] [f (==> T T)])
(forall
 [n nat]
 (forall
  [y T]
  (==>
   ((nat-fixpoint-rel x f) n y)
   ((nat-fixpoint-rel x f) (succ n) (f y)))))

Lemma:

nat-fixpoint-zero

(nat-fixpoint-zero [x T] [f (==> T T)])
((nat-fixpoint-rel x f) zero x)

Lemma:

nat-rec-ex

(nat-rec-ex [x T] [f (==> T T)])
(exists [g (==> nat T)] ((nat-recur-prop x f) g))

Lemma:

nat-rec-single

(nat-rec-single [x T] [f (==> T T)])
(forall
 [g1 g2 (==> nat T)]
 (==>
  ((nat-recur-prop x f) g1)
  ((nat-recur-prop x f) g2)
  (equal g1 g2)))

Lemma:

nat-recur

(nat-recur [x T] [f (==> T T)])
(q/unique (nat-recur-prop x f))

Theorem: The recursion principle for natural numbers. cf. nat-recur-prop.

nat-recur-prop

(nat-recur-prop [x T] [f (==> T T)])
(lambda
 [g (==> nat T)]
 (and
  (equal (g zero) x)
  (forall [n nat] (equal (g (succ n)) (f (g n))))))

Definition: The property of the recursion principle for natural numbers.

nat-recur-prop-prop-rel

(nat-recur-prop-prop-rel [x T] [f (==> T T)] [g (==> nat T)])
(==> ((nat-recur-prop x f) g) ((nat-recur-prop-rel x f) (rel/funrel g)))

Theorem:

nat-recur-prop-rel

(nat-recur-prop-rel [x T] [f (==> T T)])
(lambda
 [R (rel nat T)]
 (and
  (R zero x)
  (forall [n nat] (forall [y T] (==> (R n y) (R (succ n) (f y)))))))

Definition: A relational variant of the recursion principle nat-recur-prop.

nat-recur-prop-rel-prop

(nat-recur-prop-rel-prop [x T] [f (==> T T)] [g (==> nat T)])
(==> ((nat-recur-prop-rel x f) (rel/funrel g)) ((nat-recur-prop x f) g))

Theorem:

nat-recur-rel-prop-rel-prop

(nat-recur-rel-prop-rel-prop [x T] [f (==> T T)] [R (rel nat T)] [func (rel/functional R)])
(==>
 ((nat-recur-prop-rel x f) R)
 ((nat-recur-prop x f) (rel/relfun R func)))

Lemma: