Bourbaki LaTTe

(ns latte-bourbaki
  (:refer-clojure :exclude [and or not set complement])
  (:require [latte.core :refer [defthm defaxiom definition example 
                                lambda try-proof proof assume have pose qed 
                                type-of type-check?]]
            [latte-prelude.quant :refer [ex exists ex-elim] :as q]
            [latte-prelude.classic :as classic]
            [latte-prelude.prop :refer [and or not absurd] :as prop]
            [latte-prelude.equal :refer [equal] :as e]
						[latte-sets.core :refer [set elem set-equal set-equal-prop
                                     forall-in] 
                             :as sets]
            [latte-sets.algebra :refer [complement]]
            [latte-sets.rel :refer [rel]]
            [latte-sets.pfun :refer [pfun]]))

(definition magma "A bourbakian Magma over the type T"
 [[T :type]]
 (==> T T T))

(clojure.repl/source example)

(example [[T :type][m (magma T)][x T][y T]]
  T
  (qed (m x y)))

(definition associative ""
  [[T :type][m (magma T)]]
  (forall [x y z T] 
   (equal (m x (m y z))
          (m (m x y) z))))

(definition monoid "A Monoid is an associative magma with an Identity"
  [[T :type][m (magma T)][e T]]
  (and (associative T m)
       (forall [x T] (and (equal x (m x e))
                          (equal x (m e x))))))

(definition group "A group is a Monoid with inverses"
  [[T :type][m (magma T)][e T][i (==> T T)]]
  (and (monoid T m e)
			 (forall [x T] (and (equal e (m (i x) x))
                          (equal e (m x (i x)))))))

(definition subgroup "A set closed under multiplication and inverses"
  [[G :type][m (magma G)][e G][i (==> G G)][H (set G)]]
  (and (group G m e i)
       (and (elem e H)
            (forall-in [x G H]
             (forall-in [y G H] (elem (m (i y) x) H))))))