better than apmxi

## Primary tabs

# better than apmxi

I'm working on hammering out a better notation for talking about

math with the computer.

Critera:

* I want something better than the notation used by apmxi.

* This time I'd actually like both people and computers to understand what I'm saying.

* I want something "LISP-based" (because I like writing LISP code).

At this point, I'm still just sketching things out.

Here is an example. This is a version of the first proof in djao's

entry about cosets.

http://planetmath.org/encyclopedia/Coset.html

The style for definitions is based on APM-xi (roughly put, everything

in the definition is inside an "and").

Unfortunately, I don't have a very good sense of how to deal with

"mathematical foundations", so we begin with a couple of what seem to

be *particularly* weakly put together definitions.

Comments are welcome. I'd like to know what you think about the

readability of this code,

Joe

<pre>

(defn set (X)

(eq (type X)

set))

(defn elt (x X)

(member x X))

(defn subset (Y X)

(set Y)

(set X)

(forall y :in Y :st (elt y X)))

(defn operation (* X)

(set X)

(forall a b :in X :st (elt (* a b) X)))

(defn associative (* X)

(operation * X)

(forall a b c :in X :st (eq (* a b c)

(* (* a b)

c)

(* a

(* b c)))))

(defn group (G *)

(set G)

(operation * G)

(associative *)

(exists e :in G :st (forall a :in G :st (eq (* e a)

(* a e)

a)))

(forall a :in G :st (exists a' :in G :st (eq (* a a')

(* a' a)

e))))

(defn subgroup (H G)

(group H)

(subset H G))

(defn coset (a H G S)

(group G)

(subgroup H G)

(elt a G)

(eq S (setof (* a h) :st h :in H)))

(defproof two-left-cosets-identical-or-disjoint ()

(coset a H G aH)

(coset b H G bH)

(if (elt c (intersection aH bH))

;; this is the body of the proof

(and

;; rewriting what it means for `c' to be in the intersection of

;; the two cosets

(exists h1 h2 :in H :st (eq c

(* a h1)

(* b h2)))

;; use the last equality to show another equivalent equality

;; first step

(eq (* (inv b) a h1)

h2)

;; second step

(eq (* (inv b) a)

(* h2 (inv h1)))

;; conclude from the last step (and closure of H) -- [0]

(elt (* (inv b) a) H)

;; we now make a big statement about elements of H

(forall h :in H :st (and

;; [1]

(eq (* a

h)

;; introduce `e' in a nice way

(* (* b

(inv b))

a

h)

;; regroup terms

(* b

(* (inv b)

a)

h))

;; from [0] and the definition of bH

;; [2]

(elt (* b

(* (inv b)

a)

h)

bH)

;; just rewrite [2] using [1]

(elt (* a

h)

bH)))

;; shorthand for a variation on the last chain of reasoning

(symmetrically b a

bH aH)

;; summarize the last step

(subset aH bH)

;; using the previous symmetrical argument

(symmetrically bH aH)

(eq aH bH))

;; if there is no element `c' in the intersection

;; the intersection is empty

(eq (intersection S1 S2) nil)))

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections

## Re: better than apmxi

In case you want to easily download and play this code, I'm posting it on

my webpage too.

http://www.ma.utexas.edu/~jcorneli/j/cosets.lisp