Merge branch 'main' of https://github.com/teorth/equational_theories

.github/workflows/blueprint.yml

@@ -14,17 +14,29 @@ concurrency:
   group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
   cancel-in-progress: true  # Cancel any ongoing runs in the same group
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
 permissions:
-  contents: read  # Read access to repository contents
-  pages: write    # Write access to GitHub Pages
-  id-token: write # Write access to ID tokens
+  contents: read          # Read access to repository contents
+  pages: write            # Write access to GitHub Pages
+  id-token: write         # Write access to ID tokens
+  issues: write           # Write access to issues
+  pull-requests: write    # Write access to pull requests
 
 jobs:
   build_project:
     runs-on: ubuntu-latest
     name: Build project
     steps:
+      - name: Add 'awaiting-CI' label
+        if: >
+          github.event_name == 'pull_request'
+        run: |
+          curl --request POST \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
+            --header 'Content-Type: application/json' \
+            --data '["awaiting-CI"]'
+
       - name: Checkout project
         uses: actions/checkout@v4
         with:
@@ -103,25 +115,38 @@ jobs:
           find home_page/docs -name "*.hash" -delete
 
       - name: Bundle dependencies
+        if: github.event_name == 'push' && github.event.pull_request == null
         uses: ruby/setup-ruby@v1
         with:
           working-directory: home_page
           ruby-version: "3.0"  # Specify Ruby version
           bundler-cache: true  # Enable caching for bundler
 
       - name: Build website using Jekyll
-        if: env.HOME_PAGE_EXISTS == 'true'
+        if: github.event_name == 'push' && github.event.pull_request == null && env.HOME_PAGE_EXISTS == 'true'
         working-directory: home_page
         run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into home_page/_site
 
       - name: "Upload website (API documentation, blueprint and any home page)"
+        if: github.event_name == 'push' && github.event.pull_request == null
         uses: actions/upload-pages-artifact@v3
         with:
           path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
 
       - name: Deploy to GitHub Pages
+        if: github.event_name == 'push' && github.event.pull_request == null
         id: deployment
         uses: actions/deploy-pages@v4
 
       - name: Make sure the API documentation cache works
         run: mv home_page/docs .lake/build/doc
+
+      - name: Remove 'awaiting-CI' label
+        if: >
+          always() &&
+          github.event_name == 'pull_request'
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
+            --header 'Content-Type: application/json'

blueprint/src/chapter/counterexamples.tex

@@ -55,7 +55,7 @@ \chapter{Counterexamples}
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x \cdot y + 1$.
 \end{proof}
 
-\begin{theorem}[4513 does not imply 4552]\label{4513_not_imply_4552}\lean{Equation4513_not_implies_Equation4552}\leanok\uses{eq4513,eq4552} Definition \ref{eq4513} does not imply Definition \ref{eq4552}.
+\begin{theorem}[4513 does not imply 4522]\label{4513_not_imply_4522}\lean{Equation4513_not_implies_Equation4522}\leanok\uses{eq4513,eq4522} Definition \ref{eq4513} does not imply Definition \ref{eq4522}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y$ equal to $1$ if $x=0$ and $y \leq 2$, $2$ if $x=0$ and $y>2$, and $x$ otherwise.

blueprint/src/chapter/equations.tex

@@ -57,7 +57,7 @@ \chapter{Equations}
 \begin{definition}[Equation 4513]\label{eq4513}\lean{Equation4513}\leanok\uses{magma-def}  Equation 4513 is the law $x \circ (y \circ z) = (x \circ y) \circ w$.
 \end{definition}
 
-\begin{definition}[Equation 4552]\label{eq4552}\lean{Equation4552}\leanok\uses{magma-def}  Equation 4552 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
+\begin{definition}[Equation 4522]\label{eq4522}\lean{Equation4522}\leanok\uses{magma-def}  Equation 4522 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
 \end{definition}
 
 \begin{definition}[Equation 4582]\label{eq4582}\lean{Equation4582}\leanok\uses{magma-def}  Equation 4582 is the law $x \circ (y \circ z) = (w \circ u) \circ v$.

blueprint/src/chapter/implications.tex

@@ -29,14 +29,14 @@ \chapter{Implications}
 \begin{theorem}[7 equivalent to 2]\label{7_equiv_2}\uses{eq2,eq7}\lean{Equation7_implies_Equation2, Equation2_implies_Equation7}\leanok  Definition \ref{eq7} is equivalent to Definition \ref{eq2}.
 \end{theorem}
 
-\begin{proof}
+\begin{proof}\leanok
   When $x = y * z$, obviously $x = y$ because $x = x * x$ and $y = x * x$. the other way around is trivial.
 \end{proof}
 
 \begin{theorem}[6 equivalent to 2]\label{6_equiv_2}\uses{eq2,eq6}\lean{Equation6_implies_Equation2, Equation2_implies_Equation6}\leanok  Definition \ref{eq6} is equivalent to Definition \ref{eq2}.
 \end{theorem}
 
