null

b-mehta · Oct 1, 2024 · 79f842a · 79f842a
1 parent 5021c3d
commit 79f842a
Show file tree

Hide file tree

Showing 30 changed files with 30,922 additions and 322 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -1,27 +1,57 @@
-# Contributing to Equational Theories
-
-Anyone can contribute to the equational theories project! Specific guidelines for contributions are as follows.
-
-## The Contributions Process
-The project is coordinated using a [Github project dashboard](https://github.com/users/teorth/projects/1).
-Contributions to the project take the form of Github pull requests that complete tasks. The detailed instructions are as follows:
-
-1. Each task is posted as an issue that appears in the `Unclaimed Outstanding Task` column of the [dashboard](https://github.com/users/teorth/projects/1)
-2. A contributor can lay claim to a task by commenting `claim` in the corresponding github issue. A user who wishes to drop their claim can comment `disclaim` on the issue.
-3. If there is no other user assigned to the task, the user gets assigned to the issue. A `claim`ed issue moves to the `Claimed Tasks` column of the dashboard.
-   * If you wish to give up on a task, please comment `disclaim` on it. This allows others to `claim` it. Only one github user can claim a task at a time.
-5. The user creates a PR to solve the task and then comments `propose PR #xyz` under the issue. If the issue is already assigned to them, their PR is now linked to the issue. The PR now moves to the `In Progress` column of the dashboard and is shown with the linked PR.
-   * _A PR proposal is only accepted if an issue has been claimed by the github user._
-7. To withdraw their PR, a user can comment `withdraw PR #xyz`. The task moves to the `Claimed Tasks` column and the user remains assigned to the Github issue.
-     * **Important**: _If a user wishes to propose a different PR, the user needs to first withdraw their previous PR (step 6) in one comment. In a subsequent comment, they may propose the new PR (as in step 4)._
-8. Upon finishing the PR, the user may comment `awaiting-review` on the PR which is shown in the task view of the dashboard against the PR.
-Maintainers review and merge it.
-9. Merged tasks move to the `Completed Tasks` column of the dashboard.
-
-### Some Rules and Notes
-1. Please respect the issue claims. If an issue has been assigned to someone, please don't try to work on it simultaneously without discussing with the claimant first. This allows for a coordination process that respects every contributor's time and effort.
-2. Please note that this process is still experimental. As such there are bound to be issues and bugs. We will improve this as we go along. Feedback is welcome on the [Lean Zulip chat channel](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/)
-3.  Until the process above is automated with enough CI actions, maintainers of the project dashboard are manually handling things. So please be patient with us.
+# Contributing to the Equational Theories Project
+
+Thank you for your interest in contributing to the Equational Theories Project! This guide provides detailed instructions on how to effectively and efficiently contribute to the project.
+
+## Project Coordination
+
+The project is managed using a [GitHub project dashboard](https://github.com/users/teorth/projects/1), which tracks tasks through various stages, from assignment to completion.
+
+## How to Contribute
+
+Contributions to the project are made through GitHub pull requests (PRs) that correspond to specific tasks outlined in the project's issues.
+The following instructions detail the process for claiming and completing tasks.
+
+### 1. Task Identification
+
+- Tasks are posted as GitHub issues and can be found in the `Unclaimed Outstanding Tasks` column of the project dashboard.
+- Each issue represents a specific task to be completed. The issue title and description contain relevant details and requirements.
+
+### 2. Claiming a Task
+
+- To claim a task, comment `claim` on the relevant GitHub issue.
+- If no other user is assigned, you will automatically be assigned to the task, and the issue will move to the `Claimed Tasks` column.
+- You may only claim one task at a time. If you decide not to work on a task after claiming it, comment `disclaim` on the issue. This will unassign you and return the issue to the `Unclaimed Outstanding Tasks` column, making it available for others to claim.
+
+### 3. Working on the Task
+
+Once you are assigned to an issue, begin working on the corresponding task. You should create a new branch from the `main` branch to develop your solution.
+
+### 4. Submitting a Pull Request
+
+- When you are ready to submit your solution, create a PR from your working branch to the project’s `main` branch.
+- After submitting the PR, comment `propose PR #PR_NUMBER` on the original issue. This links your PR to the task, and the task will move to the `In Progress` column on the dashboard.
+- A task can only move to `In Progress` if it has been claimed by the user proposing the PR.
+
+### 5. Withdrawing or Updating a PR
+
+- If you need to withdraw your PR, comment `withdraw PR #PR_NUMBER` on the issue. The task will return to the `Claimed Tasks` column, but you will remain assigned to the issue.
+- To submit an updated PR after withdrawal, comment `propose PR #NEW_PR_NUMBER` following the same process outlined in step 4.
+
+### 6. Review Process
+
+- After finishing the task and ensuring your PR is ready for review, comment `awaiting-review` on the PR. This will add the `awaiting-review` label to your PR and move the task from `In Progress` to the `PRs in Review` column of the dashboard.
+- The project maintainers will review the PR. They may request changes, approve the PR, or provide feedback.
+
+### 7. Task Completion
+
+- Once the PR is approved and merged, the task will automatically move to the `Completed` column.
+- If further adjustments are needed after merging, a new issue will be created to track additional work.
+
+### Additional Guidelines and Notes
+
+1. Please adhere to the issue claiming process. If an issue is already assigned to another contributor, refrain from working on it without prior communication with the current claimant. This ensures a collaborative and respectful workflow that values each contributor’s efforts.
+2. Be aware that this contribution process is still in an experimental phase. As a result, occasional issues and inefficiencies may arise. We are committed to continuously refining the process, and your constructive feedback is highly appreciated. You can share your thoughts and suggestions on the [Lean Zulip chat channel](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/).
+3. Until the integration of sufficient CI automation, the management of the project dashboard is handled manually by the maintainers. We ask for your patience and understanding as we work to keep the process running smoothly.
 
 ## Discussion
 

diff --git a/README.md b/README.md
@@ -16,6 +16,7 @@ Some automatically generated progress:
 - Sep 28, 2024: [18972 implications](equational_theories/Generated/SimpleRewrites/theorems) were established by simple rewrite laws.
 - Sep 28, 2024: [4.2m implications proven by a transitive reduction of 15k theorems](equational_theories/Generated/TrivialBruteforce) were proven using simple rewrite proof scripts.
 - Sep 29, 2024: [13.7m implications were conjectured to be refused by a collection of 515 magmas](equational_theories/Generated/All4x4Tables), collected by enumerating all 4^(4*4) operators and reducing to a covering set.
+- Oct 1, 2024: Another [~250k transitive implications](equational_theories/Generated/TrivialBruteforce) were proven by simple proof generation.
 
 Some statistics and data files from a given point in time:
 - Sep 28, 2024: [A repository of unknown implications](https://github.com/amirlb/equational_theories/tree/unknown-implications), including all unknown implications, known equivalence classes, unknown implications modulo known equivalence, and only the strongest unknown implications.
@@ -63,6 +64,7 @@ To build this project after [installing Lean](https://www.lean-lang.org/lean-get
         - [`find_dual`](scripts/find_dual.py) - finds the dual of an equation
         - [`find_equation_id`](scripts/find_equation_id.py) - finds the equation number of an equation string
         - [`generate_eqs_list`](scripts/generate_eqs_list.py) - generates a list of equations
+        - [`generate_graphviz_graph`](scripts/generate_graphviz_graph.rb) - generates a graphviz dot file, that can be used to create an implication graph
         - [`generate_image`](scripts/generate_image.py) - generates an image of implications
         - [`generate_most_wanted_list`](scripts/generate_most_wanted_list.py) - generates the "most wanted" implications
         - [`generate_z3_counterexample`](scripts/generate_z3_counterexample.py) - given an implication statement between two equations, calls Z3 to try to generate a counterexample

diff --git a/blueprint/src/chapter/general_implications.tex b/blueprint/src/chapter/general_implications.tex
@@ -7,10 +7,10 @@ \chapter{General implications}
 Two laws are said to be \emph{equivalent} if they imply each other.
 \end{definition}
 
-\begin{lemma}[Pre-order]\label{pre-order}\uses{impl}  Implication is a pre-order on the set of laws, and equivalence is an equivalence relation.
+\begin{lemma}[Pre-order]\leanok\label{pre-order}\uses{impl}  Implication is a pre-order on the set of laws, and equivalence is an equivalence relation.
 \end{lemma}
 
-\begin{proof} Trivial.
+\begin{proof}\leanok Trivial.
 \end{proof}
 
 Implications between the laws from Chapter \ref{subgraph-eq} are depicted in Figure \ref{fig:implications}.

diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex
@@ -50,7 +50,7 @@ \chapter{Basic theory of magmas}
 and so forth.
 
 \begin{definition}[Law]\label{law-def}
-  \lean{MagmaLaw}\leanok
+  \lean{Law.MagmaLaw}\leanok
   \uses{induced-def}
   Let $X$ be a set. A \emph{law} with alphabet $X$ is a formal expression of the form $w \formaleq w'$,
   where $w, w' \in M_X$ are words with alphabet $X$ (thus one can identify laws with alphabet $X$
@@ -67,7 +67,7 @@ \chapter{Basic theory of magmas}
 \begin{equation}\label{comm-law-2}
  x \circ y = y \circ x
 \end{equation}
-for all $x, y \in G$.  We refer to \eqref{comm-law-2} as the \emph{equation} associated to the law \eqref{comm-law}.  One can think of equations as the ``semantic'' intrepretation of a ``syntactic'' law.  However, we shall often abuse notation and a law with its associated equation thus we shall (somewhat carelessly) also refer to \eqref{comm-law-2} as ``the commutative law'' (rather than ``the commutative equation'').
+for all $x, y \in G$.  We refer to \eqref{comm-law-2} as the \emph{equation} associated to the law \eqref{comm-law}.  One can think of equations as the ``semantic'' interpretation of a ``syntactic'' law.  However, we shall often abuse notation and a law with its associated equation thus we shall (somewhat carelessly) also refer to \eqref{comm-law-2} as ``the commutative law'' (rather than ``the commutative equation'').
 
 \begin{definition}[Models]\label{models-def}
   \lean{models}\leanok
@@ -87,7 +87,7 @@ \chapter{Basic theory of magmas}
     \item $\Gamma\vdash w\formaleq w$ for any word $w$
     \item if $\Gamma\vdash w\formaleq w'$ then $\Gamma\vdash w'\formaleq w$
     \item if $\Gamma\vdash w\formaleq w'$ and $\Gamma\vdash w'\formaleq w''$ then $\Gamma\vdash w\formaleq w''$
-    \item if $\Gamma\vdash w\formaleq w'$ then $\Gamma\vdash w\sigma\formaleq w'\sigma$, where $\sigma$ is an arbitrary map from $X$ to words in $M_X$ and $w\sigma$ replaces each occurence of an element of $X$ with it's image by $\sigma$ in $w$.
+    \item if $\Gamma\vdash w\formaleq w'$ then $\Gamma\vdash w\sigma\formaleq w'\sigma$, where $\sigma$ is an arbitrary map from $X$ to words in $M_X$ and $w\sigma$ replaces each occurrence of an element of $X$ with it's image by $\sigma$ in $w$.
     \item if $\Gamma\vdash w_1\formaleq w_2$ and $\Gamma\vdash w_3\formaleq w_4$ then $\Gamma\vdash w_1 \circ w_3\formaleq w2\circ w_4$
   \end{enumerate}
 \end{definition}

diff --git a/blueprint/src/chapter/trivial_auto.tex b/blueprint/src/chapter/trivial_auto.tex
@@ -1,5 +1,51 @@
 \chapter{Trivial auto-generated theorems}
 
-\href{https://github.com/teorth/equational_theories/tree/main/equational_theories/Generated/TrivialBruteforce/theorems}{4.2m implications proven by a transitive reduction of 15k theorems} were proven using simple rewrite proof scripts.
+\href{https://github.com/teorth/equational_theories/tree/main/equational_theories/Generated/TrivialBruteforce}{Approximately 4.5m transitive implications were proven by a transitive reduction of about 15k theorems}. Most of these implications were derived from being the first automated run to connect the largest equivalence classes, hence creating a large set of transitively closed implications.
 
-{\bf include more details of the methodology, and any comparisons with other generated implication data sets.}
+Scripts generated theorems to try simple combinations of equation rewrites to reach the desired goal for every unknown implication. The generated proof scripts were run with lean and the successful theorems were extracted. An example of the types of generated rewrites that were tested:
+
+\begin{verbatim}
+  repeat intro
+  apply
+\end{verbatim}
+
+\begin{verbatim}
+  repeat intro
+  try { rw [<-h] }
+  try { rw [<-h, <-h] }
+  try { rw [<-h, <-h, <-h] }
+  try { rw [<-h, <-h, <-h, <-h] }
+  try { rw [<-h, <-h, <-h, <-h, <-h] }
+  repeat rw [h]
+\end{verbatim}
+
+\begin{verbatim}
+  repeat intro
+  try {
+    nth_rewrite 1 [h]
+    try { rw [h] }
+    try { rw [<-h] }
+  }
+  try {
+    nth_rewrite 2 [h]
+    try { rw [h] }
+    try { rw [<-h] }
+  }
+  try {
+    nth_rewrite 3 [h]
+    try { rw [h] }
+    try { rw [<-h] }
+  }
+  try {
+    nth_rewrite 4 [h]
+    try { rw [h] }
+    try { rw [<-h] }
+  }
+  try {
+    nth_rewrite 1 [h]
+    nth_rewrite 1 [h]
+    try { rw [h] }
+    try { rw [<-h] }
+  }
+  ...
+\end{verbatim}
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -1,6 +1,7 @@
 import equational_theories.Completeness
 import equational_theories.Compactness
 import equational_theories.FreeMagma
+import equational_theories.MagmaOp
 import equational_theories.Subgraph
 import equational_theories.AllEquations
 import equational_theories.InfModel

diff --git a/equational_theories/Closure.lean b/equational_theories/Closure.lean
@@ -306,18 +306,44 @@ def list_outcomes {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] :
   for edge in toEdges prs do
     outcomes := outcomes.modify eqs[edge.lhs]! (fun a ↦ a.set! eqs[edge.rhs]!
       (.explicit_theorem edge.isTrue))
-  for edge in toEdges rs do
-    outcomes := outcomes.modify eqs[edge.lhs]! (fun a ↦ a.modify eqs[edge.rhs]!
-      fun y ↦ if y = .unknown then .explicit_conjecture edge.isTrue else y)
 
   for ⟨x, y, is_true⟩ in closure_aux prs eqs do
     outcomes := outcomes.modify x (fun a ↦ a.modify y
                 fun y ↦ if y = .unknown then .implicit_theorem is_true else y)
 
+  for edge in toEdges rs do
+    outcomes := outcomes.modify eqs[edge.lhs]! (fun a ↦ a.modify eqs[edge.rhs]!
+      fun y ↦ if y = .unknown then .explicit_conjecture edge.isTrue else y)
+
   for ⟨x, y, is_true⟩ in closure_aux rs eqs do
     outcomes := outcomes.modify x (fun a ↦ a.modify y
                 fun y ↦ if y = .unknown then .implicit_conjecture is_true else y)
 
   return (eqs_order, outcomes)
 
+def outcomes_mod_equiv (inp : Array EntryVariant) : Array String × Array (Array (Option Bool)) := Id.run do
+  let (eqs, eqs_order) := number_equations inp
+  let n := eqs.size
+  let reachable := closure_aux inp eqs
+  let mut reprs_id : Std.HashMap Nat Nat := {}
+  let mut reprs : Array String := Array.mkEmpty (reachable.components.size / 2)
+  for comp in reachable.components do
+    if comp[0]! < n then
+      reprs_id := reprs_id.insert comp[0]! reprs.size
+      reprs := reprs.push eqs_order[comp[0]!]!
+
+  let mut implies : Array (Array (Option Bool)) :=
+    Array.mkArray reprs.size (Array.mkArray reprs.size none)
+
+  for i in reachable.components, i2 in reachable.reachable do
+    if i[0]! >= reachable.size then continue
+      for j in reachable.components, j2 in [:reachable.components.size] do
+        if i2.get j2 then
+          if j[0]! < n then
+            implies := implies.modify reprs_id[j[0]!]! (fun x ↦ x.set! reprs_id[i[0]!]! true)
+          else if j.back < 2*n then
+            implies := implies.modify reprs_id[i[0]!]! (fun x ↦ x.set! reprs_id[j[0]! - n]! false)
+
+  return (reprs, implies)
+
 end Closure
diff --git a/equational_theories/Compactness.lean b/equational_theories/Compactness.lean
@@ -1,6 +1,9 @@
-import equational_theories.Completeness
 import Mathlib.Data.Finset.Basic
+import equational_theories.Completeness
+
+open Law
 
+set_option linter.unusedVariables false
 def derive.getAxioms {α} [DecidableEq α] {Γ : Ctx α} {E : MagmaLaw α} (h : Γ ⊢ E) :
     Finset (MagmaLaw α) :=
   match h with

diff --git a/equational_theories/Completeness.lean b/equational_theories/Completeness.lean
@@ -4,12 +4,20 @@
 import equational_theories.FreeMagma
 import Mathlib.Data.Set.Defs
 
+open FreeMagma
+
+namespace Law
+
 structure MagmaLaw (α : Type) where
   lhs : FreeMagma α
   rhs : FreeMagma α
 deriving DecidableEq
 
-local infix:60 " ≃ " => MagmaLaw.mk
+infix:60 " ≃ " => MagmaLaw.mk
+
+end Law
+
+open Law
 
 def substFreeMagma {α β} (t : FreeMagma α) (σ : α → FreeMagma β) : FreeMagma β :=
 match t with
@@ -24,6 +32,8 @@ def Ctx α := Set (MagmaLaw α)
 -- FIXME: figure out how to remove this.
 instance Ctx.Membership α : Membership (MagmaLaw α) (Ctx α) := ⟨ Set.instMembership.mem ⟩
 
+instance {α : Type} : Singleton (MagmaLaw α) (Ctx α) := ⟨Set.singleton⟩
+
 section DeriveDef
 
 set_option hygiene false
@@ -44,7 +54,7 @@ inductive derive {α} : Ctx α → MagmaLaw α → Type :=
 end DeriveDef
 
 def satisfiesPhi {α G : Type} [Magma G] (φ : α → G) (E : MagmaLaw α) : Prop :=
-  evalInMagma φ E.lhs = evalInMagma φ E.rhs
+  E.lhs.evalInMagma φ = E.rhs.evalInMagma φ
 
 def satisfies {α : Type} (G : Type) [Magma G] (E : MagmaLaw α) := ∀ (φ : α → G), satisfiesPhi φ E
 

diff --git a/equational_theories/FreeComm.lean b/equational_theories/FreeComm.lean
diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -19,7 +19,9 @@ theorem FreeMagma_op_eq_fork (α : Type u) (a b : FreeMagma α) : a ∘ b = a
 
 notation "Lf" => FreeMagma.Leaf
 
-instance FreeMagma.Magma {α} : Magma (FreeMagma α) := ⟨ Fork ⟩
+instance FreeMagma.isMagma {α} : Magma (FreeMagma α) := ⟨ Fork ⟩
+
+namespace FreeMagma
 
 def fmapFreeMagma {α : Type u} {β : Type v} (f : α → β) : FreeMagma α → FreeMagma β
   | Lf a => FreeMagma.Leaf (f a)
@@ -29,22 +31,24 @@ def evalInMagma {α : Type u} {G : Type v} [Magma G] (f : α -> G) : FreeMagma
   | Lf a => f a
   | lchild ⋆ rchild => (evalInMagma f lchild) ∘ (evalInMagma f rchild)
 
-theorem ExpressionEqualsAnything_implies_Equation2 (G: Type u) [Magma G]
-  : (∃ n : Nat, ∃ expr : FreeMagma (Fin n), ∀ x : G, ∀ sub : Fin n → G, x = evalInMagma sub expr) → Equation2 G := by
+end FreeMagma
+
+theorem ExpressionEqualsAnything_implies_Equation2 (G: Type u) [Magma G] :
+    (∃ n : Nat, ∃ expr : FreeMagma (Fin n), ∀ x : G, ∀ sub : Fin n → G, x = expr.evalInMagma sub) → Equation2 G := by
   intro ⟨n, expr, univ⟩ x y
   let constx : Fin n → G := fun _ ↦ x
   exact (univ x constx).trans (univ y constx).symm
 
-theorem Equation37_implies_Equation2 (G : Type u) [Magma G]
-  : (∀ x y z w : G, x = (y ∘ z) ∘ w) → Equation2 G :=
+theorem Equation37_implies_Equation2 (G : Type u) [Magma G] :
+    (∀ x y z w : G, x = (y ∘ z) ∘ w) → Equation2 G :=
   fun univ ↦ ExpressionEqualsAnything_implies_Equation2 G ⟨
     3,
     (Lf 0 ⋆ Lf 1) ⋆ Lf 2, -- The syntactic representation of (y ∘ z) ∘ w
     fun k sub ↦ univ k (sub 0) (sub 1) (sub 2)
   ⟩
 
-theorem Equation514_implies_Equation2 (G : Type u) [Magma G]
-  : (∀ x y : G, x = y ∘ (y ∘ (y ∘ y))) → Equation2 G :=
+theorem Equation514_implies_Equation2 (G : Type u) [Magma G] :
+    (∀ x y : G, x = y ∘ (y ∘ (y ∘ y))) → Equation2 G :=
   fun univ ↦ ExpressionEqualsAnything_implies_Equation2 G ⟨
     1,
     Lf 0 ⋆ (Lf 0 ⋆ (Lf 0 ⋆ Lf 0)), -- The syntactic representation of y ∘ (y ∘ (y ∘ y)))