Version 10 (modified by diatchki, 2 years ago)

--

(NOTE: This is work in progress)

These axioms are used by GHC's solver to construct proofs/evidence for various predicates involving type-level naturals.

The actual algorithm for constructing the evidence is implemented as set of rules (interactions) which are described separately.

The "*Def" axioms bellow look a bit odd but all they are saying is that the predicates which are being defined behave like their corresponding mathematical operations.

Notation:

```k,m,n:  literals of kind Nat
r,s,t:  arbitrary terms of kind Nat
```

Comparison:

```leqDef:      m <= n    -- if "m <= n"
leqLeast:    0 <= t
leqRefl:     t <= t
leqTrans:    (r <= s, s <= t) => r <= t
leqAntiSym:  (s <= t, t <= s) => s ~ t
```

```addDef:      m + n ~ k     -- if "m + n == k"
addUnit:     0 + t ~ t
addAssoc:    (r + s) + t ~ r + (s + t)
addCommutes: t + s ~ s + t
addCancel:   (r + s ~ r + t) => s ~ t
```

Multiplication:

```mulDef:      m * n ~ k   -- if "m * n == k"
mulUnit:     1 * t ~ t
mulAssoc:    (r * s) * t ~ r * (s * t)
mulCommutes: t * s ~ s * t
mulCancel:   (r * s ~ r * t, 1 <= r) => s ~ t
```

Exponentiation:

```expDef:      m ^ n ~ k    -- if "m ^ n == k"
exp0:        a ^ 0 ~ 1
exp1:        a ^ 1 ~ a
log1:        1 ^ a ~ 1

XXX:
m ^ a ~ a => m ~ 1
a ^ m ~ a => a <= 1        -- 2 <= m
0 ^ a ~ b => b <= 1
```

Interactions:

```addMulDistr: r * (s + t) = (r * s) + (r * t)
```

References: