Library SN_NAT
In this file, we build a strong normalization model of the
Calculus of Constructions extended with natural numbers and
the usual recursor.
Require Import basic Can Sat SATnat SN_CC_Real.
Require Import ZF ZFcoc ZFind_nat.
Module Lc:=Lambda.
Import CCSN SN.
Definition Zero : trm.
left; exists (fun _ => ZERO) (fun _ => ZE).
Defined.
Definition Succ : trm.
left; exists (fun _ => lam (mkTY NAT cNAT) SUCC) (fun _ => SU).
Defined.
Definition Nat : trm.
left; exists (fun _ => mkTY NAT cNAT) (fun _ => Lc.K).
Defined.
Lemma ElNat_eq i : El (int i Nat) == NAT.
Lemma RealNat_eq i n :
n ∈ NAT ->
eqSAT (Real (int i Nat) n) (cNAT n).
Notation "[ x , t ] \real A" := (x ∈ El A /\ inSAT t (Real A x)) (at level 60).
Lemma realNat_def : ∀ i n t,
[n,t] \real int i Nat <-> n ∈ NAT /\ inSAT t (cNAT n).
Typing rules of constructors
Lemma typ_0 : ∀ e, typ e Zero Nat.
Lemma sn_SU : Lc.sn SU.
Lemma typ_S : ∀ e, typ e Succ (Prod Nat (lift 1 Nat)).
Lemma typ_N : ∀ e, typ e Nat kind.
Require Import ZFord.
Require Import ZFrepl.
Lemma sn_SU : Lc.sn SU.
Lemma typ_S : ∀ e, typ e Succ (Prod Nat (lift 1 Nat)).
Lemma typ_N : ∀ e, typ e Nat kind.
Require Import ZFord.
Require Import ZFrepl.
Definition NREC f g n y :=
∀ P,
Proper (eq_set ==> eq_set ==> iff) P ->
P ZERO f -> (∀ m x, P m x -> P (SUCC m) (g m x)) -> P n y.
Lemma NREC_inv : ∀ f g n y,
morph2 g ->
NREC f g n y ->
NREC f g n y /\
(n == ZERO -> y == f) /\
(∀ m, n == SUCC m -> exists2 z, NREC f g m z & y == g m z).
Lemma NREC_choice_0 : ∀ f g, uchoice_pred (NREC f g ZERO).
Lemma NREC_choice : ∀ f g n,
n ∈ NAT ->
morph2 g ->
uchoice_pred (NREC f g n).
Recursor at the level of sets
Definition NATREC f g n := uchoice (NREC f g n).
Instance NATREC_morph :
Proper (eq_set ==> (eq_set ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) NATREC.
Qed.
Lemma NATREC_def : ∀ f g n,
morph2 g -> n ∈ NAT -> NREC f g n (NATREC f g n).
Lemma NATREC_0 : ∀ f g, NATREC f g ZERO == f.
Lemma NATREC_S : ∀ f g n, morph2 g -> n ∈ NAT ->
NATREC f g (SUCC n) == g n (NATREC f g n).
Lemma NATREC_typ P f g n :
morph1 P ->
morph2 g ->
n ∈ NAT ->
f ∈ P ZERO ->
(∀ k h, k ∈ NAT -> h ∈ P k -> g k h ∈ P (SUCC k)) ->
NATREC f g n ∈ P n.
Instance NATREC_morph :
Proper (eq_set ==> (eq_set ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) NATREC.
Qed.
Lemma NATREC_def : ∀ f g n,
morph2 g -> n ∈ NAT -> NREC f g n (NATREC f g n).
Lemma NATREC_0 : ∀ f g, NATREC f g ZERO == f.
Lemma NATREC_S : ∀ f g n, morph2 g -> n ∈ NAT ->
NATREC f g (SUCC n) == g n (NATREC f g n).
Lemma NATREC_typ P f g n :
morph1 P ->
morph2 g ->
n ∈ NAT ->
f ∈ P ZERO ->
(∀ k h, k ∈ NAT -> h ∈ P k -> g k h ∈ P (SUCC k)) ->
NATREC f g n ∈ P n.
Recursor
Definition NatRec (f g n:trm) : trm.
left; exists (fun i => NATREC (int i f) (fun n y => app (app (int i g) n) y) (int i n))
(fun j => Lc.App2 (tm j n) (tm j f) (tm j g)).
Defined.
left; exists (fun i => NATREC (int i f) (fun n y => app (app (int i g) n) y) (int i n))
(fun j => Lc.App2 (tm j n) (tm j f) (tm j g)).
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).
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).
beta-reduction on the realizers simulates the reduction of
the eliminator