Library SN_CIC
Strong normalization of the model of CC+NAT in the type-based
termination presentation.
This is work in progress, several lemmas of this module are admitted.
Require Import List Bool Models.
Require SN_CC_Real.
Import ZFgrothendieck.
Import ZF ZFsum ZFnats ZFrelations ZFord ZFfix.
Require Import ZFfunext ZFfixrec ZFecc ZFind_nat.
Import SN_CC_Real.
Import SN_CC_Real.CCSN.
Import SN_CC_Real.SN.
Opaque Real.
Import Sat Sat.SatSet.
Lemma Real_intro x t T :
x ∈ El T ->
(x ∈ El T -> inSAT t (Real T x)) ->
[x,t] \real T.
split; auto.
Qed.
Lemma Real_ax x t T R :
(∀ x x', x ∈ T -> x==x' -> eqSAT (R x) (R x')) ->
([x,t] \real mkTY T R <-> x ∈ T /\ inSAT t (R x)).
intros.
unfold inX; rewrite El_def.
split; destruct 1; split; trivial; rewrite Real_def in *; auto with *.
Qed.
Lemma Real_intro2 x t T R :
(∀ x x', x ∈ T -> x==x' -> eqSAT (R x) (R x')) ->
x ∈ T ->
(x ∈ T -> inSAT t (R x)) ->
[x,t] \real mkTY T R.
split.
unfold inX; rewrite El_def; trivial.
rewrite Real_def; auto.
Qed.
Derived rules of the basic judgements
Lemma eq_typ_betar : ∀ e N T M,
typ e N T ->
T <> kind ->
eq_typ e (App (Abs T M) N) (subst N M).
intros.
apply eq_typ_beta; trivial.
reflexivity.
reflexivity.
Qed.
Lemma typ_var0 : ∀ e n T,
match T, nth_error e n with
Some _, value T' => T' <> kind /\ sub_typ e (lift (S n) T') T
| _,_ => False end ->
typ e (Ref n) T.
intros.
case_eq T; intros.
rewrite H0 in H.
case_eq (nth_error e n); intros.
rewrite H1 in H.
destruct H.
apply typ_subsumption with (lift (S n) t); auto.
apply typ_var; trivial.
destruct t as [(t,tm)|]; simpl; try discriminate.
elim H; trivial.
discriminate.
rewrite H1 in H; contradiction.
rewrite H0 in H; contradiction.
Qed.
Subtyping
Definition sub_typ_covariant : ∀ e U1 U2 V1 V2,
U1 <> kind ->
eq_typ e U1 U2 ->
sub_typ (U1::e) V1 V2 ->
sub_typ e (Prod U1 V1) (Prod U2 V2).
intros.
apply sub_typ_covariant; trivial.
intros.
unfold eqX, lam, app.
unfold inX in H2.
unfold prod in H2; rewrite El_def in H2.
apply cc_eta_eq in H2; trivial.
Qed.
Universes
Ordinals
Definition Ord (o:set) : trm :=
cst o Lc.K (fun _ _ => eq_refl) (fun _ _ _ => eq_refl).
Definition Ordt (o:set) : trm :=
cst (mkTY o (fun _ => snSAT)) Lc.K (fun _ _ => eq_refl) (fun _ _ _ => eq_refl).
Definition typ_ord_kind : ∀ e o, zero ∈ o -> typ e (Ordt o) kind.
red; simpl; intros.
split; [|split]; simpl.
discriminate.
exists nil; exists (Ordt o);[reflexivity|].
exists zero; intros; simpl.
unfold inX; rewrite El_def; trivial.
apply Lc.sn_K.
Qed.
Definition typ_ord_ord : ∀ e o o',
o < o' -> typ e (Ord o) (Ordt o').
red; simpl; intros.
apply in_int_intro; try discriminate.
simpl.
rewrite Real_ax;[split|]; auto with *.
apply Lc.sn_K.
Qed.
Definition OSucc : trm -> trm.
intros o; left; exists (fun i => osucc (int i o)) (fun j => tm j o).
do 2 red; intros.
rewrite H; reflexivity.
do 2 red; intros.
rewrite H; reflexivity.
red; intros.
apply tm_liftable.
red; intros.
apply tm_substitutive.
Defined.
Definition OSucct : trm -> trm.
intros o; left; exists (fun i => mkTY (osucc (int i o)) (fun _ => snSAT)) (fun j => tm j o).
do 2 red; intros.
apply mkTY_ext; auto with *.
rewrite H; reflexivity.
do 2 red; intros.
rewrite H; reflexivity.
red; intros.
apply tm_liftable.
red; intros.
apply tm_substitutive.
Defined.
Lemma tyord_inv : ∀ e i j o o',
isOrd o' ->
typ e o (Ordt o') ->
val_ok e i j ->
isOrd (int i o) /\ int i o < o' /\ Lc.sn (tm j o).
unfold typ; intros.
specialize H0 with (1:=H1).
apply in_int_not_kind in H0.
2:discriminate.
simpl in H0.
rewrite Real_ax in H0; auto with *.
destruct H0.
eauto using isOrd_inv.
Qed.
Nat
Require Import SATnat.
Opaque cNAT.
Definition Nat : trm.
left; exists (fun _ => mkTY NAT cNAT) (fun _ => Lc.K).
do 2 red; reflexivity.
do 2 red; reflexivity.
red; reflexivity.
red; reflexivity.
Defined.
Definition NatI (O:trm) : trm.
left; exists (fun i => mkTY (NATi (int i O)) cNAT) (fun j => tm j O).
do 2 red; intros.
unfold eqX.
apply mkTY_ext.
rewrite H; reflexivity.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT.
admit.
do 2 red; intros.
rewrite H; reflexivity.
red; intros.
apply tm_liftable.
red; intros.
apply tm_substitutive.
Defined.
Lemma typ_natI : ∀ e eps o,
isOrd eps ->
typ e o (Ordt eps) ->
typ e (NatI o) kind.
red; intros; simpl.
red in H0; specialize H0 with (1:=H1).
apply in_int_not_kind in H0.
2:discriminate.
split;[|split].
discriminate.
exists nil; exists (NatI o);[reflexivity|].
admit.
simpl.
apply real_sn in H0; trivial.
Qed.
Lemma realNati_def x t i O :
isOrd (int i O) ->
([x,t] \real int i (NatI O) <->
x ∈ NATi (int i O) /\ inSAT t (cNAT x)).
intros.
simpl.
rewrite Real_ax; auto with *.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT; trivial.
Qed.
Definition Zero : trm.
left; exists (fun _ => ZERO) (fun _ => ZE).
do 2 red; reflexivity.
do 2 red; reflexivity.
red; reflexivity.
red; reflexivity.
Defined.
Lemma typ_Zero : ∀ o e O,
isOrd o ->
typ e O (Ordt o) ->
typ e Zero (NatI (OSucc O)).
red; simpl; intros.
destruct tyord_inv with (2:=H0)(3:=H1) as (?,(?,_)); trivial.
apply in_int_intro; try discriminate.
rewrite realNati_def.
2:simpl; auto.
split.
simpl.
apply ZEROi_typ; trivial.
simpl tm.
apply cNAT_ZE.
Qed.
Definition Succ (o:trm): trm.
left; exists (fun i => lam (int i (NatI o)) SUCC) (fun _ => SU).
do 2 red; intros.
apply lam_ext.
apply mkTY_ext; auto with *.
rewrite H; reflexivity.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT.
admit.
red; intros.
rewrite H1; reflexivity.
do 2 red; auto.
red; reflexivity.
red; reflexivity.
Defined.
Lemma El_prod A Ar B Br :
ext_fun A B ->
El (prod(mkTY A Ar) (fun x => mkTY (B x) (Br x))) ==
cc_prod A B.
intros.
unfold prod; rewrite El_def.
apply cc_prod_ext.
rewrite El_def; reflexivity.
red; intros.
rewrite El_def; apply H; trivial.
rewrite El_def in H0; trivial.
Qed.
Lemma typ_succi : ∀ e o i,
isOrd o ->
typ e i (Ordt o) ->
typ e (Succ i) (Prod (NatI i) (NatI (OSucc (lift 1 i)))).
red; intros.
destruct tyord_inv with (2:=H0) (3:=H1) as (?,(?,?)); trivial.
clear H0.
apply in_int_intro; try discriminate.
apply prod_intro_sn.
red; intros.
rewrite H5; reflexivity.
red; intros.
rewrite H5; reflexivity.
simpl.
unfold SU.
constructor; intros.
red in H0; apply Lc.nf_norm in H0; [contradiction|].
repeat constructor.
intros.
rewrite realNati_def in H0 |- *; auto with *.
2:simpl;rewrite int_lift_eq; simpl; auto.
destruct H0.
split.
simpl; rewrite int_lift_eq; simpl.
apply SUCCi_typ; auto.
apply cNAT_SU; trivial.
revert H0; apply NATi_NAT; auto.
Qed.
Definition Natcase (fZ fS n : trm) : trm.
left; exists (fun i => NATCASE (int i fZ) (fun k => int (V.cons k i) fS) (int i n))
(fun j => NCASE (tm j fZ) (Lc.Abs (tm (Lc.ilift j) fS)) (tm j n)).
do 2 red; intros.
red.
apply NATCASE_morph.
rewrite H; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
rewrite H; reflexivity.
admit.
admit.
admit.
Defined.
Instance Natcase_morph :
Proper (eq_trm ==> eq_trm ==> eq_trm ==> eq_trm) Natcase.
do 4 red; intros.
split; red; simpl; intros.
apply NATCASE_morph_gen; intros.
rewrite H1; rewrite H2; reflexivity.
rewrite H; rewrite H2; reflexivity.
rewrite H0; rewrite H4; rewrite H2; reflexivity.
rewrite H; rewrite H0; rewrite H1; rewrite H2; trivial.
Qed.
Notation "'int0' x y" := (int y x) (at level 10, x at level 9, y at level 9).
Lemma Natcase_succ : ∀ o O e n fZ fS,
isOrd o ->
typ e O (Ordt o) ->
typ e n (NatI O) ->
eq_typ e (Natcase fZ fS (App (Succ O) n)) (subst n fS).
red; intros.
destruct tyord_inv with (2:=H0) (3:=H2) as (?,(?,_)); trivial.
red in H1; specialize H1 with (1:=H2).
apply in_int_not_kind in H1.
2:discriminate.
rewrite realNati_def in H1; trivial.
destruct H1 as (H1,_).
red; simpl.
rewrite <- (fun e1 e2 => NATCASE_morph (int0 fZ i) (int0 fZ i) e1
(fun k => int0 fS (V.cons k i)) (fun k => int0 fS (V.cons k i)) e2
(SUCC (int0 n i))); auto with *.
rewrite NATCASE_SUCC; auto.
rewrite int_subst_eq; reflexivity.
intros.
rewrite H5; reflexivity.
red; intros.
rewrite H5; reflexivity.
rewrite beta_eq; auto with *.
red; intros.
unfold SUCC; apply inr_morph; trivial.
rewrite El_def; trivial.
Qed.
Existing Instance NATi_morph.
Opaque cNAT.
Definition Nat : trm.
left; exists (fun _ => mkTY NAT cNAT) (fun _ => Lc.K).
do 2 red; reflexivity.
do 2 red; reflexivity.
red; reflexivity.
red; reflexivity.
Defined.
Definition NatI (O:trm) : trm.
left; exists (fun i => mkTY (NATi (int i O)) cNAT) (fun j => tm j O).
do 2 red; intros.
unfold eqX.
apply mkTY_ext.
rewrite H; reflexivity.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT.
admit.
do 2 red; intros.
rewrite H; reflexivity.
red; intros.
apply tm_liftable.
red; intros.
apply tm_substitutive.
Defined.
Lemma typ_natI : ∀ e eps o,
isOrd eps ->
typ e o (Ordt eps) ->
typ e (NatI o) kind.
red; intros; simpl.
red in H0; specialize H0 with (1:=H1).
apply in_int_not_kind in H0.
2:discriminate.
split;[|split].
discriminate.
exists nil; exists (NatI o);[reflexivity|].
admit.
simpl.
apply real_sn in H0; trivial.
Qed.
Lemma realNati_def x t i O :
isOrd (int i O) ->
([x,t] \real int i (NatI O) <->
x ∈ NATi (int i O) /\ inSAT t (cNAT x)).
intros.
simpl.
rewrite Real_ax; auto with *.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT; trivial.
Qed.
Definition Zero : trm.
left; exists (fun _ => ZERO) (fun _ => ZE).
do 2 red; reflexivity.
do 2 red; reflexivity.
red; reflexivity.
red; reflexivity.
Defined.
Lemma typ_Zero : ∀ o e O,
isOrd o ->
typ e O (Ordt o) ->
typ e Zero (NatI (OSucc O)).
red; simpl; intros.
destruct tyord_inv with (2:=H0)(3:=H1) as (?,(?,_)); trivial.
apply in_int_intro; try discriminate.
rewrite realNati_def.
2:simpl; auto.
split.
simpl.
apply ZEROi_typ; trivial.
simpl tm.
apply cNAT_ZE.
Qed.
Definition Succ (o:trm): trm.
left; exists (fun i => lam (int i (NatI o)) SUCC) (fun _ => SU).
do 2 red; intros.
apply lam_ext.
apply mkTY_ext; auto with *.
rewrite H; reflexivity.
intros.
apply fam_mrph; trivial.
revert H0; apply NATi_NAT.
admit.
red; intros.
rewrite H1; reflexivity.
do 2 red; auto.
red; reflexivity.
red; reflexivity.
Defined.
Lemma El_prod A Ar B Br :
ext_fun A B ->
El (prod(mkTY A Ar) (fun x => mkTY (B x) (Br x))) ==
cc_prod A B.
intros.
unfold prod; rewrite El_def.
apply cc_prod_ext.
rewrite El_def; reflexivity.
red; intros.
rewrite El_def; apply H; trivial.
rewrite El_def in H0; trivial.
Qed.
Lemma typ_succi : ∀ e o i,
isOrd o ->
typ e i (Ordt o) ->
typ e (Succ i) (Prod (NatI i) (NatI (OSucc (lift 1 i)))).
red; intros.
destruct tyord_inv with (2:=H0) (3:=H1) as (?,(?,?)); trivial.
clear H0.
apply in_int_intro; try discriminate.
apply prod_intro_sn.
red; intros.
rewrite H5; reflexivity.
red; intros.
rewrite H5; reflexivity.
simpl.
unfold SU.
constructor; intros.
red in H0; apply Lc.nf_norm in H0; [contradiction|].
repeat constructor.
intros.
rewrite realNati_def in H0 |- *; auto with *.
2:simpl;rewrite int_lift_eq; simpl; auto.
destruct H0.
split.
simpl; rewrite int_lift_eq; simpl.
apply SUCCi_typ; auto.
apply cNAT_SU; trivial.
revert H0; apply NATi_NAT; auto.
Qed.
Definition Natcase (fZ fS n : trm) : trm.
left; exists (fun i => NATCASE (int i fZ) (fun k => int (V.cons k i) fS) (int i n))
(fun j => NCASE (tm j fZ) (Lc.Abs (tm (Lc.ilift j) fS)) (tm j n)).
do 2 red; intros.
red.
apply NATCASE_morph.
rewrite H; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
rewrite H; reflexivity.
admit.
admit.
admit.
Defined.
Instance Natcase_morph :
Proper (eq_trm ==> eq_trm ==> eq_trm ==> eq_trm) Natcase.
do 4 red; intros.
split; red; simpl; intros.
apply NATCASE_morph_gen; intros.
rewrite H1; rewrite H2; reflexivity.
rewrite H; rewrite H2; reflexivity.
rewrite H0; rewrite H4; rewrite H2; reflexivity.
rewrite H; rewrite H0; rewrite H1; rewrite H2; trivial.
Qed.
Notation "'int0' x y" := (int y x) (at level 10, x at level 9, y at level 9).
Lemma Natcase_succ : ∀ o O e n fZ fS,
isOrd o ->
typ e O (Ordt o) ->
typ e n (NatI O) ->
eq_typ e (Natcase fZ fS (App (Succ O) n)) (subst n fS).
red; intros.
destruct tyord_inv with (2:=H0) (3:=H2) as (?,(?,_)); trivial.
red in H1; specialize H1 with (1:=H2).
apply in_int_not_kind in H1.
2:discriminate.
rewrite realNati_def in H1; trivial.
destruct H1 as (H1,_).
red; simpl.
rewrite <- (fun e1 e2 => NATCASE_morph (int0 fZ i) (int0 fZ i) e1
(fun k => int0 fS (V.cons k i)) (fun k => int0 fS (V.cons k i)) e2
(SUCC (int0 n i))); auto with *.
rewrite NATCASE_SUCC; auto.
rewrite int_subst_eq; reflexivity.
intros.
rewrite H5; reflexivity.
red; intros.
rewrite H5; reflexivity.
rewrite beta_eq; auto with *.
red; intros.
unfold SUCC; apply inr_morph; trivial.
rewrite El_def; trivial.
Qed.
Existing Instance NATi_morph.
Admitted:
Lemma NCASE_fNAT' o f g n k (A B:family) :
isOrd o ->
k ∈ NATi (osucc o) ->
inSAT n (fNAT A k) ->
inSAT f (B ZERO) ->
inSAT g (piNATi(fun m => prodSAT (A m) (B (SUCC m)))o) ->
inSAT (NCASE f g n) (B k).
unfold NCASE; intros.
rewrite fNAT_def in H1.
apply H1 with (P:=B); intros; trivial.
rewrite piNATi_ax in H3; intros.
destruct H3 as (sng,H3).
rewrite piNAT_ax.
split; intros.
do 2 apply Lc.sn_abs.
apply Lc.sn_app_var.
apply Lc.sn_lift; trivial.
Admitted.
Lemma typ_natcase : ∀ o e O P fZ fS n,
isOrd o ->
typ e O (Ordt o) ->
typ e fZ (App P Zero) ->
typ (NatI O :: e) fS (App (lift 1 P) (App (Succ (lift 1 O)) (Ref 0))) ->
typ e n (NatI (OSucc O)) ->
typ e (Natcase fZ fS n) (App P n).
red; intros.
destruct tyord_inv with (2:=H0)(3:=H4) as (?,(?,_ )); trivial.
red in H1; specialize H1 with (1:=H4).
apply in_int_not_kind in H1;[|discriminate].
red in H3; specialize H3 with (1:=H4).
apply in_int_not_kind in H3;[|discriminate].
apply in_int_intro; try discriminate.
destruct H1.
rewrite realNati_def in H3; simpl in H3|-*; auto.
destruct H3.
apply Real_intro; intros.
apply NATCASE_typ with (o:=int i O) (P:=fun n => El(app (int i P) n)); intros; trivial.
do 2 red; intros.
rewrite H9; reflexivity.
do 2 red; intros.
rewrite H9; reflexivity.
assert (val_ok (NatI O :: e) (V.cons n0 i) (I.cons daimon j)).
apply vcons_add_var; trivial.
2:discriminate.
rewrite realNati_def; auto with *.
split; trivial.
apply varSAT.
apply H2 in H10; clear H1; simpl in H10.
apply in_int_not_kind in H10;[|discriminate].
destruct H10 as(H10,_ ).
revert H10; apply eq_elim; simpl.
rewrite int_cons_lift_eq.
rewrite beta_eq; auto with *.
red; intros; apply inr_morph; auto.
rewrite El_def.
rewrite int_cons_lift_eq; trivial.
rewrite cNAT_eq in H8.
pose (B:=fun k => Real (app (int0 P i) k)
(NATCASE (int0 fZ i) (fun k => int0 fS (V.cons k i)) k)).
assert (Bm : ∀ x y, x ∈ NAT -> x == y -> eqSAT (B x) (B y)).
unfold B; intros.
apply Real_morph.
rewrite H11; reflexivity.
apply NATCASE_morph; auto with *.
red; intros.
rewrite H12; reflexivity.
apply NCASE_fNAT' with (o:=int0 O i) (A:=cNAT) (B:=mkFam B Bm) (k:=int0 n i); trivial.
unfold B; simpl in H1|-*.
rewrite NATCASE_ZERO.
trivial.
rewrite piNATi_ax.
split; intros.
apply typ_abs in H2.
3:discriminate.
2:left.
2:apply typ_natI with o; trivial.
apply H2 in H4.
apply in_int_sn in H4.
eapply Lc.subterm_sn.
eapply Lc.subterm_sn.
eexact H4.
apply Lc.sbtrm_app_l.
apply Lc.sbtrm_app_r.
apply prodSAT_intro.
intros.
rewrite <- tm_subst_cons.
unfold B; simpl.
rewrite NATCASE_SUCC.
2:intros ? e'; rewrite e'; reflexivity.
assert (val_ok (NatI O :: e) (V.cons n0 i) (I.cons v j)).
apply vcons_add_var; trivial.
2:discriminate.
rewrite realNati_def; auto with *.
apply H2 in H12.
apply in_int_not_kind in H12.
2:discriminate.
destruct H12 as (_,H12).
simpl in H12.
rewrite int_lift_eq in H12.
revert H12; apply inSAT_morph; trivial.
apply Real_morph; auto with *.
apply cc_app_morph; [reflexivity|].
unfold app, lam; rewrite cc_beta_eq; auto with *.
rewrite El_def.
rewrite int_lift_eq; trivial.
Qed.
Lemma typ_natcase' : ∀ o e O P fZ fS n T,
isOrd o ->
T <> kind ->
typ e O (Ordt o) ->
sub_typ e (App P n) T ->
typ e fZ (App P Zero) ->
typ (NatI O :: e) fS
(App (lift 1 P) (App (Succ (lift 1 O)) (Ref 0))) ->
typ e n (NatI (OSucc O)) ->
typ e (Natcase fZ fS n) T.
intros.
apply typ_subsumption with (App P n); auto.
2:discriminate.
apply typ_natcase with o O; trivial.
Qed.
isOrd o ->
k ∈ NATi (osucc o) ->
inSAT n (fNAT A k) ->
inSAT f (B ZERO) ->
inSAT g (piNATi(fun m => prodSAT (A m) (B (SUCC m)))o) ->
inSAT (NCASE f g n) (B k).
unfold NCASE; intros.
rewrite fNAT_def in H1.
apply H1 with (P:=B); intros; trivial.
rewrite piNATi_ax in H3; intros.
destruct H3 as (sng,H3).
rewrite piNAT_ax.
split; intros.
do 2 apply Lc.sn_abs.
apply Lc.sn_app_var.
apply Lc.sn_lift; trivial.
Admitted.
Lemma typ_natcase : ∀ o e O P fZ fS n,
isOrd o ->
typ e O (Ordt o) ->
typ e fZ (App P Zero) ->
typ (NatI O :: e) fS (App (lift 1 P) (App (Succ (lift 1 O)) (Ref 0))) ->
typ e n (NatI (OSucc O)) ->
typ e (Natcase fZ fS n) (App P n).
red; intros.
destruct tyord_inv with (2:=H0)(3:=H4) as (?,(?,_ )); trivial.
red in H1; specialize H1 with (1:=H4).
apply in_int_not_kind in H1;[|discriminate].
red in H3; specialize H3 with (1:=H4).
apply in_int_not_kind in H3;[|discriminate].
apply in_int_intro; try discriminate.
destruct H1.
rewrite realNati_def in H3; simpl in H3|-*; auto.
destruct H3.
apply Real_intro; intros.
apply NATCASE_typ with (o:=int i O) (P:=fun n => El(app (int i P) n)); intros; trivial.
do 2 red; intros.
rewrite H9; reflexivity.
do 2 red; intros.
rewrite H9; reflexivity.
assert (val_ok (NatI O :: e) (V.cons n0 i) (I.cons daimon j)).
apply vcons_add_var; trivial.
2:discriminate.
rewrite realNati_def; auto with *.
split; trivial.
apply varSAT.
apply H2 in H10; clear H1; simpl in H10.
apply in_int_not_kind in H10;[|discriminate].
destruct H10 as(H10,_ ).
revert H10; apply eq_elim; simpl.
rewrite int_cons_lift_eq.
rewrite beta_eq; auto with *.
red; intros; apply inr_morph; auto.
rewrite El_def.
rewrite int_cons_lift_eq; trivial.
rewrite cNAT_eq in H8.
pose (B:=fun k => Real (app (int0 P i) k)
(NATCASE (int0 fZ i) (fun k => int0 fS (V.cons k i)) k)).
assert (Bm : ∀ x y, x ∈ NAT -> x == y -> eqSAT (B x) (B y)).
unfold B; intros.
apply Real_morph.
rewrite H11; reflexivity.
apply NATCASE_morph; auto with *.
red; intros.
rewrite H12; reflexivity.
apply NCASE_fNAT' with (o:=int0 O i) (A:=cNAT) (B:=mkFam B Bm) (k:=int0 n i); trivial.
unfold B; simpl in H1|-*.
rewrite NATCASE_ZERO.
trivial.
rewrite piNATi_ax.
split; intros.
apply typ_abs in H2.
3:discriminate.
2:left.
2:apply typ_natI with o; trivial.
apply H2 in H4.
apply in_int_sn in H4.
eapply Lc.subterm_sn.
eapply Lc.subterm_sn.
eexact H4.
apply Lc.sbtrm_app_l.
apply Lc.sbtrm_app_r.
apply prodSAT_intro.
intros.
rewrite <- tm_subst_cons.
unfold B; simpl.
rewrite NATCASE_SUCC.
2:intros ? e'; rewrite e'; reflexivity.
assert (val_ok (NatI O :: e) (V.cons n0 i) (I.cons v j)).
apply vcons_add_var; trivial.
2:discriminate.
rewrite realNati_def; auto with *.
apply H2 in H12.
apply in_int_not_kind in H12.
2:discriminate.
destruct H12 as (_,H12).
simpl in H12.
rewrite int_lift_eq in H12.
revert H12; apply inSAT_morph; trivial.
apply Real_morph; auto with *.
apply cc_app_morph; [reflexivity|].
unfold app, lam; rewrite cc_beta_eq; auto with *.
rewrite El_def.
rewrite int_lift_eq; trivial.
Qed.
Lemma typ_natcase' : ∀ o e O P fZ fS n T,
isOrd o ->
T <> kind ->
typ e O (Ordt o) ->
sub_typ e (App P n) T ->
typ e fZ (App P Zero) ->
typ (NatI O :: e) fS
(App (lift 1 P) (App (Succ (lift 1 O)) (Ref 0))) ->
typ e n (NatI (OSucc O)) ->
typ e (Natcase fZ fS n) T.
intros.
apply typ_subsumption with (App P n); auto.
2:discriminate.
apply typ_natcase with o O; trivial.
Qed.
Occurrences
Definition noccur (f:nat->bool) (T:trm) : Prop :=
∀ i i',
(∀ n, if f n then True else i n == i' n) ->
int i T == int i' T.
Lemma noc_var : ∀ f n, f n = false -> noccur f (Ref n).
red; simpl; intros.
specialize (H0 n).
rewrite H in H0; trivial.
Qed.
Lemma noc_kind : ∀ f, noccur f kind.
red; simpl; reflexivity.
Qed.
Lemma noc_prop : ∀ f, noccur f prop.
red; simpl; reflexivity.
Qed.
Lemma noc_app : ∀ f a b,
noccur f a -> noccur f b -> noccur f (App a b).
unfold noccur; simpl; intros.
rewrite (H _ _ H1).
rewrite (H0 _ _ H1).
reflexivity.
Qed.
Judgements with variance
Module Beq.
Definition t := bool.
Definition eq := @eq bool.
Definition eq_equiv : Equivalence eq := eq_equivalence.
Existing Instance eq_equiv.
End Beq.
Module B := VarMap.Make(Beq).
Module OTeq.
Definition t := option trm.
Definition eq := @eq (option trm).
Definition eq_equiv : Equivalence eq := eq_equivalence.
Existing Instance eq_equiv.
End OTeq.
Module OT := VarMap.Make(OTeq).
Record fenv := {
tenv : env;
ords : B.map;
fixs : OT.map
}.
Definition tinj e :=
Build_fenv e (B.nil false) (OT.nil None).
Definition push_var e T :=
Build_fenv (T::tenv e) (B.cons false (ords e)) (OT.cons None (fixs e)).
Definition push_fun e dom rng :=
Build_fenv (Prod dom rng::tenv e)
(B.cons false (ords e)) (OT.cons (Some dom) (fixs e)).
Definition push_ord e T :=
Build_fenv (T::tenv e) (B.cons true (ords e)) (OT.cons None (fixs e)).
Definition val_mono (e:fenv) i j i' j' :=
val_ok (tenv e) i j /\
val_ok (tenv e) i' j' /\
∀ n,
if ords e n then i n ⊆ i' n
else match fixs e n with
Some T => ∀ x, x ∈ El(int (V.shift (S n) i) T) -> app (i n) x == app (i' n) x
| _ => i n == i' n
end.
Lemma val_mono_refl : ∀ e i j,
val_ok (tenv e) i j -> val_mono e i j i j.
split;[idtac|split]; simpl; auto with *.
intro n.
destruct (ords e n); auto with *.
destruct (fixs e n); auto with *.
Qed.
Lemma val_push_var : ∀ e i j i' j' x t x' t' T,
val_mono e i j i' j' ->
x == x' ->
[x,t] \real int i T ->
[x',t'] \real int i' T ->
T <> kind ->
val_mono (push_var e T) (V.cons x i) (I.cons t j) (V.cons x' i') (I.cons t' j').
destruct 1 as (?&?&?); split;[idtac|split]; trivial.
unfold push_var; simpl.
apply vcons_add_var; trivial.
unfold push_var; simpl.
apply vcons_add_var; trivial.
destruct n as [|n]; simpl; auto.
generalize (H1 n).
destruct (ords e n); trivial.
Qed.
Lemma val_push_ord : ∀ e i j i' j' x t x' t' T,
val_mono e i j i' j' ->
x ⊆ x' ->
[x,t] \real int i T ->
[x',t'] \real int i' T ->
T <> kind ->
val_mono (push_ord e T) (V.cons x i) (I.cons t j) (V.cons x' i') (I.cons t' j').
destruct 1 as (?&?&?); split;[idtac|split]; trivial.
unfold push_ord; simpl.
apply vcons_add_var; trivial.
unfold push_ord; simpl.
apply vcons_add_var; trivial.
destruct n as [|n]; simpl; auto.
generalize (H1 n).
destruct (ords e n); trivial.
Qed.
Lemma val_push_fun : ∀ e i j i' j' f tf g tg T U,
val_mono e i j i' j' ->
[f,tf] \real prod (int i T) (fun x => int (V.cons x i) U) ->
[g,tg] \real prod (int i' T) (fun x => int (V.cons x i') U) ->
fcompat (El(int i T)) f g ->
val_mono (push_fun e T U) (V.cons f i) (I.cons tf j) (V.cons g i') (I.cons tg j').
destruct 1 as (?&?&?); split;[idtac|split]; trivial.
unfold push_fun; simpl.
apply vcons_add_var; trivial.
discriminate.
unfold push_fun; simpl.
apply vcons_add_var; trivial.
discriminate.
destruct n as [|n]; simpl; auto.
generalize (H1 n).
destruct (ords e n); trivial.
Qed.
Function Extension judgment
Definition fx_extends e dom M :=
∀ i i' j j', val_mono e i j i' j' ->
fcompat (El(int i dom)) (int i M) (int i' M).
∀ i i' j j', val_mono e i j i' j' ->
fcompat (El(int i dom)) (int i M) (int i' M).
Covariance judgment
Definition fx_sub e M :=
∀ i i' j j', val_mono e i j i' j' ->
∀ x t, [x,t] \real int i M -> [x,t] \real int i' M.
Definition fx_subval e M :=
∀ i i' j j', val_mono e i j i' j' -> int i M ⊆ int i' M.
∀ i i' j j', val_mono e i j i' j' ->
∀ x t, [x,t] \real int i M -> [x,t] \real int i' M.
Definition fx_subval e M :=
∀ i i' j j', val_mono e i j i' j' -> int i M ⊆ int i' M.
Invariance
Definition fx_equals e M :=
∀ i i' j j', val_mono e i j i' j' -> int i M == int i' M.
Definition spec_var e n :=
ords e n || match fixs e n with Some _ => true | _ => false end.
Lemma fx_eq_noc : ∀ e t,
noccur (spec_var e) t ->
fx_equals e t.
unfold noccur, fx_equals, spec_var; intros.
apply H; intros.
destruct H0 as (_,(_,H0)).
generalize (H0 n).
destruct (ords e n); simpl; trivial.
destruct (fixs e n); simpl; trivial.
Qed.
Lemma fx_eq_app : ∀ e u v,
fx_equals e u ->
fx_equals e v ->
fx_equals e (App u v).
unfold fx_equals; intros.
specialize H with (1:=H1).
specialize H0 with (1:=H1).
simpl.
rewrite H; rewrite H0; reflexivity.
Qed.
Lemma fx_eq_abs : ∀ e T M,
T <> kind ->
fx_equals e T ->
fx_equals (push_var e T) M ->
fx_equals e (Abs T M).
unfold fx_equals; intros.
simpl.
apply lam_ext; eauto.
red; intros.
apply H1 with (I.cons daimon j) (I.cons daimon j').
specialize H0 with (1:=H2).
apply val_push_var; auto.
split; trivial.
apply varSAT.
split.
2:apply varSAT.
unfold inX; rewrite <- H4; rewrite <- H0; trivial.
Qed.
Lemma fx_eq_rec_call : ∀ e n x T U,
ords e n = false ->
fixs e n = Some T ->
T <> kind ->
typ (tenv e) (Ref n) (Prod (lift (S n) T) U) ->
fx_equals e x ->
typ (tenv e) x (lift (S n) T) ->
fx_equals e (App (Ref n) x).
unfold fx_equals; intros.
simpl.
specialize H3 with (1:=H5).
rewrite <- H3.
destruct H5 as (Hty,(Hty',Hrec)).
specialize Hrec with n.
rewrite H in Hrec; rewrite H0 in Hrec.
apply Hrec.
red in H4; specialize H4 with (1:=Hty); trivial.
apply in_int_not_kind in H4; trivial.
2:destruct T;[discriminate|elim H1;reflexivity].
destruct H4 as (?,_ ).
unfold inX in H4.
unfold lift in H4; rewrite int_lift_rec_eq in H4.
rewrite V.lams0 in H4; trivial.
Qed.
Lemma fx_equals_subval : ∀ e M, fx_equals e M -> fx_subval e M.
unfold fx_subval, fx_equals; intros.
apply H in H0.
rewrite <- H0; reflexivity.
Qed.
Lemma fx_equals_sub : ∀ e M, fx_equals e M -> fx_sub e M.
unfold fx_sub, fx_equals; intros.
apply H in H0.
rewrite <- H0; trivial.
Qed.
Lemma var_sub : ∀ e n,
ords e n = true ->
fx_subval e (Ref n).
unfold fx_subval; intros.
destruct H0 as (_,(_,H0)).
generalize (H0 n); rewrite H.
simpl; trivial.
Qed.
Lemma fx_sub_prod : ∀ e T U,
T <> kind ->
fx_equals e T ->
fx_sub (push_var e T) U ->
fx_sub e (Prod T U).
red; intros.
rewrite intProd_eq in H3|-*.
specialize (H0 _ _ _ _ H2).
destruct H3.
unfold inX in H3.
rewrite Real_prod in H4; trivial.
unfold prod in H3; rewrite El_def in H3.
assert (x ∈ El(prod (int i' T) (fun x0 : X => int (V.cons x0 i') U))).
unfold prod, inX; rewrite El_def.
revert H3; apply cc_prod_covariant.
do 2 red; intros.
rewrite H5; reflexivity.
rewrite H0; reflexivity.
intros.
red in H1.
assert (val_mono (push_var e T) (V.cons x0 i) (I.cons daimon j) (V.cons x0 i') (I.cons daimon j')).
apply val_push_var; auto with *.
split; trivial; apply varSAT.
split.
rewrite <- H0; trivial.
apply varSAT.
specialize (H1 _ _ _ _ H5).
red; intros.
destruct H1 with z daimon; trivial.
split; trivial.
apply varSAT.
split; trivial.
rewrite Real_prod; trivial.
unfold piSAT.
apply interSAT_intro' with
(F:=fun v => prodSAT(Real(int i' T) v)(Real(int(V.cons v i') U)(cc_app x v))).
apply sat_sn in H4; trivial.
intros.
rewrite <- H0 in H6.
specialize interSAT_elim with (1:=H4) (x:=exist (fun x=>_) x0 H6); simpl proj1_sig; intros.
revert H7; apply prodSAT_mono.
do 2 red; intros.
rewrite <- H0 in H7; trivial.
red; intros.
apply H1 with (i:=V.cons x0 i) (j:=I.cons daimon j) (j':=I.cons daimon j').
apply val_push_var; auto with *.
split; trivial; apply varSAT.
split.
rewrite <- H0; trivial.
apply varSAT.
split; trivial.
unfold inX; apply cc_prod_elim with (1:=H3); trivial.
red; intros.
rewrite H7; reflexivity.
red; intros.
rewrite H6; reflexivity.
Qed.
Lemma NATi_sub : ∀ e o O,
isOrd o ->
typ (tenv e) O (Ordt o) ->
fx_subval e O ->
fx_sub e (NatI O).
unfold fx_sub, fx_subval; intros.
destruct tyord_inv with (2:=H0) (3:=proj1 H2); trivial.
destruct tyord_inv with (2:=H0) (3:=proj1 (proj2 H2)); trivial.
specialize H1 with (1:=H2).
rewrite realNati_def in H3|-*; trivial.
destruct H3.
split; trivial.
revert H3; apply TI_mono; auto.
Qed.
Lemma OSucc_sub : ∀ e O,
fx_subval e O ->
fx_subval e (OSucc O).
unfold fx_subval; simpl; intros.
apply osucc_mono; eauto.
admit.
admit.
Qed.
Lemma fx_abs : ∀ e U T M,
T <> kind ->
fx_sub e T ->
fx_equals (push_var e T) M ->
typ (T::tenv e) M U ->
U <> kind ->
fx_extends e T (Abs T M).
unfold fx_sub, fx_equals, fx_extends; intros.
specialize H0 with (1:=H4).
simpl.
red; intros.
fold app.
rewrite beta_eq; try assumption.
rewrite beta_eq.
apply H1 with (I.cons daimon j) (I.cons daimon j').
apply val_push_var; auto with *.
split; [trivial|apply varSAT].
split; [trivial|apply varSAT].
destruct H0 with x daimon; trivial.
split; [trivial|apply varSAT].
red; red; intros.
rewrite H7; reflexivity.
apply H0 with (x:=x) (t:=daimon); trivial.
split; [trivial|apply varSAT].
red; red; intros.
rewrite H7; reflexivity.
Qed.
∀ i i' j j', val_mono e i j i' j' -> int i M == int i' M.
Definition spec_var e n :=
ords e n || match fixs e n with Some _ => true | _ => false end.
Lemma fx_eq_noc : ∀ e t,
noccur (spec_var e) t ->
fx_equals e t.
unfold noccur, fx_equals, spec_var; intros.
apply H; intros.
destruct H0 as (_,(_,H0)).
generalize (H0 n).
destruct (ords e n); simpl; trivial.
destruct (fixs e n); simpl; trivial.
Qed.
Lemma fx_eq_app : ∀ e u v,
fx_equals e u ->
fx_equals e v ->
fx_equals e (App u v).
unfold fx_equals; intros.
specialize H with (1:=H1).
specialize H0 with (1:=H1).
simpl.
rewrite H; rewrite H0; reflexivity.
Qed.
Lemma fx_eq_abs : ∀ e T M,
T <> kind ->
fx_equals e T ->
fx_equals (push_var e T) M ->
fx_equals e (Abs T M).
unfold fx_equals; intros.
simpl.
apply lam_ext; eauto.
red; intros.
apply H1 with (I.cons daimon j) (I.cons daimon j').
specialize H0 with (1:=H2).
apply val_push_var; auto.
split; trivial.
apply varSAT.
split.
2:apply varSAT.
unfold inX; rewrite <- H4; rewrite <- H0; trivial.
Qed.
Lemma fx_eq_rec_call : ∀ e n x T U,
ords e n = false ->
fixs e n = Some T ->
T <> kind ->
typ (tenv e) (Ref n) (Prod (lift (S n) T) U) ->
fx_equals e x ->
typ (tenv e) x (lift (S n) T) ->
fx_equals e (App (Ref n) x).
unfold fx_equals; intros.
simpl.
specialize H3 with (1:=H5).
rewrite <- H3.
destruct H5 as (Hty,(Hty',Hrec)).
specialize Hrec with n.
rewrite H in Hrec; rewrite H0 in Hrec.
apply Hrec.
red in H4; specialize H4 with (1:=Hty); trivial.
apply in_int_not_kind in H4; trivial.
2:destruct T;[discriminate|elim H1;reflexivity].
destruct H4 as (?,_ ).
unfold inX in H4.
unfold lift in H4; rewrite int_lift_rec_eq in H4.
rewrite V.lams0 in H4; trivial.
Qed.
Lemma fx_equals_subval : ∀ e M, fx_equals e M -> fx_subval e M.
unfold fx_subval, fx_equals; intros.
apply H in H0.
rewrite <- H0; reflexivity.
Qed.
Lemma fx_equals_sub : ∀ e M, fx_equals e M -> fx_sub e M.
unfold fx_sub, fx_equals; intros.
apply H in H0.
rewrite <- H0; trivial.
Qed.
Lemma var_sub : ∀ e n,
ords e n = true ->
fx_subval e (Ref n).
unfold fx_subval; intros.
destruct H0 as (_,(_,H0)).
generalize (H0 n); rewrite H.
simpl; trivial.
Qed.
Lemma fx_sub_prod : ∀ e T U,
T <> kind ->
fx_equals e T ->
fx_sub (push_var e T) U ->
fx_sub e (Prod T U).
red; intros.
rewrite intProd_eq in H3|-*.
specialize (H0 _ _ _ _ H2).
destruct H3.
unfold inX in H3.
rewrite Real_prod in H4; trivial.
unfold prod in H3; rewrite El_def in H3.
assert (x ∈ El(prod (int i' T) (fun x0 : X => int (V.cons x0 i') U))).
unfold prod, inX; rewrite El_def.
revert H3; apply cc_prod_covariant.
do 2 red; intros.
rewrite H5; reflexivity.
rewrite H0; reflexivity.
intros.
red in H1.
assert (val_mono (push_var e T) (V.cons x0 i) (I.cons daimon j) (V.cons x0 i') (I.cons daimon j')).
apply val_push_var; auto with *.
split; trivial; apply varSAT.
split.
rewrite <- H0; trivial.
apply varSAT.
specialize (H1 _ _ _ _ H5).
red; intros.
destruct H1 with z daimon; trivial.
split; trivial.
apply varSAT.
split; trivial.
rewrite Real_prod; trivial.
unfold piSAT.
apply interSAT_intro' with
(F:=fun v => prodSAT(Real(int i' T) v)(Real(int(V.cons v i') U)(cc_app x v))).
apply sat_sn in H4; trivial.
intros.
rewrite <- H0 in H6.
specialize interSAT_elim with (1:=H4) (x:=exist (fun x=>_) x0 H6); simpl proj1_sig; intros.
revert H7; apply prodSAT_mono.
do 2 red; intros.
rewrite <- H0 in H7; trivial.
red; intros.
apply H1 with (i:=V.cons x0 i) (j:=I.cons daimon j) (j':=I.cons daimon j').
apply val_push_var; auto with *.
split; trivial; apply varSAT.
split.
rewrite <- H0; trivial.
apply varSAT.
split; trivial.
unfold inX; apply cc_prod_elim with (1:=H3); trivial.
red; intros.
rewrite H7; reflexivity.
red; intros.
rewrite H6; reflexivity.
Qed.
Lemma NATi_sub : ∀ e o O,
isOrd o ->
typ (tenv e) O (Ordt o) ->
fx_subval e O ->
fx_sub e (NatI O).
unfold fx_sub, fx_subval; intros.
destruct tyord_inv with (2:=H0) (3:=proj1 H2); trivial.
destruct tyord_inv with (2:=H0) (3:=proj1 (proj2 H2)); trivial.
specialize H1 with (1:=H2).
rewrite realNati_def in H3|-*; trivial.
destruct H3.
split; trivial.
revert H3; apply TI_mono; auto.
Qed.
Lemma OSucc_sub : ∀ e O,
fx_subval e O ->
fx_subval e (OSucc O).
unfold fx_subval; simpl; intros.
apply osucc_mono; eauto.
admit.
admit.
Qed.
Lemma fx_abs : ∀ e U T M,
T <> kind ->
fx_sub e T ->
fx_equals (push_var e T) M ->
typ (T::tenv e) M U ->
U <> kind ->
fx_extends e T (Abs T M).
unfold fx_sub, fx_equals, fx_extends; intros.
specialize H0 with (1:=H4).
simpl.
red; intros.
fold app.
rewrite beta_eq; try assumption.
rewrite beta_eq.
apply H1 with (I.cons daimon j) (I.cons daimon j').
apply val_push_var; auto with *.
split; [trivial|apply varSAT].
split; [trivial|apply varSAT].
destruct H0 with x daimon; trivial.
split; [trivial|apply varSAT].
red; red; intros.
rewrite H7; reflexivity.
apply H0 with (x:=x) (t:=daimon); trivial.
split; [trivial|apply varSAT].
red; red; intros.
rewrite H7; reflexivity.
Qed.
Recursor (without case analysis)
Definition NatFix (O M:trm) : trm.
left.
exists (fun i =>
NATREC (fun o' f => int (V.cons f (V.cons o' i)) M) (int i O))
(fun j => NATFIX (Lc.Abs (tm (Lc.ilift (I.cons (tm j O) j)) M))).
admit.
admit.
admit.
admit.
Defined.
Typing rules of NatFix
Section NatFixRules.
Variable infty : set.
Hypothesis infty_ord : isOrd infty.
Variable E : fenv.
Let e := tenv E.
Variable O U M : trm.
Hypothesis M_nk : ~ eq_trm M kind.
Hypothesis ty_O : typ e O (Ordt infty).
Hypothesis ty_M : typ (Prod (NatI (Ref 0)) U::OSucct O::e)
M (Prod (NatI (OSucc (Ref 1)))
(lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))).
Hypothesis stab : fx_extends
(push_fun (push_ord E (OSucct O)) (NatI (Ref 0)) U)
(NatI (OSucc (Ref 1)))
M.
Let F i := fun o' f => int (V.cons f (V.cons o' i)) M.
Lemma morph_fix_body : ∀ i, morph2 (F i).
unfold F; do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
Qed.
Lemma ext_fun_ty : ∀ o i,
ext_fun (NATi o) (fun x => int (V.cons x (V.cons o i)) U).
do 2 red; intros.
rewrite H0;reflexivity.
Qed.
Hypothesis fx_sub_U :
fx_sub (push_var (push_ord E (OSucct O)) (NatI (OSucc (Ref 0)))) U.
Lemma ty_fix_body : ∀ i j o f,
val_ok e i j ->
o < osucc (int i O) ->
f ∈ cc_prod (NATi o) (fun x => El(int (V.cons x (V.cons o i)) U)) ->
F i o f ∈
cc_prod (NATi (osucc o)) (fun x => El(int (V.cons x (V.cons (osucc o) i)) U)).
unfold F; intros.
destruct tyord_inv with (2:=ty_O) (3:=H); trivial.
red in ty_M.
assert (val_ok (Prod (NatI(Ref 0)) U::OSucct O::e)
(V.cons f (V.cons o i)) (I.cons daimon (I.cons daimon j))).
apply vcons_add_var; auto.
3:discriminate.
apply vcons_add_var; auto.
2:discriminate.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; trivial.
split;[|apply varSAT].
rewrite intProd_eq.
unfold inX, prod; rewrite El_def.
revert H1; apply eq_elim.
apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H4; reflexivity.
specialize ty_M with (1:=H4).
apply in_int_not_kind in ty_M.
2:discriminate.
destruct ty_M as (?,_).
rewrite intProd_eq in H5; unfold inX in H5.
unfold prod in H5; rewrite El_def in H5.
revert H5; apply eq_elim.
symmetry; apply cc_prod_ext.
simpl; rewrite El_def.
reflexivity.
red; intros.
rewrite int_lift_rec_eq.
rewrite int_subst_rec_eq.
rewrite int_lift_rec_eq.
apply El_morph; apply int_morph; auto with *.
do 2 red.
intros [|[|k]].
compute; trivial.
unfold V.lams, V.shift; simpl.
reflexivity.
unfold V.lams, V.shift; simpl.
replace (k-0) with k; auto with *.
Qed.
Lemma fix_body_irrel : ∀ i j,
val_ok e i j ->
NAT_ord_irrel (int i O) (F i) (fun o' x => El(int (V.cons x (V.cons o' i)) U)).
Admitted.
Lemma fix_codom_mono : ∀ o o' x x' i j,
val_ok e i j ->
isOrd o' ->
o' ⊆ int i O ->
isOrd o ->
o ⊆ o' ->
x ∈ NATi o ->
x == x' ->
El (int (V.cons x (V.cons o i)) U) ⊆ El(int (V.cons x' (V.cons o' i)) U).
Admitted.
Hint Resolve morph_fix_body ext_fun_ty ty_fix_body fix_codom_mono fix_body_irrel.
Let fix_typ o i j:
val_ok e i j ->
isOrd o ->
isOrd (int i O) ->
o ⊆ int i O ->
NATREC (F i) o
∈ cc_prod (NATi o) (fun n => El (int (V.cons n (V.cons o i)) U)).
intros.
eapply NATREC_wt with (U:=fun o n => El(int(V.cons n (V.cons o i))U)); trivial.
intros.
apply fix_codom_mono with (1:=H); trivial.
transitivity o; trivial.
intros; apply ty_fix_body with (1:=H); trivial.
apply isOrd_plump with (int i O); auto.
transitivity o; trivial.
apply lt_osucc; trivial.
red; intros; apply fix_body_irrel with (1:=H); trivial.
transitivity o; trivial.
Qed.
Lemma fix_irr i j o o' x :
val_ok e i j ->
isOrd o ->
isOrd o' ->
isOrd (int i O) ->
o ⊆ o' ->
o' ⊆ int i O ->
x ∈ NATi o ->
cc_app (NATREC (F i) o) x == cc_app (NATREC (F i) o') x.
intros.
apply NATREC_ord_irrel with
(ord:=int i O)
(U:=fun o x => int (V.cons x (V.cons o i)) U); auto.
admit.
admit.
admit.
Qed.
Lemma fix_eqn : ∀ i j o n,
val_ok e i j ->
isOrd o ->
isOrd (int i O) ->
o ⊆ int i O ->
n ∈ NATi (osucc o) ->
cc_app (NATREC (F i) (osucc o)) n ==
cc_app (int (V.cons (NATREC (F i) o) (V.cons o i)) M) n.
intros.
unfold NATREC at 1.
rewrite REC_eq; auto with *.
apply cc_app_morph; auto with *.
apply incl_eq.
red; intros.
rewrite sup_ax in H4; auto with *.
destruct H4.
assert (xo : isOrd x) by eauto using isOrd_inv.
assert (xle : x ⊆ o) by (apply olts_le; auto).
assert (xle' : x ⊆ int i O) by (transitivity o; trivial).
assert (F i x (REC (F i) x) ∈
cc_prod (NATi (osucc x)) (fun n => El (int (V.cons n (V.cons (osucc x) i)) U))).
apply ty_fix_body with (1:=H); trivial.
apply ole_lts; auto.
apply fix_typ with (1:=H); trivial.
assert (F i o (NATREC (F i) o) ∈
cc_prod (NATi (osucc o)) (fun n => El (int (V.cons n (V.cons (osucc o) i)) U))).
apply ty_fix_body with (1:=H).
apply ole_lts; trivial.
apply fix_typ with (1:=H); trivial.
rewrite cc_eta_eq with (1:=H6) in H5.
unfold F at 1 in H7; rewrite cc_eta_eq with (1:=H7).
rewrite cc_lam_def in H5|-*.
destruct H5.
destruct H8.
exists x0.
revert H5; apply TI_mono; auto with *.
apply osucc_mono; auto.
exists x1; trivial.
revert H8; apply eq_elim.
do 2 red in stab.
apply stab with (I.cons daimon (I.cons daimon j)) (I.cons daimon (I.cons daimon j)).
apply val_push_fun.
apply val_push_ord; trivial.
apply val_mono_refl; trivial.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
discriminate.
split;[|apply varSAT].
unfold inX,prod; rewrite El_def.
eapply eq_elim.
2:eapply fix_typ with (1:=H); auto.
apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H10; reflexivity.
split;[|apply varSAT].
unfold inX,prod; rewrite El_def.
eapply eq_elim.
2:eapply fix_typ with (1:=H); auto.
apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H10; reflexivity.
red; intros.
apply fix_irr with (1:=H); auto with *.
simpl in H8; rewrite El_def in H8; trivial.
simpl; rewrite El_def; trivial.
do 2 red; intros; apply cc_app_morph; auto with *.
do 2 red; intros; apply cc_app_morph; auto with *.
apply sup_incl with (F:=fun o'=>F i o'(REC (F i) o')); auto with *.
apply lt_osucc; trivial.
Qed.
Lemma nat_fix_eqn : ∀ i j,
val_ok e i j ->
NATREC (F i) (int i O) ==
cc_lam (NATi (int i O))
(fun x => cc_app (F i (int i O) (NATREC (F i) (int i O))) x).
intros.
destruct tyord_inv with (2:=ty_O) (3:=H); trivial.
apply NATREC_eqn with
(ord:=int i O)
(U:=fun o x => int (V.cons x (V.cons o i)) U); auto.
admit.
admit.
admit.
Qed.
Lemma equiv_piSAT_piNAT o B B' f:
isOrd o ->
(∀ n, n ∈ NATi o -> eqSAT (Real (B n) (f n)) (B' n)) ->
eqSAT (piSAT (mkTY (NATi o) cNAT) B f)
(piNATi (fun n => prodSAT (cNAT n) (B' n)) o).
intros.
red; intro.
unfold piSAT, piNATi.
apply interSAT_morph.
split; intros.
destruct x as (n,xty); simpl proj1_sig.
simpl in xty; rewrite El_def in xty.
exists (exist (fun n=>_) n xty); simpl proj1_sig.
apply prodSAT_morph; auto.
rewrite Real_def; auto with *.
intros; apply fam_mrph; trivial.
revert H1; apply NATi_NAT; simpl; auto.
destruct y as (n,xty); simpl proj1_sig.
assert (nty : n ∈ El (mkTY (NATi o) cNAT)).
rewrite El_def; trivial.
exists (exist (fun n=>_) n nty); simpl proj1_sig.
apply prodSAT_morph; auto.
rewrite Real_def; auto with *.
intros; apply fam_mrph; trivial.
revert H1; apply NATi_NAT; simpl; auto.
Qed.
Lemma typ_nat_fix :
typ e (NatFix O M) (Prod (NatI O) (subst_rec O 1 U)).
red; intros.
destruct tyord_inv with (2:=ty_O)(3:=H); trivial.
apply in_int_intro.
2:discriminate.
2:discriminate.
assert (int i (NatFix O M) ∈ El(int i (Prod (NatI O) (subst_rec O 1 U)))).
rewrite intProd_eq.
eapply eq_elim.
2:simpl.
2:apply fix_typ with (1:=H); auto with *.
unfold prod; rewrite El_def; apply cc_prod_ext.
simpl; rewrite El_def; auto with *.
red; intros.
rewrite int_subst_rec_eq.
apply El_morph.
apply int_morph; auto with *.
intros [|[|k]]; try reflexivity.
exact H3.
split; trivial.
rewrite intProd_eq.
rewrite Real_prod; trivial.
simpl tm.
unfold piSAT.
assert (inSAT (NATFIX (Lc.Abs (tm (Lc.ilift (I.cons (tm j O) j)) M)))
(piNATi (fun n => prodSAT (cNAT n)
(Real (int (V.cons n (V.cons (int i O) i)) U)
(cc_app (NATREC (F i) (int i O)) n))) (int i O))).
apply NATFIX_sat with (X:=fun o n => Real (int (V.cons n (V.cons o i)) U)
(cc_app (NATREC (F i) o) n)); trivial.
red; intros.
red in fx_sub_U.
apply fx_sub_U with (V.cons n (V.cons y i))
(I.cons daimon (I.cons daimon j)) (I.cons daimon (I.cons daimon j)).
apply val_push_var; auto with *.
4:discriminate.
apply val_push_ord; auto with *.
4:discriminate.
apply val_mono_refl; trivial.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
transitivity y'; trivial.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
rewrite realNati_def.
2:simpl; auto.
split;[|apply varSAT].
simpl.
revert H7; apply TI_incl; auto with *.
rewrite realNati_def.
2:simpl; auto.
split;[|apply varSAT].
simpl.
revert H7; apply TI_incl; auto with *.
apply isOrd_plump with y'; auto with *.
apply lt_osucc; trivial.
rewrite <- fix_irr with (1:=H) (o:=y); auto.
split; trivial.
unfold inX.
apply cc_prod_elim with (dom:=NATi y) (F:=fun n=>El(int(V.cons n (V.cons y i))U)); trivial.
apply fix_typ with (1:=H); trivial.
transitivity y'; trivial.
apply interSAT_intro.
exists (int i O); auto.
apply lt_osucc; auto.
intros.
destruct x as (o',?); simpl proj1_sig.
cbv zeta.
apply prodSAT_intro; intros.
assert (val_ok (Prod (NatI(Ref 0)) U::OSucct O::e)
(V.cons (NATREC (F i) o') (V.cons o' i)) (I.cons v (I.cons (tm j O) j))).
apply vcons_add_var; auto.
3:discriminate.
apply vcons_add_var; auto.
2:discriminate.
split.
unfold inX; simpl; rewrite El_def; trivial.
simpl int; rewrite Real_def; auto with *.
apply ty_O in H.
apply in_int_sn in H; trivial.
rewrite intProd_eq.
assert (NATREC (F i) o' ∈ cc_prod (NATi o')
(fun x => El(int(V.cons x(V.cons o' i)) U))).
apply fix_typ with (1:=H); trivial.
eauto using isOrd_inv.
apply olts_le in i0; trivial.
split.
unfold inX, prod; rewrite El_def.
revert H4; apply eq_elim; apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H5; reflexivity.
rewrite Real_prod.
revert H3; apply equiv_piSAT_piNAT; eauto using isOrd_inv.
intros.
reflexivity.
red; intros.
rewrite H6; reflexivity.
eapply eq_elim.
2:simpl.
2:apply fix_typ with (1:=H); auto with *.
2: eauto using isOrd_inv.
2: apply olts_le; trivial.
unfold prod; rewrite El_def; apply cc_prod_ext.
simpl; rewrite El_def; auto with *.
red; intros.
rewrite H6; reflexivity.
red in ty_M; specialize ty_M with (1:=H4).
apply in_int_not_kind in ty_M.
2:discriminate.
destruct ty_M.
replace (Lc.subst v (tm (Lc.ilift (I.cons (tm j O) j)) M))
with (tm (I.cons v (I.cons (tm j O) j)) M).
rewrite intProd_eq in H6.
rewrite Real_prod in H6; trivial.
revert H6; apply equiv_piSAT_piNAT.
eauto using isOrd_inv.
intros.
apply Real_morph.
rewrite int_lift_rec_eq.
rewrite int_subst_rec_eq.
rewrite int_lift_rec_eq.
apply int_morph; auto with *.
intros [|[|k]]; try reflexivity.
compute; fold minus.
replace (k-0) with k; auto with *.
symmetry; apply fix_eqn with (1:=H); auto.
eauto using isOrd_inv.
apply olts_le; trivial.
red; intros.
rewrite H8; reflexivity.
unfold Lc.subst; rewrite <- tm_substitutive.
apply tm_morph; auto with *.
intros [|[|k]].
unfold Lc.ilift,I.cons; simpl.
rewrite Lc.lift0; trivial.
unfold Lc.ilift,I.cons; simpl.
rewrite Lc.simpl_subst; trivial.
rewrite Lc.lift0; trivial.
unfold Lc.ilift,I.cons; simpl.
rewrite Lc.simpl_subst; trivial.
rewrite Lc.lift0; trivial.
revert H3; apply interSAT_morph_subset.
simpl; intros.
rewrite El_def.
reflexivity.
intros; simpl proj1_sig.
apply prodSAT_morph.
red; intros.
unfold int,NatI,iint.
rewrite Real_def; auto.
intros.
apply fam_mrph; auto with *.
revert H3; apply NATi_NAT; auto.
simpl.
rewrite int_subst_rec_eq.
apply Real_morph; [|reflexivity].
apply int_morph; auto with *.
intros [|[|k]].
reflexivity.
reflexivity.
reflexivity.
red; intros.
rewrite H4; reflexivity.
Qed.
Lemma nat_fix_eq : ∀ N,
typ e N (NatI O) ->
eq_typ e (App (NatFix O M) N)
(App (subst O (subst (lift 1 (NatFix O M)) M)) N).
red; intros.
unfold eqX.
change
(app (NATREC (F i) (int i O)) (int i N) ==
app (int i (subst O (subst (lift 1 (NatFix O M)) M))) (int i N)).
do 2 rewrite <- int_subst_eq.
rewrite int_cons_lift_eq.
rewrite nat_fix_eqn with (1:=H0); trivial.
rewrite cc_beta_eq.
reflexivity.
do 2 red; intros.
rewrite H2; reflexivity.
red in H; specialize H with (1:=H0).
apply in_int_not_kind in H.
destruct H.
unfold inX in H; simpl in H; rewrite El_def in H; trivial.
discriminate.
Qed.
Lemma nat_fix_extend :
fx_subval E O ->
fx_extends E (NatI O) (NatFix O M).
intro subO.
do 2 red; intros.
simpl in H0; rewrite El_def in H0.
assert (isval := proj1 H).
assert (isval' := proj1 (proj2 H)).
assert (oo: isOrd (int i O)).
destruct tyord_inv with (2:=ty_O) (3:=isval); trivial.
assert (oo': isOrd (int i' O)).
destruct tyord_inv with (2:=ty_O) (3:=isval'); trivial.
assert (inclo: int i O ⊆ int i' O).
apply subO in H; trivial.
clear subO.
change (cc_app (NATREC (F i) (int i O)) x == cc_app (NATREC (F i') (int i' O)) x).
revert x H0.
elim oo using isOrd_ind; intros.
apply TI_elim in H3; auto.
destruct H3 as (o',?,?).
assert (o_o' : isOrd o') by eauto using isOrd_inv.
rewrite <- TI_mono_succ in H4; auto with *.
rewrite <- fix_irr with (1:=isval) (o:=osucc o'); auto.
rewrite fix_eqn with (1:=isval); auto.
rewrite <- fix_irr with (1:=isval') (o:=osucc o'); auto with *.
rewrite fix_eqn with (1:=isval'); auto.
do 2 red in stab.
apply stab with (I.cons daimon (I.cons daimon j)) (I.cons daimon (I.cons daimon j')).
apply val_push_fun.
apply val_push_ord; auto with *.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
split;[|apply varSAT].
unfold inX; simpl; rewrite El_def; apply ole_lts; auto.
discriminate.
split;[|apply varSAT].
unfold inX,prod; rewrite El_def.
eapply eq_elim.
2:eapply fix_typ with (1:=isval); auto.
apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H6; reflexivity.
split;[|apply varSAT].
unfold inX,prod; rewrite El_def.
eapply eq_elim.
2:eapply fix_typ with (1:=isval'); auto.
apply cc_prod_ext.
simpl; rewrite El_def; reflexivity.
red; intros.
rewrite H6; reflexivity.
red; intros.
simpl in H5; rewrite El_def in H5.
rewrite fix_irr with (1:=isval') (o':=int i' O); auto with *.
simpl; rewrite El_def; trivial.
red; intros.
apply inclo; apply H1.
apply le_lt_trans with o'; trivial.
red; intros.
apply le_lt_trans with o'; trivial.
Qed.
Lemma nat_fix_equals :
fx_equals E O ->
fx_equals E (NatFix O M).
red; intros.
assert (fxs: fx_subval E O).
apply fx_equals_subval; trivial.
apply nat_fix_extend in fxs.
red in fxs.
specialize fxs with (1:=H0).
apply fcompat_typ_eq with (3:=fxs).
eapply cc_prod_is_cc_fun.
assert (h := typ_nat_fix _ _ (proj1 H0)).
apply in_int_not_kind in h.
2:discriminate.
destruct h.
rewrite intProd_eq in H1.
unfold inX, prod in H1; rewrite El_def in H1.
eexact H1.
setoid_replace (int i (NatI O)) with (int i' (NatI O)).
eapply cc_prod_is_cc_fun.
assert (h := typ_nat_fix _ _ (proj1 (proj2 H0))).
apply in_int_not_kind in h.
2:discriminate.
destruct h.
rewrite intProd_eq in H1.
unfold inX, prod in H1; rewrite El_def in H1.
eexact H1.
do 2 red.
assert (h:= H _ _ _ _ H0).
apply mkTY_ext.
rewrite h; reflexivity.
intros; apply fam_mrph; auto.
revert H1; apply NATi_NAT; auto.
destruct tyord_inv with (2:=ty_O) (3:=proj1 H0); trivial.
Qed.
End NatFixRules.
Print Assumptions typ_nat_fix.
Lemma typ_nat_fix' : ∀ infty e O U M T,
T <> kind ->
isOrd infty ->
typ e O (Ordt infty) ->
typ (Prod (NatI (Ref 0)) U :: OSucct O :: e) M
(Prod (NatI (OSucc (Ref 1)))
(lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U)))) ->
fx_extends (push_fun (push_ord (tinj e) (OSucct O)) (NatI (Ref 0)) U)
(NatI (OSucc (Ref 1))) M ->
fx_sub (push_var (push_ord (tinj e) (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
sub_typ e (Prod (NatI O) (subst_rec O 1 U)) T ->
typ e (NatFix O M) T.
intros.
apply typ_subsumption with (Prod (NatI O) (subst_rec O 1 U)); auto.
2:discriminate.
change e with (tenv (tinj e)).
apply typ_nat_fix with (infty:=infty); trivial.
Qed.
Compound judgements : typing + variance
Definition typ_ext e M A B :=
fx_extends e A M /\ typ (tenv e) M (Prod A B).
Definition typ_mono e M :=
fx_sub e M /\ typs (tenv e) M.
Definition typ_monoval e M T :=
fx_subval e M /\ typ (tenv e) M T.
Definition typ_impl e M T :=
fx_equals e M /\ typ (tenv e) M T.
Instance typ_impl_morph e : Proper (eq_trm ==> eq_trm ==> iff) (typ_impl e).
apply morph_impl_iff2; auto with *.
do 4 red; intros.
destruct H1; split.
red; intros.
rewrite <- H; eauto.
rewrite <- H; rewrite <- H0; eauto.
Qed.
Lemma typ_var_impl : ∀ e n t T,
spec_var e n = false ->
nth_error (tenv e) n = value t ->
t <> kind ->
T <> kind ->
sub_typ (tenv e) (lift (S n) t) T ->
typ_impl e (Ref n) T.
intros.
split.
apply fx_eq_noc; apply noc_var; trivial.
apply typ_subsumption with (lift (S n) t); trivial.
apply typ_var; trivial.
destruct t as [(t,tm)|]; simpl in *; auto.
discriminate.
Qed.
Lemma impl_abs : ∀ e s1 U T T' M,
T <> kind ->
U <> kind ->
s1=prop \/ s1=kind ->
eq_typ (tenv e) T T' ->
typ_impl e T s1 ->
typ_impl (push_var e T) M U ->
typ_impl e (Abs T M) (Prod T' U).
intros.
destruct H3; destruct H4.
split.
apply fx_eq_abs; trivial.
apply typ_conv with (Prod T U); auto.
apply typ_abs; trivial.
destruct H1; subst s1; red; auto.
apply eq_typ_prod; trivial.
reflexivity.
discriminate.
discriminate.
Qed.
Lemma impl_app : ∀ e u v V Ur T,
T <> kind ->
V <> kind ->
Ur <> kind ->
sub_typ (tenv e) (subst v Ur) T ->
typ_impl e u (Prod V Ur) ->
typ_impl e v V ->
typ_impl e (App u v) T.
intros.
destruct H3.
destruct H4.
split.
apply fx_eq_app; trivial.
apply typ_subsumption with (subst v Ur); trivial.
apply typ_app with V; auto.
destruct Ur as [(Ur,Urm)|]; simpl; trivial.
discriminate.
Qed.
Lemma NATi_fx_sub : ∀ e o O,
isOrd o ->
typ_monoval e O (Ordt o) ->
fx_sub e (NatI O).
destruct 2.
apply NATi_sub with (o:=o); trivial.
Qed.
Lemma OSucc_fx_sub : ∀ e O o,
isOrd o ->
typ_monoval e O (Ordt o)->
typ_monoval e (OSucc O) (Ordt (osucc o)).
destruct 2.
split.
apply OSucc_sub; trivial.
red; simpl; intros.
apply in_int_intro; try discriminate.
assert (osucc (int i O) ∈ El (int i (Ordt (osucc o)))).
simpl; rewrite El_def.
apply lt_osucc_compat; trivial.
destruct tyord_inv with (2:=H1)(3:=H2) as (_,(?,_)); trivial.
split; trivial.
unfold int at 1, Ordt, cst, iint.
rewrite Real_def; auto with *.
assert (h:= H1 _ _ H2).
apply in_int_sn in h.
simpl; trivial.
simpl.
apply lt_osucc_compat; trivial.
destruct tyord_inv with (2:=H1)(3:=H2) as (_,(?,_)); trivial.
Qed.
Lemma typ_var_mono : ∀ e n t T,
ords e n = true ->
nth_error (tenv e) n = value t ->
T <> kind ->
t <> kind ->
sub_typ (tenv e) (lift (S n) t) T ->
typ_monoval e (Ref n) T.
intros.
split.
apply var_sub; trivial.
apply typ_subsumption with (lift (S n) t); trivial.
apply typ_var; trivial.
destruct t as [(t,tm)|]; simpl in *; auto.
discriminate.
Qed.
Lemma ext_abs : ∀ e U T M,
T <> kind ->
U <> kind ->
typ_mono e T ->
typ_impl (push_var e T) M U ->
typ_ext e (Abs T M) T U.
intros.
destruct H1; destruct H2; split.
apply fx_abs with U; trivial.
apply typ_abs; trivial.
Qed.
Lemma impl_call : ∀ e n x t u T,
ords e n = false ->
fixs e n = Some t ->
T <> kind ->
t <> kind ->
u <> kind ->
nth_error (tenv e) n = value (Prod t u) ->
sub_typ (tenv e) (subst x (lift_rec (S n) 1 u)) T ->
typ_impl e x (lift (S n) t) ->
typ_impl e (App (Ref n) x) T.
intros.
destruct H6.
assert (typ (tenv e) (Ref n) (Prod (lift (S n) t) (lift_rec (S n) 1 u))).
apply typ_var0; rewrite H4; split;[discriminate|].
apply sub_refl.
admit.
split.
apply fx_eq_rec_call with t (lift_rec (S n) 1 u); trivial.
apply typ_subsumption with (subst x (lift_rec (S n) 1 u)); auto.
2:destruct u as [(u,um)|]; trivial.
2:discriminate.
apply typ_app with (lift (S n) t); trivial.
destruct t as [(t,tm)|]; trivial.
discriminate.
destruct u as [(u,um)|]; trivial.
discriminate.
Qed.
Lemma typ_nat_fix'' : ∀ infty e O U M T,
isOrd infty ->
T <> kind ->
sub_typ (tenv e) (Prod (NatI O) (subst_rec O 1 U)) T ->
typ (tenv e) O (Ordt infty) ->
typ_mono (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U)
M (NatI (OSucc (Ref 1)))
(lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
typ (tenv e) (NatFix O M) T.
intros.
destruct H3; destruct H4.
apply typ_subsumption with (2:=H1); trivial.
2:discriminate.
apply typ_nat_fix with infty; trivial.
Qed.
Lemma typ_ext_fix : ∀ eps e O U M,
isOrd eps ->
typ_monoval e O (Ordt eps) ->
typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U) M
(NatI (OSucc (Ref 1))) (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
fx_sub (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
typ_ext e (NatFix O M) (NatI O) (subst_rec O 1 U).
intros eps e O U M eps_ord tyO tyM tyU.
destruct tyO as (inclO,tyO).
destruct tyM as (extM,tyM).
assert (tyF: typ (tenv e) (NatFix O M) (Prod (NatI O) (subst_rec O 1 U))).
apply typ_nat_fix with eps; trivial.
split; trivial.
apply nat_fix_extend with eps U; trivial.
Qed.
Lemma typ_impl_fix : ∀ eps e O U M,
isOrd eps ->
typ_impl e O (Ordt eps) ->
typ_ext (push_fun (push_ord e (OSucct O)) (NatI (Ref 0)) U) M
(NatI (OSucc (Ref 1))) (lift_rec 1 1 (subst_rec (OSucc (Ref 0)) 1 (lift_rec 1 2 U))) ->
fx_sub (push_var (push_ord e (OSucct O)) (NatI (OSucc (Ref 0)))) U ->
typ_impl e (NatFix O M) (Prod (NatI O) (subst_rec O 1 U)).
intros eps e O U M eps_ord tyO tyM tyU.
destruct tyO as (inclO,tyO).
destruct tyM as (extM,tyM).
assert (tyF: typ (tenv e) (NatFix O M) (Prod (NatI O) (subst_rec O 1 U))).
apply typ_nat_fix with eps; trivial.
split; trivial.
apply nat_fix_equals with eps U; trivial.
Qed.