peano.mm0

delimiter $ ( ) ~ { } , $;
--| Well formed formulas, or propositions - true or false.
strict provable sort wff;
--| Implication: if p, then q.
term im (p q: wff): wff; infixr im: $->$ prec 25;
--| Negation: p is false.
term not (p: wff): wff; prefix not: $~$ prec 41;

--| Axiom 1 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_1 (a b: wff): $ a -> b -> a $;
--| Axiom 2 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $;
--| Axiom 3 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $;
--| Modus ponens: from `a -> b` and `a`, infer `b`.
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;

--| Conjunction: `a` and `b` are both true.
def an (a b: wff): wff = $ ~(a -> ~b) $;
infixl an: $/\$ prec 34;

--| If and only if: `a` implies `b`, and `b` implies `a`.
def iff (a b: wff): wff = $ (a -> b) /\ (b -> a) $;
infixl iff: $<->$ prec 20;

--| Disjunction: either `a` is true or `b` is true.
def or (a b: wff): wff = $ ~a -> b $;
infixl or: $\/$ prec 30;

--| Selection: `ifp p a b` is equivalent to `a` if `p` is true,
--| and equivalent to `b` if `p` is false.
def ifp (p a b: wff): wff;
theorem ifppos (p a b: wff): $ p -> (ifp p a b <-> a) $;
theorem ifpneg (p a b: wff): $ ~p -> (ifp p a b <-> b) $;

--| The constant `true`.
term tru: wff; prefix tru: $T.$ prec max;
--| `true` is true.
axiom itru: $ T. $;
--| The constant `false`.
def fal: wff = $ ~T. $; prefix fal: $F.$ prec max;

--| The sort of natural numbers, or nonnegative integers.
--| In Peano Arithmetic this is the domain of discourse,
--| the basic sort over which quantifiers range.
sort nat;

--| The for-all quantifier. `A. x p` means
--| "for all natural numbers `x`, `p` holds",
--| where `(p: wff x)` in the declaration indicates that `p` may contain
--| free occurrences of variable `x` that are bound by this quantifier.
term al {x: nat} (p: wff x): wff; prefix al: $A.$ prec 41;

--| The exists quantifier. `E. x p` means
--| "there is a natural number `x`, such that `p` holds",
--| where `(p: wff x)` in the declaration indicates that `p` may contain
--| free occurrences of variable `x` that are bound by this quantifier.
def ex {x: nat} (p: wff x): wff = $ ~(A. x ~p) $;
prefix ex: $E.$ prec 41;

--| Equality of natural numbers: `a = b`
--| means that `a` and `b` have the same value.
term eq (a b: nat): wff; infixl eq: $=$ prec 50;

--| The axiom of generalization. If `|- p` is derivable
--| (the lack of a precondition means this is a proof in the empty context),
--| then `p` is universally true, so `|- A. x p` is also true.
axiom ax_gen {x: nat} (p: wff x): $ p $ > $ A. x p $;

