update readme

README.md

@@ -35,12 +35,16 @@ Using widespread and commonly supported languages gives a huge leg up in terms o
 
 It is not desirable or within my capabilities to build a giant universe in which to live. The goal is to take a subtle blade and bolt together things that already exist.
 
-The de Bruijn criterion is going to be bent or broken in certain senses. The kernel will be small. It is still of matter of design whether to have checkable proof objects or a controlled checking process.
+The de Bruijn criterion is going to be bent or broken in certain senses. Attention is paid to what is kernel and what is not. Proof objects are basically trees recording chains of lemmas from Automated Theorem Prover (ATP) calls.
 
 Soundness will be attempted, accidental misuse will be made difficult but not impossible.
 
-Core functionality comes from Z3 and other ATPs. To some degree, this is a metalayer to guide automated provers down proofs they could perhaps do on their own, but of course would get lost. The core logic is more or less multi-sorted first order logic.
+Core functionality comes from [Z3](https://github.com/Z3Prover/z3) and other ATPs. To some degree, knuckledragger is a metalayer to guide automated provers down proofs they could perhaps do on their own, but of course would get lost.
 
-A big feature that ATP do not often support is induction, definitions, and other axiom schema. These are supported.
+Other theorem provers of interest: [cvc5](https://cvc5.github.io/), [Vampire](https://vprover.github.io/), [eprover](https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html), [Twee](https://nick8325.github.io/twee/), [egglog](https://egglog-python.readthedocs.io/latest/), [nanoCoP](https://leancop.de/nanocop/).
 
-A hope is to be able to use easy access to Jupyter, copilot, ML ecosystems, sympy, cvxpy, numpy, scipy, calcium, flint, sage, singular will make metaprogramming this system very powerful. I maintain the option to just trust these results but hopefully they can be translated into arguments the kernel can understand.
+The core logic is more or less multi-sorted first order logic.
+
+Big features that ATPs do not often support is induction, definitions, and other axiom schema. These are supported.
+
+A hope is to be able to use easy access to [Jupyter](https://jupyter.org/), [copilot](https://copilot.microsoft.com/), ML ecosystems, [sympy](https://www.sympy.org/), [cvxpy](https://www.cvxpy.org/), [numpy](https://numpy.org/), scipy, [Julia](https://github.com/JuliaPy/PythonCall.jl), [Prolog](https://www.swi-prolog.org/pldoc/man?section=janus-call-prolog), [calcium](https://fredrikj.net/calcium/), [flint](https://fredrikj.net/python-flint/), and [sage](https://www.sagemath.org/) will make metaprogramming this system very powerful. I maintain the option to just trust these results but hopefully they can be translated into arguments the kernel can understand.

knuckledragger/theories/Real.py

@@ -1,8 +1,12 @@
 import z3
 from z3 import ForAll, Function
 from knuckledragger import lemma, axiom
+import knuckledragger as kd
 
 R = z3.RealSort()
+RFun = z3.ArraySort(R, R)
+RSeq = z3.ArraySort(z3.IntSort(), R)
+
 x, y, z = z3.Reals("x y z")
 
 plus = Function("plus", R, R, R)
@@ -28,8 +32,21 @@
     by=[mul_def, plus_def],
 )
 
-abs = Function("abs", R, R)
-abs_def = axiom(ForAll([x], abs(x) == z3.If(x >= 0, x, -x)), "definition")
 
-RFun = z3.ArraySort(R, R)
-RSeq = z3.ArraySort(z3.IntSort(), R)
+abs = kd.define("abs", [x], z3.If(x >= 0, x, -x))
+
+abs_idem = kd.lemma(ForAll([x], abs(abs(x)) == abs(x)), by=[abs.defn])
+abd_neg = kd.lemma(ForAll([x], abs(-x) == abs(x)), by=[abs.defn])
+abs_ge_0 = kd.lemma(ForAll([x], abs(x) >= 0), by=[abs.defn])
+
+nonneg = kd.define("nonneg", [x], abs(x) == x)
+nonneg_ge_0 = kd.lemma(ForAll([x], nonneg(x) == (x >= 0)), by=[nonneg.defn, abs.defn])
+
+max = kd.define("max", [x, y], z3.If(x >= y, x, y))
+max_comm = kd.lemma(ForAll([x, y], max(x, y) == max(y, x)), by=[max.defn])
+max_assoc = kd.lemma(
+    ForAll([x, y, z], max(x, max(y, z)) == max(max(x, y), z)), by=[max.defn]
+)
+max_idem = kd.lemma(ForAll([x], max(x, x) == x), by=[max.defn])
+max_ge = kd.lemma(ForAll([x, y], max(x, y) >= x), by=[max.defn])
+max_ge_2 = kd.lemma(ForAll([x, y], max(x, y) >= y), by=[max.defn])