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.
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.
Lemma typ_S : ∀ e, typ e Succ (Prod Nat (lift 1 Nat)).
Lemma typ_N : ∀ e, typ e Nat kind.
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.
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').
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