Version 6 (modified by diatchki, 4 years ago) (diff) |
---|

(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

Addition:

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 -- {m ^ n == k} exp0: a ^ 0 ~ 1 exp1: a ^ 1 ~ a log1: 1 ^ a ~ 1 (m ^ a ~ a) <=> False -- m /= 1 (a ^ m ~ a) <=> (a <= 1) -- 2 <= m

Interactions:

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

References: