Library SATnat

Saturated sets constructions related to natural numbers: interpreting constructors, dependent pattern-matching and fixpoint. Also support size annotations.

Require Import basic Can Sat.
Require Import ZF ZFind_nat.
Module Lc:=Lambda.

A family is a realizability relation for natural numbers

Record family := mkFam {
  fam :> set -> SAT;
  fam_mrph : ∀ x y, x ∈ NAT -> x == y -> eqSAT (fam x) (fam y)
}.

Definition dflt_family : family.
exists (fun _ => snSAT).
Defined.

Definition eqfam (A B:family) :=
  ∀ x y, x ∈ NAT -> x == y -> eqSAT (A x) (B y).

Denotation of the intersection of (F(n)) expressions when n:Nat

Definition piNAT F :=
interSAT (fun p:{n|n ∈ NAT } => F (proj1_sig p)).

Lemma piNAT_ax t F :
inSAT t (piNAT F) <-> sn t /\ ∀ n, n ∈ NAT -> inSAT t (F n).

Quantification over families

Definition piFAM F :=
interSAT (fun P:family => F P).

Lemma piFAM_ax t F :
inSAT t (piFAM F) <-> ∀ P:family, inSAT t (F P).

Functional applying constructors of Nat to A

Definition fNAT (A:family) (k:set) :=
  piFAM(fun P =>
        prodSAT (P ZERO)
       (prodSAT (piNAT(fun n => prodSAT (A n) (prodSAT (P n) (P (SUCC n)))))
                (P k))).

Lemma fNAT_morph : ∀ A B, eqfam A B ->
  ∀ x y, x ∈ NAT -> x == y -> eqSAT (fNAT A x) (fNAT B y).

Definition fNATf (A:family) : family.
exists (fNAT A).
Defined.

Lemma fNAT_def : ∀ t A k,
  inSAT t (fNAT A k) <->
  ∀ (P:family) f g,
  inSAT f (P ZERO) ->
  inSAT g (piNAT(fun n => prodSAT (A n) (prodSAT (P n) (P (SUCC n))))) ->
  inSAT (Lc.App2 t f g) (P k).

Lemma fNAT_mono : ∀ (A B:family),
  (∀ k, inclSAT (A k) (B k)) -> ∀ k, inclSAT (fNAT A k) (fNAT B k).

Realizability relation of Nat: fixpoint of fNAT

cNAT is intersection of all families that are post-fixpoint (that is, P s.t. fNAT P included in P)

Definition cNAT : family.
exists (fun n =>
interSAT (fun P:{P:family |∀ k, inclSAT (fNAT P k) (P k)} =>
proj1_sig P n)).
Defined.

Lemma cNAT_post : ∀ k, inclSAT (fNAT cNAT k) (cNAT k).

Lemma cNAT_pre : ∀ k, inclSAT (cNAT k) (fNAT cNAT k).

Fixpoint equation

Lemma cNAT_eq : ∀ k, eqSAT (cNAT k) (fNAT cNAT k).

Constructors

Interp of 0

Definition ZE := Lc.Abs (Lc.Abs (Lc.Ref 1)).

Lemma fNAT_ZE : ∀ A, inSAT ZE (fNAT A ZERO).

ZE realizes 0

Lemma cNAT_ZE : inSAT ZE (cNAT ZERO).

Interp of successor. Unlike in system F the function corresponding to the successor expects two arguments: the predecessor and the usual result of recursive call. S(n) is (fun f g => g n (n f g)) instead of the usual (fun f g => g (n f g)).

Definition SU := Lc.Abs (Lc.Abs (Lc.Abs
    (Lc.App2 (Lc.Ref 0) (Lc.Ref 2) (Lc.App2 (Lc.Ref 2) (Lc.Ref 1) (Lc.Ref 0))))).

Lemma fNAT_SU : ∀ (A:family) n t,
  n ∈ NAT ->
  inSAT t (A n) ->
  inSAT t (fNAT A n) ->
  inSAT (Lc.App SU t) (fNAT A (SUCC n)).

SU realizes the successor

Lemma cNAT_SU : ∀ n t, n ∈ NAT -> inSAT t (cNAT n) -> inSAT (Lc.App SU t) (cNAT (SUCC n)).

Pattern-matching