-\begin{proof}  Similar to the previous argument.
+\begin{proof}\leanok  Similar to the previous argument.
 \end{proof}
 
 More generally, any equation of the form $x = f(y,z,w,u,v)$ is equivalent to Equation 2 (eventually once we have enough API for Magma relations, we could formalize this general claim rather than establish it on a case by case basis).  It is also trivial that Equation 2 implies every other equation.

equational-theories.code-workspace

@@ -0,0 +1,21 @@
+{
+	"folders": [
+		{
+			"path": "."
+		},
+	],
+	"settings": {
+		"files.insertFinalNewline": true,
+		"files.trimTrailingWhitespace": true,
+		"[lean4]": {
+			"editor.rulers": [
+				100
+			]
+		}
+	},
+	"extensions": {
+		"recommendations": [
+			"leanprover.lean4"
+		]
+	}
+}

equational_theories/Basic.lean

@@ -28,22 +28,30 @@ def Equation4 (G: Type*) [Magma G] := ∀ x y : G, x = x ∘ y
 /-- The right absorption law -/
 def Equation5 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ x
 
+@[inherit_doc Equation2]
 def Equation6 (G: Type*) [Magma G] := ∀ x y : G, x = y ∘ y
 
+@[inherit_doc Equation2]
 def Equation7 (G: Type*) [Magma G] := ∀ x y z : G, x = y ∘ z
 
 def Equation8 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ x)
 
+/-- value of multiplication is independent of right argument -/
 def Equation38 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = x ∘ y
 
+/-- value of multiplication is independent of left argument; dual of 38 -/
 def Equation39 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ x
 
+/-- all squares are the same -/
 def Equation40 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = y ∘ y
 
+/-- all products are the same -/
 def Equation41 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ x = y ∘ z
 
+@[inherit_doc Equation38]
 def Equation42 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ y = x ∘ z
 
+/-- The commutative law -/
 def Equation43 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x
 
 /-- The constant law -/
@@ -59,8 +67,9 @@ def Equation4512 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ (y ∘ z) = (x ∘
 
 def Equation4513 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ (y ∘ z) = (x ∘ y) ∘ w
 
-def Equation4552 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
+def Equation4522 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
 
+/-- all products of three values are the same, regardless bracketing -/
 def Equation4582 (G: Type*) [Magma G] := ∀ x y z w u v: G, x ∘ (y ∘ z) = (w ∘ u) ∘ v
 
 
@@ -73,19 +82,21 @@ theorem Equation2_implies_Equation4 (G: Type*) [Magma G] (h: Equation2 G) : Equa
   fun _ _ => h _ _
 
 theorem Equation2_implies_Equation6 (G: Type*) [Magma G] (h: Equation2 G) : Equation6 G :=
-  sorry
+  fun _ _ => h _ _
 
 theorem Equation2_implies_Equation7 (G: Type*) [Magma G] (h: Equation2 G) : Equation7 G :=
-  sorry
+  fun _ _ _ => h _ _
 
 theorem Equation2_implies_Equation46 (G: Type*) [Magma G] (h: Equation2 G) : Equation46 G :=
   fun _ _ _ _ => h _ _
 
-theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G :=
-  sorry
+theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G := by
+  intro a b
+  rw [h a a, ← h b]
 
-theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G :=
-  sorry
+theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G := by
+  intro a b
+  rw [h a a a, ←h b]
 
 theorem Equation4_implies_Equation3 (G: Type*) [Magma G] (h: Equation4 G) : Equation3 G := by
   intro _
@@ -95,7 +106,7 @@ theorem Equation4_implies_Equation42 (G: Type*) [Magma G] (h: Equation4 G) : Equ
   intro _ _ _
   rw [<-h, <-h]
 
-theorem Equation4_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4 G) : Equation4552 G := by
+theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : Equation4522 G := by
   intro x y z w u
   rw [<-h, <-h, <-h]
 
@@ -122,10 +133,10 @@ theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) :
 theorem Equation4513_implies_Equation4512 (G: Type*) [Magma G] (h: Equation4513 G) : Equation4512 G :=
   fun _ _ _ => h _ _ _ _
 
-theorem Equation4552_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4552 G) : Equation4513 G :=
+theorem Equation4522_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4522 G) : Equation4513 G :=
   fun _ _ _ _ => h _ _ _ _ _
 
-theorem Equation4582_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4552 G :=
+theorem Equation4582_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4522 G :=
   fun _ _ _ _ _ => h _ _ _ _ _ _
 
 
@@ -337,7 +348,7 @@ theorem Equation4512_not_implies_Equation4513 : ∃ (G: Type) (_: Magma G), Equa
   dsimp [hG] at h
   linarith
 
-theorem Equation4513_not_implies_Equation4552 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4552 G := by
+theorem Equation4513_not_implies_Equation4522 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4522 G := by
   let hG : Magma Nat := {
     op := fun x y => if x = 0 then (if y ≤ 2 then 1 else 2) else x
   }