--| Axiom 4 for predicate logic: forall distributes over implication.
axiom ax_4 {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $;

--| Axiom 5 for predicate logic: If `p` does not contain an occurrence of `x`
--| (note that `(p: wff)` in contrast to `(p: wff x)` means that `p` cannot
--| depend on variable `x`), then `p` implies `A. x p`
--| because the quantifier is trivial.
axiom ax_5 {x: nat} (p: wff): $ p -> A. x p $;

--| Axiom 6 for predicate logic: for any term `a` (which cannot depend on `x`),
--| there exists an `x` which is equal to `a`.
axiom ax_6 (a: nat) {x: nat}: $ E. x x = a $;

--| Axiom 7 for predicate logic: equality satisfies the euclidean property
--| (which implies symmetry and transitivity, and reflexivity given axiom 6).
axiom ax_7 (a b c: nat): $ a = b -> a = c -> b = c $;

-- axiom 9 has been proven redundant; axiom 8 is displaced below

--| Axiom 10 for predicate logic: `x` is bound in `~(A. x p)`, so we can
--| safely introduce a `A. x` quantifier. (This axiom is used to internalize
--| the notion of "bound in" when axiom 5 does not apply.)
axiom ax_10 {x: nat} (p: wff x): $ ~(A. x p) -> A. x ~(A. x p) $;

--| Axiom 11 for predicate logic: forall quantifiers commute.
axiom ax_11 {x y: nat} (p: wff x y): $ A. x A. y p -> A. y A. x p $;

--| Axiom 12 for predicate logic: If `x` is some fixed `a` and `p(x)` holds,
--| then for all `x` which are equal to `a`, `p(x)` holds. This expresses the
--| substitution property of `=`, but the name shadowing on `x` allows us to
--| express this without changing `p`,
--| because we haven't defined proper substitution yet.
axiom ax_12 {x: nat} (a: nat) (p: wff x): $ x = a -> p -> A. x (x = a -> p) $;

--| Not equal: `a != b` means `a` and `b` are distinct natural numbers.
def ne (a b: nat): wff = $ ~ a = b $; infixl ne: $!=$ prec 50;

--| Proper substitution. `[a / x] p` is `p`, with free occurrences of `x` in
--| `p` replaced by `a`. If we write `p(x)`, this may also be denoted as `p(a)`.
--| (Note that this is only provably equivalent to `p(a)`;
--| `[0 / x] (x < x + y)` is equivalent but not syntactically identical to
--| `0 < 0 + y`, and it requires a rewriting/substitution proof to show.)
def sb (a: nat) {x .y: nat} (p: wff x): wff =
$ A. y (y = a -> A. x (x = y -> p)) $;
notation sb (a: nat) {x: nat} (p: wff x): wff =
  ($[$:41) a ($/$:0) x ($]$:0) p;

--| The sort of sets of natural numbers. Because we are working in
--| Peano Arithmetic, we cannot quantify over variables of this type, and these
--| should be thought of only as sugar for formulas with one free variable.
--| This is a conservative extension of PA.
strict sort set;

--| A "class abstraction" `{x | p(x)}` is the set of natural numbers `x` such that `p(x)` holds.
term ab {x: nat} (p: wff x): set;
notation ab {x: nat} (p: wff x): set = (${$:max) x ($|$:0) p ($}$:0);

--| Given a natural number `a` and a set `A`, `a e. A` (read `e.` as epsilon)
--| means `a` is in the set `A`.
term el (a: nat) (A: set): wff; infixl el: $e.$ prec 50;

--| `a` is in `{x | p(x)}` iff `p(a)` holds.
axiom elab (a: nat) {x: nat} (p: wff x): $ a e. {x | p} <-> [ a / x ] p $;

--| Elementhood respects equality. This is a theorem for most definitions
--| but has to be axiomatized for primitive term constructors like `e.`
--| This is Axiom 8 of predicate logic (which has an instance for every
--| primitive predicate in the language).
axiom ax_8 (a b: nat) (A: set): $ a = b -> a e. A -> b e. A $;

--| `A == B` is equality for sets. Two sets are equal if they have the
--| same elements.
def eqs (A B: set) {.x: nat}: wff = $ A. x (x e. A <-> x e. B) $;
infixl eqs: $==$ prec 50;

--| `A C_ B` means `A` is a subset of `B`.
def subset (A B: set) (.x: nat): wff = $ A. x (x e. A -> x e. B) $;
infixl subset: $C_$ prec 50;

--| `A i^i B` is the intersection of sets `A` and `B`.
def Inter (A B: set) (.x: nat): set = $ {x | x e. A /\ x e. B} $;
infixl Inter: $i^i$ prec 70;

--| `A u. B` is the union of sets `A` and `B`.
def Union (A B: set) (.x: nat): set = $ {x | x e. A \/ x e. B} $;
infixl Union: $u.$ prec 65;

--| `Compl A` is the complement of `A`, the set of all natural numbers not in `A`.
def Compl (A: set) (.x: nat): set = $ {x | ~x e. A} $;

--| `Univ`, or `_V` is the set of all natural numbers.
def Univ (.x: nat): set = $ {x | T.} $; prefix Univ: $_V$ prec max;

--| Substitution for sets. `S[a / x] A` is the set `A` when
--| free variable `x` is evaluated at `a`.
def sbs (a: nat) {x .y: nat} (A: set x): set = $ {y | [ a / x ] y e. A} $;
notation sbs (a: nat) {x: nat} (A: set x): set = ($S[$:99) a ($/$:0) x ($]$:0) A;

--| `0` is a natural number.
term d0: nat; prefix d0: $0$ prec max;
--| The successor operation: `suc n` is a natural number when `n` is.
term suc (n: nat): nat;

def d1:  nat = $suc 0$; prefix d1:  $1$  prec max;
def d2:  nat = $suc 1$; prefix d2:  $2$  prec max;
def d3:  nat = $suc 2$; prefix d3:  $3$  prec max;
def d4:  nat = $suc 3$; prefix d4:  $4$  prec max;
def d5:  nat = $suc 4$; prefix d5:  $5$  prec max;
def d6:  nat = $suc 5$; prefix d6:  $6$  prec max;
def d7:  nat = $suc 6$; prefix d7:  $7$  prec max;
def d8:  nat = $suc 7$; prefix d8:  $8$  prec max;
def d9:  nat = $suc 8$; prefix d9:  $9$  prec max;
def d10: nat = $suc 9$; prefix d10: $10$ prec max;

--| Zero is not a successor. Axiom 1 of Peano Arithmetic.
axiom peano1 (a: nat): $ suc a != 0 $;
--| The successor function is injective. Axiom 2 of Peano Arithmetic.
axiom peano2 (a b: nat): $ suc a = suc b <-> a = b $;
--| The induction axiom of Peano Arithmetic. If `p(0)` is true,
--| and `p(x)` implies `p(suc x)` for all `x`, then `p(x)` is true for all `x`.
axiom peano5 {x: nat} (p: wff x):
  $ [ 0 / x ] p -> A. x (p -> [ suc x / x ] p) -> A. x p $;

--| The definite description operator: `the A` is the value `a` such that
--| `A = {a}`, if there is such a value, otherwise `0`.
term the (A: set): nat;
--| The positive case of definite description: `A = {a}` then `the A = a`.
axiom theid {x: nat} (A: set) (a: nat): $ A == {x | x = a} -> the A = a $;
--| The negative case of definite description: `A`` is not a singleton then `the A = 0`.
axiom the0 {x y: nat} (A: set): $ ~E. y A == {x | x = y} -> the A = 0 $;

--| Substitution for numbers. If `b(x)` is an expression denoting a natural number,
--| with free `x`, then `N[a / x] b` is the term `b(a)`.
def sbn (a: nat) {x .y: nat} (b: nat x): nat = $ the {y | [ a / x ] y = b} $;
notation sbn (a: nat) {x: nat} (b: nat x): nat = ($N[$:99) a ($/$:0) x ($]$:0) b;

--| Addition of natural numbers, a primitive term constructor in PA.
term add (a b: nat): nat; infixl add: $+$ prec 64;
--| Multiplication of natural numbers, a primitive term constructor in PA.
term mul (a b: nat): nat; infixl mul: $*$ prec 70;

--| Addition respects equalty.
axiom addeq (a b c d: nat): $ a = b -> c = d -> a + c = b + d $;
--| Multiplication respects equalty.
axiom muleq (a b c d: nat): $ a = b -> c = d -> a * c = b * d $;
--| The base case in the definition of addition.
axiom add0 (a: nat): $ a + 0 = a $;
--| The successor case in the definition of addition.
axiom addS (a b: nat): $ a + suc b = suc (a + b) $;
--| The base case in the definition of multiplication.
axiom mul0 (a: nat): $ a * 0 = 0 $;
--| The successor case in the definition of multiplication.
axiom mulS (a b: nat): $ a * suc b = a * b + a $;

----------------------------------------------------------------------
-- Axioms end here! This completes the axiomatization of Peano Arithmetic,
-- although we will introduce more (conservative) axioms in `peano_hex.mm0`.
-- The rest is definitions needed for downstream files.
----------------------------------------------------------------------

--| (Truncated) subtraction of natural numbers.
--| Note that `a - b = 0` when `a < b`.
def sub (a b: nat) {.x: nat}: nat = $ the {x | b + x = a} $;
infixl sub: $-$ prec 64;

--| `a <= b` means `a` is less than or equal to `b`.
def le (a b .x: nat): wff = $ E. x a + x = b $;
infixl le: $<=$ prec 50;

--| `a < b` means `a` is strictly less than `b`.
def lt (a b: nat): wff = $ suc a <= b $;
infixl lt: $<$ prec 50;

--| `finite A` means `A` is a finite set
--| (here defined as one that is upper bounded by some natural number).
def finite (A: set) (.n .x: nat): wff = $ E. n A. x (x e. A -> x < n) $;

--| `if p a b` is the if-then-else construct:
--| if `p` is true then `a`, else `b`.
def if (p: wff) (a b: nat): nat;
theorem ifpos (p: wff) (a b: nat): $ p -> if p a b = a $;
theorem ifneg (p: wff) (a b: nat): $ ~p -> if p a b = b $;

--| `true n` means `n` is "truthy", that is, nonzero.
def true (n: nat): wff = $ n != 0 $;
--| `bool n` means `n` is "boolean", that is, 0 or 1.
def bool (n: nat): wff = $ n < 2 $;
--| `nat p` turns wff `p` into a natural number: if `p` is true then `1`, else `0`.
def nat (p: wff): nat = $ if p 1 0 $;

--| `min a b` is the smaller of `a` and `b`.
def min (a b: nat): nat = $ if (a < b) a b $;
--| `max a b` is the larger of `a` and `b`.
def max (a b: nat): nat = $ if (a < b) b a $;

--| `a // b` is the quotient on dividing `a` by `b`.
--| (The double slash is used as in python to remind the reader that
--| this is a rounding-down division, not exact division.)
--| Division by 0 is defined and equal to 0.
def div (a b: nat): nat; infixl div: $//$ prec 70;

--| `a % b` is the remainder on dividing `a` by `b`.
--| Modulus by 0 is defined and `a % 0 = a`.
def mod (a b: nat): nat; infixl mod: $%$ prec 70;

theorem div0 (a: nat): $ a // 0 = 0 $;
theorem divmod (a b: nat): $ b * (a // b) + a % b = a $;
theorem modlt (a b: nat): $ b != 0 -> a % b < b $;

--| `a || b` means that `a` divides `b`, or equivalently,
--| `b` is a multiple of `a`.
def dvd (a b .c: nat): wff = $ E. c c * a = b $;
infixl dvd: $||$ prec 50;

--| `b0 n` is `n * 2`.
--| It is named for "bit 0" as in binary representation of numbers.
def b0 (n: nat): nat = $ n + n $;
--| `b1 n` is `n * 2 + 1`.
--| It is named for "bit 1" as in binary representation of numbers.
def b1 (n: nat): nat = $ suc (b0 n) $;
--| `odd n` means `n` is odd, not divisible by 2.
def odd (n: nat): wff = $ n % 2 = 1 $;

--| `a <> b` is the pairing operator `(a, b)`.
--| It is defined using the Cantor pairing function.
--| It is right associative, i.e. `a <> b <> c` means `(a, (b, c))`.
def pr (a b: nat): nat = $ (a + b) * suc (a + b) // 2 + b $;
infixr pr: $<>$ prec 55;
--| The first component of a pair.
def fst (a: nat): nat;
--| The second component of a pair.
def snd (a: nat): nat;

theorem pr0: $ 0 <> 0 = 0 $;
theorem fstpr (a b: nat): $ fst (a <> b) = a $;
theorem sndpr (a b: nat): $ snd (a <> b) = b $;
theorem fstsnd (a: nat): $ fst a <> snd a = a $;

--| `pi11 ((a, b), c) = a`
def pi11 (n: nat): nat = $ fst (fst n) $;
--| `pi12 ((a, b), c) = b`
def pi12 (n: nat): nat = $ snd (fst n) $;
--| `pi21 (a, (b, c)) = b`
def pi21 (n: nat): nat = $ fst (snd n) $;
--| `pi22 (a, (b, c)) = c`
def pi22 (n: nat): nat = $ snd (snd n) $;
--| `pi221 (a, (b, (c, d))) = c`
def pi221 (n: nat): nat = $ fst (pi22 n) $;
--| `pi222 (a, (b, (c, d))) = d`
def pi222 (n: nat): nat = $ snd (pi22 n) $;

--| `isfun A` means `A` is a function,
--| i.e. if `(x,y)` and `(x,z)` are in `A` then `y = z`.
def isfun (A: set) (.a .b .b2: nat): wff =
$ A. a A. b A. b2 (a <> b e. A -> a <> b2 e. A -> b = b2) $;

--| `S\ x, A` is "lambda for relations": `a <> b e. S\ x, A(x)` if `b e. A(a)`.
--| It can be iterated to produce n-ary relations.
--| `S\ x, S\ y, {z | p(x,y,z)}` is the set `S` such that
--| `x <> y <> z e. S` iff `p(x,y,z)`.
def sab {x .z: nat} (A: set x): set = $ {z | snd z e. S[ fst z / x ] A} $;
notation sab {x: nat} (A: set x): set = ($S\$:100) x ($,$:0) A;

--| Indexed disjoint union, a restricted version of `S\`.
--| `a <> b e. X\ x e. A, B(x)` iff `a e. A` and `b e. B(a)`.
def xab {x .z: nat} (A: set) (B: set x): set =
$ {z | fst z e. A /\ snd z e. S[ fst z / x ] B} $;
notation xab {x: nat} (A: set) (B: set x): set =
  ($X\$:100) x ($e.$:50) A ($,$:0) B;

--| `Xp A B` is the cartesian product of sets:
--| `(a,b) e. Xp A B` iff `a e. A` and `b e. B`.
def Xp (A B: set) (.x: nat): set = $ X\ x e. A, B $;

--| The domain of a binary relation:
--| `x e. Dom A` if there exists `y` such that `(x,y) e. A`.
def Dom (A: set) (.x .y: nat): set = $ {x | E. y x <> y e. A} $;
--| The range of a binary relation:
--| `y e. Ran A` if there exists `x` such that `(x,y) e. A`.
def Ran (A: set) (.x .y: nat): set = $ {y | E. x x <> y e. A} $;

--| The image of a relation under a set: `y e. F '' A`
--| if there exists `x e. A` such that `(x,y) e. F`.
def Im (F A: set) (.x .y: nat): set = $ {y | E. x (x e. A /\ x <> y e. F)} $;
infixl Im: $''$ prec 80;

--| The converse of a relation: `(x,y) e. cnv A` if `(y,x) e. A`.
def cnv (A: set) (.x .y: nat): set = $ S\ x, {y | y <> x e. A} $;

--| The relational composition: `(x,z) e. F o> G` if there exists `y` such that
--| `(x,y) e. F` and `(y,z) e. G`. *Warning*: This is also applicable for functions,
--| but it does not match the more conventional right-to-left composition order.
--| `(F o> G) @ x = G @ (F @ x)`. We use an arrow like notation
--| `o>` to remind the reader of this: we apply `F` *then* `G`.
def comp (F G: set) (.x .y .z: nat): set =
$ S\ x, {z | E. y (x <> y e. F /\ y <> z e. G)} $;
infixr comp: $o>$ prec 91;

--| The restriction of a relation to a set: `A |` B` is
--| the set of `(x,y) e. A` such that `y e. B`.
def res (A B: set): set = $ A i^i Xp B _V $;
infixl res: $|`$ prec 54;

--| The lambda operator: `\ x, v(x)` is the set of pairs `(x, v(x))` over
--| all natural numbers `x`.
def lam {x .p: nat} (a: nat x): set = $ {p | E. x p = x <> a} $;
notation lam {x: nat} (a: nat x): set = ($\$:53) x ($,$:0) a;

--| The application operator. If `F` is a function and `x` is a natural number then
--| `F @ x` is `F` evaluated at `x`. That is, it is the value `y`
--| for which `(x,y) e. F`, if there is a unique such number.
def app (F: set) (x .y: nat): nat = $ the {y | x <> y e. F} $;
infixl app: $@$ prec 200;

--| Define a function by cases on a disjoint union.
--| `case A B` is the function such that
--| * `case A B @ b0 n = A @ n`
--| * `case A B @ b1 n = B @ n`
def case (A B: set) (.n: nat): set =
$ \ n, if (odd n) (B @ (n // 2)) (A @ (n // 2)) $;
theorem casel (A B: set) (n: nat): $ case A B @ b0 n = A @ n $;
theorem caser (A B: set) (n: nat): $ case A B @ b1 n = B @ n $;

--| Disjoint union of sets; also `case` for wff-valued functions.
--| * `b0 n e. Sum A B <-> n e. A`
--| * `b1 n e. Sum A B <-> n e. B`
def Sum (A B: set): set;
theorem Suml (A B: set) (n: nat): $ b0 n e. Sum A B <-> n e. A $;
theorem Sumr (A B: set) (n: nat): $ b1 n e. Sum A B <-> n e. B $;

--| Simple recursion operator:
--| * `rec 0 = z`
--| * `rec (n+1) = S (rec n)`
def rec (z: nat) (S: set) (n: nat): nat;
theorem rec0 (z: nat) (S: set): $ rec z S 0 = z $;
theorem recS (z: nat) (S: set) (n: nat):
  $ rec z S (suc n) = S @ rec z S n $;

--| The "bind" operator for the option monad,
--| `obind : Option A -> (A -> Option B) -> Option B`.
--| * `obind none F = none`
--| * `obind (some a) F = F a`
def obind (a: nat) (F: set): nat;
theorem obind0 (F: set): $ obind 0 F = 0 $;
theorem obindS (n: nat) (F: set): $ obind (suc n) F = F @ n $;

--| The power function on natural numbers.
--| * `a ^ 0 = 1`
--| * `a ^ suc b = a * a ^ b`
def pow (a b: nat): nat; infixr pow: $^$ prec 81;
theorem pow0 (a: nat): $ a ^ 0 = 1 $;
theorem powS (a b: nat): $ a ^ suc b = a * a ^ b $;

--| Left shift for natural numbers: `shl a n = a * 2 ^ n`.
def shl (a n: nat): nat = $ a * 2 ^ n $;
--| Right shift for natural numbers: `shr a n = a // 2 ^ n`.
def shr (a n: nat): nat = $ a // 2 ^ n $;

--| Lift a natural number to a set, via `a ~> {x | odd (shr a x)}`.
--| That is, `x e. a` if the `x`'th bit of `a` is 1.
--| This mapping is injective, and surjective onto finite sets,
--| so we can view the sort `nat` as a subtype of `set`
--| consisting of the finite sets.
def ns (a .x: nat): set = $ {x | odd (shr a x)} $; coercion ns: nat > set;
theorem axext (a b: nat): $ a == b -> a = b $;
theorem ellt (a b: nat): $ a e. b -> a < b $;
theorem nel0 (a: nat): $ ~ a e. 0 $;

--| Convert a finite set to a natural number with the same elements.
--| We use this when we wish to construct a natural number
--| from a set expression. It returns a garbage value 0 if the set is not finite.
--| This is the inverse to the `ns` coercion.
def lower (A: set) (.n: nat): nat = $ the {n | n == A} $;
theorem eqlower (A: set): $ finite A <-> A == lower A $;

--| A singleton set `{a}`, as a `nat` because it is always finite.
def sn (a: nat): nat;
theorem elsn (a b: nat): $ a e. sn b <-> a = b $;

--| `ins a b` or `a ; b` is the set `{a} u. b`, the set containing `a`
--| and the elements of `b`. It is finite because `b` is.
def ins (a b: nat): nat; infixr ins: $;$ prec 85;
theorem elins (a b c: nat): $ a e. ins b c <-> a = b \/ a e. c $;

--| `upto n = {x | x < n}` is the set of numbers less than `n`.
def upto (n: nat): nat = $ 2 ^ n - 1 $;
theorem elupto (k n: nat): $ k e. upto n <-> k < n $;

--| `Bool = {x | bool x}` is the set of boolean values (0 and 1).
def Bool: nat = $ 0 ; sn 1 $;
--| `Option A` is the set `A` disjointly extended with an additional element.
--| We use `0` and `suc` in place of the `none` and `some` constructors.
def Option (A: set) (.n: nat): set = $ {n | n = 0 \/ n - 1 e. A} $;

--| `Power A` is the set of all (finite) subsets of `A`.
def Power (A: set) (.x: nat): set = $ {x | x C_ A} $;
--| `power a` is the finite set of all subsets of the finite set `a`.
def power (a: nat): nat = $ lower (Power a) $;

--| `sUnion A` is the set union: the union of all the elements of `A`.
def sUnion (A: set) (.x .y: nat): set = $ {x | E. y (x e. y /\ y e. A)} $;

--| `cons a b`, or `a : b`, is the list cons operator:
--| `cons : A -> List A -> List A`
def cons (a b: nat): nat = $ suc (a <> b) $; infixr cons: $:$ prec 91;

--| `sep n {x | p(x)}` is `{x e. n | p(x)}`,
--| the set of elements of `n` such that `p(x)`. Because it is a subset of an
--| existing finite set `n`, it is also finite.
--| This is analogous to the separation axiom of ZFC.
def sep (n: nat) (A: set): nat;
theorem elsep (n: nat) (A: set) (a: nat): $ a e. sep n A <-> a e. n /\ a e. A $;

--| `Arrow A B` (which has no notation but is denoted `A -> B` in comments)
--| is the set of all (finite) functions from `A` to `B`.
def Arrow (A B: set) (.f: nat): set =
$ {f | isfun f /\ Dom f == A /\ Ran f C_ B} $;

--| `\. x e. a, v(x)` is the finite (restricted) lambda: the regular lambda `\ x, v(x)`
--| restricted to the finite set `a`. Since it is finite, we make it manifestly finite here.
def rlam {x: nat} (a: nat) (v: nat x): nat = $ lower ((\ x, v) |` a) $;
notation rlam {x: nat} (a: nat) (v: nat x): nat = ($\.$:53) x ($e.$:50) a ($,$:0) v;

--| `write F a b`, sometimes denoted `F[a -> b]` is
--| the function which is `b` at `a` and returns `F @ x` for `x != a`.
def write (F: set) (a b .x .y: nat): set =
$ S\ x, {y | ifp (x = a) (y = b) (x <> y e. F)} $;
theorem writeEq (F: set) (a b: nat): $ write F a b @ a = b $;
theorem writeNe (F: set) (a b x: nat): $ x != a -> write F a b @ x = F @ x $;

--| Strong recursion operator:
--| * `srec n = S (srec 0, ..., srec (n-1))`
def srec (S: set) (n: nat): nat;
theorem srecval {i: nat} (S: set) (n: nat):
  $ srec S n = S @ (\. i e. upto n, srec S i) $;

--| Strong recursion operator (for wffs):
--| * `srecp n <-> (srecp 0, ..., srecp (n-1)) e. A`
def srecp (A: set) (n: nat): wff;
theorem srecpval {i: nat} (A: set) (n: nat):
  $ srecp A n <-> n <> sep (upto n) {i | srecp A i} e. A $;

--| The cardinality (number of elements) of a finite set.
def card (s: nat): nat;
theorem card0: $ card 0 = 0 $;
theorem cardS (a s: nat): $ ~a e. s -> card (a ; s) = suc (card s) $;

--| The list recursion operator:
--| * `lrec 0 = z`
--| * `lrec (a : l) = S (a, l, lrec l)`
def lrec (z: nat) (S: set) (n: nat): nat;
theorem lrec0 (z: nat) (S: set): $ lrec z S 0 = z $;
theorem lrecS (z: nat) (S: set) (a b: nat):
  $ lrec z S (a : b) = S @ (a <> b <> lrec z S b) $;

--| The set of members of list `l`: `lmems [a, b, c] = {a, b, c}`.
--|
--| `lmems : List A -> Power A`
def lmems (l: nat): nat;
theorem lmems0: $ lmems 0 = 0 $;
theorem lmemsS (a l: nat): $ lmems (a : l) = a ; lmems l $;

--| `a IN l` means `a` is a member of the list `l`.
--|
--| `lmem : A -> List A -> Bool`
def lmem (a l: nat): wff = $ a e. lmems l $; infixl lmem: $IN$ prec 50;

--| `all {x | p(x)} l` means every element of the list `l` satisfies `p(x)`.
def all (A: set) (l: nat): wff = $ lmems l C_ A $;

--| `List A` is the type of lists with elements of type `A`.
--| It is inductively generated by the clauses:
--| * `0 e. List A`
--| * `a e. A -> l e. List A -> a : l e. List A`
def List (A: set) (.n: nat): set = $ {n | all A n} $;

--| `len l` is the length of the list `l`.
--|
--| `len : List A -> nat`
def len (l: nat): nat;
theorem len0: $ len 0 = 0 $;
theorem lenS (a b: nat): $ len (a : b) = suc (len b) $;

--| `Array A n` is the subtype of lists which have length `n`.
--| * `0 e. Array A 0`
--| * `a e. A -> l e. Array A n -> a : l e. Array A (n+1)`
def Array (A: set) (n .l: nat): set = $ {l | l e. List A /\ len l = n} $;

--| `append l1 l2`, or `l1 ++ l2`, is the result of concatenating
--| lists `l1` and `l2`.
--| * `0 ++ l = l`
--| * `(a : l) ++ r = a : (l ++ r)`
--|
--| `append : List A -> List A -> List A`
def append (l1 l2: nat): nat; infixr append: $++$ prec 85;
theorem append0 (l: nat): $ 0 ++ l = l $;
theorem appendS (a l r: nat): $ (a : l) ++ r = a : (l ++ r) $;

--| `snoc l a` (`cons` written backwards) or `l |> a` is the
--| result of putting `a` at the end of the list `l`:
--| * `l |> a = l ++ (a : 0)`.
--|
--| `snoc : List A -> A -> List A`
def snoc (l a: nat): nat; infixl snoc: $|>$ prec 84;
theorem snoc0 (a: nat): $ 0 |> a = a : 0 $;
theorem snocS (a b c: nat): $ (a : b) |> c = a : (b |> c) $;
theorem snoclt (a b: nat): $ a < a |> b $;

--| `nth n l` is the element of list `l` at position `n`,
--| returning `0` (i.e. `none`) if the index is out of range.
--| * `nth n 0 = none`
--| * `nth 0 (a : l) = some a`
--| * `nth (n+1) (a : l) = nth n l`
--|
--| `nth : nat -> List A -> Option A`
def nth (n l: nat): nat;
theorem nth0 (n: nat): $ nth n 0 = 0 $;
theorem nthZ (a l: nat): $ nth 0 (a : l) = suc a $;
theorem nthS (n a l: nat): $ nth (suc n) (a : l) = nth n l $;

--| `repeat a n` is the list of `n` repetitions of `a`.
--|
--| `repeat : A -> nat -> List A`
def repeat (a n: nat): nat;
theorem repeat0 (a: nat): $ repeat a 0 = 0 $;
theorem repeatS (a n: nat): $ repeat a (suc n) = a : repeat a n $;

--| `map F l` is the list obtained by applying the function `F`
--| to every element of the list `l` to get another of the same length.
--| * `map F 0 = 0`
--| * `map F (a : l) = F a : map F l`
--|
--| `map : (A -> B) -> list A -> list B`
def map (F: set) (l: nat): nat;
theorem map0 (F: set): $ map F 0 = 0 $;
theorem mapS (F: set) (a l: nat):
  $ map F (a : l) = F @ a : map F l $;

--| `ljoin L` is the "join" operation of the list monad:
--| it appends all the elements of the list of lists `L`.
--| * `ljoin 0 = 0`
--| * `ljoin (l : L) = l ++ ljoin L`
--|
--| `ljoin : list (list A) -> list A`
def ljoin (L: nat): nat;
theorem ljoin0: $ ljoin 0 = 0 $;
theorem ljoinS (l L: nat): $ ljoin (l : L) = l ++ ljoin L $;

--| `sublistAt n L1 L2` means that `L2 = L1[n..n+a]`
--| where `a` is the length of `L2`.
--|
--| `sublistAt : nat -> List A -> List A -> Bool`
def sublistAt (n L1 L2 .l .r: nat): wff =
$ E. l E. r (L1 = l ++ L2 ++ r /\ len l = n) $;

--| `L1 <> L2 e. all2 R` means that `L1` and `L2` are
--| lists of the same length that are pairwise related by `R`.
--|
--| `all2 : (A -> B -> Bool) -> (list A -> list B -> Bool)`
def all2 (R: set) {.l1 .l2 .x .y .n: nat}: set =
$ S\ l1, {l2 | len l1 = len l2 /\ A. n A. x A. y
  (nth n l1 = suc x -> nth n l2 = suc y -> x <> y e. R)} $;

--| `L1 <> L2 e. ex2 R` means that `L1` and `L2` are
--| lists of the same length for which some pair is related by `R`.
--|
--| `ex2 : (A -> B -> Bool) -> (list A -> list B -> Bool)`
def ex2 (R: set) {.l1 .l2 .x .y .n: nat}: set =
$ S\ l1, {l2 | len l1 = len l2 /\ E. n E. x E. y
  (nth n l1 = suc x /\ nth n l2 = suc y /\ x <> y e. R)} $;