Version 6 (modified by diatchki, 7 years ago) (diff)

--

Notation:

```m,n,k:  natural numbers
a,b,c:  types of kind Nat
```

When overlapping, earlier rules take precedence (as in Haskell).

Top-level interactions for `TypeNat`:

```TypeNat m
```

Top-level interactions for <=

```m <= n   <=> {m <= n}
0 <= a   <=> True
a <= 0   <=> a ~ 0
```

Top-level interactions for +.

```(m + n ~ k) <=> {m + n == k}
(m + a ~ n) <=> a ~ {n - m}    -- n >= m
(a + m ~ n) <=> a ~ {n - m}    -- n >= m
(0 + a ~ b) <=> a ~ b
(a + 0 ~ b) <=> a ~ b
(a + b ~ 0) <=> (a ~ 0, b ~ 0)
(a + b ~ a) <=> (b ~ 0)
(a + b ~ b) <=> (a ~ 0)
(a + a ~ b) <=> (2 * a ~ b)
(a + m ~ b) <=> (m + a ~ b)    -- simple normalization cuts down on some rules
```

Top-level interactions for *.

```(m * n ~ k) <=> {m * n == k}
(m * a ~ n) <=> a ~ {n / m}     -- m `divides` n
(a * m ~ n) <=> a ~ {n / m}     -- m `divides` n
(0 * a ~ b) <=> b ~ 0
(a * 0 ~ b) <=> b ~ 0
(1 * a ~ b) <=> a ~ b
(a * 1 ~ b) <=> a ~ b
(a * b ~ 1) <=> (a ~ 1, b ~ 1)
(a + a ~ b) <=> a ^ 2 ~ b
```

Top-level interactions for `^`

```(m ^ n ~ k) <=> {m ^ n} == k
(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists
(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists
(a ^ 0 ~ b) <=> b ~ 1
(1 ^ a ~ b) <=> b ~ 1
```