conats in JonPRL built from nats and \bigcap

conat.jonprl

Operator iterate : (0; 1; 0).
[iterate(N; F; B)] =def= [natrec(N; B; _.x.so_apply(F; x))].

Operator top : ().
[top] =def= [⋂(void; _.void)].

Theorem top-is-top :
  [⋂(base; x.
   ⋂(base; y.
   =(x; y; top)))] {
  unfold <top>; auto
}.

Operator conatF : (0).
[conatF(X)] =def= [+(unit; X)].

Operator conat : ().
[conat] =def= [⋂(nat; n.iterate(n; x.conatF(x); top))].

Tactic unfolds {
  unfold <conat iterate conatF top>
}.

Tactic rauto {
  *{reduce; auto} ||| May not terminate but shh
}.

Theorem czero : [∈(inl(<>); conat)] {
  refine <unfolds>; refine <rauto>; elim #1; refine <rauto>
}.

Theorem csucc : [⋂(conat; x. ∈(inr(x); conat))] {
  refine <unfolds>; auto;
  elim #2; focus 1 #{elim #1 [n']};
  refine <rauto>;
  hyp-subst ← #6 [h.=(h; h; natrec(n'; ⋂(void; _.void); _.x.+(unit;x)))];
  refine <rauto>
}.


Operator Y : (0).
[Y(f)] =def= [ap(λ(x.ap(f;ap(x;x)));λ(x.ap(f;ap(x;x))))].

Operator omega : ().
[omega] =def= [Y(λ(x.inr(x)))].

Theorem omega-wf : [∈(omega; conat)] {
  refine <unfolds>; unfold <omega Y>; auto; elim #1;
  focus 0 #{reduce 1; auto};
  csubst [ceq(ap(λ(x.ap(λ(x.inr(x));ap(x;x)));λ(x.ap(λ(x.inr(x));ap(x;x))));
              inr(ap(λ(x.ap(λ(x.inr(x));ap(x;x)));λ(x.ap(λ(x.inr(x));ap(x;x))))))]
         [h.=(h;h; natrec(succ(n'); ⋂(void; _. void); _.x.+(unit; x)))];
  [step; step; auto, reduce 1; auto]
}.