Definition NCASE f g n :=
  Lc.App2 n f (Lc.Abs (Lc.Abs (Lc.App (Lc.lift 2 g) (Lc.Ref 1)))).

Lemma NCASE_sim_0 f g :
  Lc.redp (NCASE f g ZE) f.

Lemma NCASE_sim_S f g n :
  Lc.redp (NCASE f g (Lc.App SU n)) (Lc.App g n).

Lemma NCASE_fNAT f g n k (A B:family) :
  k ∈ NAT ->
  inSAT n (fNAT A k) ->
  inSAT f (B ZERO) ->
  inSAT g (piNAT(fun m => prodSAT (A m) (B (SUCC m)))) ->
  inSAT (NCASE f g n) (B k).

Structural fixpoint:

NATFIX m n --> m (NATFIX m) n when n is a constructor. let G m := "\n. (match n with | 0 => m | S _ => m end) m n" let G m := \n. n m (\_.\_.m) m n G m -/-> ; G m 0 --> m 0 ; G m (S k) --> m (S k) NATFIX m n := G (\x. m (G x)) n > (\x. m (G x)) (\x. m (G x)) n > m (G (\x. m (G x))) n == m (NATFIX m) n

Guard the self-application of m (which would produce a non-strongly normalizing term) by a natural number.

Definition G m :=
Lc.Abs (Lc.App2 (Lc.App2 (Lc.Ref 0) (Lc.lift 1 m) (Lc.Abs (Lc.Abs (Lc.lift 3 m)))) (Lc.lift 1 m) (Lc.Ref 0)).

(G m n) reduces to (m m n) when n is a constructor. Note that n need not be closed.

Lemma G_sim : ∀ m n,
  n = ZE \/ (exists t1 t2, n = Lc.Abs (Lc.Abs (Lc.App2 (Lc.Ref 0) t1 t2))) ->
  Lc.redp (Lc.App (G m) n) (Lc.App2 m m n).

Lemma G_sat A k m t X :
  k ∈ NAT ->
  inSAT t (fNAT A k) ->
  inSAT (Lc.App2 m m t) X ->
  inSAT (Lc.App (G m) t) X.

Lemma sn_G_inv m : Lc.sn (G m) -> Lc.sn m.

Definition NATFIX m :=
  G (Lc.Abs (Lc.App (Lc.lift 1 m) (G (Lc.Ref 0)))).

NATFIX reduces as a fixpoint combinator when applied to a constructor

Lemma NATFIX_sim : ∀ m n,
  n = ZE \/ (exists t1 t2, n = Lc.Abs (Lc.Abs (Lc.App2 (Lc.Ref 0) t1 t2))) ->
  Lc.redp (Lc.App (NATFIX m) n) (Lc.App2 m (NATFIX m) n).

Definition piNATi F o :=
  interSAT (fun p:{n|n ∈ NATi o } => F (proj1_sig p)).

Lemma piNATi_ax t F o :
  inSAT t (piNATi F o) <-> sn t /\ ∀ n, n ∈ NATi o -> inSAT t (F n).

Require Import ZFord.

The guard is needed mainly here: NATFIX m does not reduce

Lemma sn_natfix o m X :
  isOrd o ->
  inSAT m (interSAT (fun o':{o'|o' ∈ osucc o } => let o':=proj1_sig o' in
        prodSAT (piNATi(fun n => prodSAT (cNAT n) (X o' n)) o')
                (piNATi(fun n => prodSAT (cNAT n) (X (osucc o') n)) (osucc o')))) ->
  sn (NATFIX m).

Lemma NATFIX_sat : ∀ o m X,
  isOrd o ->
  (∀ y y' n, isOrd y -> isOrd y' -> y ⊆ y' -> y' ⊆ o -> n ∈ NATi y ->
   inclSAT (X y n) (X y' n)) ->
  inSAT m (interSAT (fun o':{o'|o' ∈ osucc o } => let o':=proj1_sig o' in
        prodSAT (piNATi(fun n => prodSAT (cNAT n) (X o' n)) o')
                (piNATi(fun n => prodSAT (cNAT n) (X (osucc o') n)) (osucc o')))) ->
  inSAT (NATFIX m) (piNATi(fun n => prodSAT (cNAT n) (X o n)) o).