Library ModelNat

In this file, we build a consistency model of the Calculus of Constructions extended with natural numbers and the usual recursor (CC+NAT). It is a follow-up of file ModelZF.

Require Import ZF ZFnats ZFrelations.
Require Import basic ModelZF.
Import CCM BuildModel.
Import T J R.

Nat and its constructors

Definition Zero : term.
left; exists (fun _ => zero).
Defined.

Definition Succ : term.
left; exists (fun _ => lam N succ).
Defined.

Definition Nat : term.
left; exists (fun _ => N).
Defined.

Typing rules of constructors

Lemma typ_0 : ∀ e, typ e Zero Nat.

Lemma typ_S : ∀ e, typ e Succ (Prod Nat (lift 1 Nat)).

Lemma typ_N : ∀ e, typ e Nat kind.

The recursor

Recursor

Definition NatRec (f g n:term) : term.
left; exists (fun i => natrec (int f i) (fun n y => app (app (int g i) n) y) (int n i)).
Defined.

Typing rule of the eliminator

Lemma typ_Nrect : ∀ e n f g P,
  typ e n Nat ->
  typ e f (App P Zero) ->
  typ e g (Prod Nat (Prod (App (lift 1 P) (Ref 0))
              (App (lift 2 P) (App Succ (Ref 1))))) ->
  typ e (NatRec f g n) (App P n).

Lemma eq_typ_NatRec e f f' g g' n n' :
  eq_typ e f f' ->
  eq_typ e g g' ->
  eq_typ e n n' ->
  eq_typ e (NatRec f g n) (NatRec f' g' n').

iota-reduction

Lemma NatRec_eq_0 e f g :
  eq_typ e (NatRec f g Zero) f.

Lemma NatRec_eq_S e f g n :
  typ e n Nat ->
  eq_typ e (NatRec f g (App Succ n)) (App (App g n) (NatRec f g n)).