Revert "Merge branch 'main' into equations-command-modification"

This reverts commit a3cf909, reversing changes made to fd25f3f.
0art0 · Oct 8, 2024 · f0eabb9 · f0eabb9
1 parent a3cf909
commit f0eabb9
Show file tree

Hide file tree

Showing 76 changed files with 198 additions and 486 deletions.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -139,7 +139,6 @@ jobs:
       - name: Generate home_page/implications/implications.js
         run: |
           ~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json
-          pip install markdown
           python scripts/generate_equation_implication_js.py /tmp/out.json
 
       - name: Bundle dependencies

diff --git a/.vscode/extensions.json b/.vscode/extensions.json
@@ -1,7 +1,12 @@
 {
+    // Learn about workspace recommendations at:
+    // https://go.microsoft.com/fwlink/?LinkId=827846
+
+    // The extension identifier format is ${publisher}.${name}
+    // Example: vscode.csharp
+
     // List of extensions that should be recommended for users of this workspace
     "recommendations": [
-        "leanprover.lean4",        // Extension for Lean 4 support
-        "James-Yu.latex-workshop"  // LaTeX Workshop extension for LaTeX support
+        "leanprover.lean4"  // Extension for Lean 4 support
     ]
 }
diff --git a/blueprint/.vscode/settings.json b/blueprint/.vscode/settings.json
diff --git a/commentary/Equation1.md b/commentary/Equation1.md
diff --git a/commentary/Equation14.md b/commentary/Equation14.md
diff --git a/commentary/Equation1571.md b/commentary/Equation1571.md
diff --git a/commentary/Equation168.md b/commentary/Equation168.md
diff --git a/commentary/Equation1689.md b/commentary/Equation1689.md
diff --git a/commentary/Equation2.md b/commentary/Equation2.md
diff --git a/commentary/Equation26302.md b/commentary/Equation26302.md
diff --git a/commentary/Equation28770.md b/commentary/Equation28770.md
diff --git a/commentary/Equation345169.md b/commentary/Equation345169.md
diff --git a/commentary/Equation3588.md b/commentary/Equation3588.md
diff --git a/commentary/Equation374794.md b/commentary/Equation374794.md
diff --git a/commentary/Equation381.md b/commentary/Equation381.md
diff --git a/commentary/Equation387.md b/commentary/Equation387.md
diff --git a/commentary/Equation43.md b/commentary/Equation43.md
diff --git a/commentary/Equation4512.md b/commentary/Equation4512.md
diff --git a/commentary/Equation46.md b/commentary/Equation46.md
diff --git a/commentary/Equation477.md b/commentary/Equation477.md
diff --git a/commentary/Equation5105.md b/commentary/Equation5105.md
diff --git a/commentary/Equation65.md b/commentary/Equation65.md
diff --git a/equational_theories/EquationLawConversion.lean b/equational_theories/EquationLawConversion.lean
diff --git a/equational_theories/EquationsCommand.lean b/equational_theories/EquationsCommand.lean
@@ -1,24 +1,8 @@
 import Lean
 import equational_theories.Magma
 import equational_theories.MagmaLaw
-import equational_theories.EquationLawConversion
 
-open Lean Elab Command Law
-
-def mkNatMagmaLaw (declName : Name) : ImportM NatMagmaLaw := do
-  let { env, opts, .. } ← read
-  IO.ofExcept <| unsafe env.evalConstCheck NatMagmaLaw opts ``NatMagmaLaw declName
-
-initialize magmaLawExt : PersistentEnvExtension Name (Name × NatMagmaLaw) (Array (Name × NatMagmaLaw)) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure .empty
-    addImportedFn := Array.concatMapM <| Array.mapM <| fun n ↦ do return (n, ← mkNatMagmaLaw n)
-    addEntryFn := Array.push
-    exportEntriesFn := .map Prod.fst
-  }
-
-def getMagmaLaws {M} [Monad M] [MonadEnv M] : M (Array (Name × NatMagmaLaw)) := do
-  return magmaLawExt.getState (← getEnv)
+open Lean Elab Command
 
 /--
 For a more concise syntax, but more importantly to speed up elaboration (where type inference
@@ -29,10 +13,7 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
   let G := mkIdent (← MonadQuotation.addMacroScope `G)
   let inst := mkIdent (← MonadQuotation.addMacroScope `inst)
   let eqName := mkIdent (.mkSimple s!"Equation{i.getNat}")
-  let finLawName := mkIdent (.mkSimple s!"FinLaw{i.getNat}")
   let lawName := mkIdent (.mkSimple s!"Law{i.getNat}")
-  let finThmName := mkIdent (.str finLawName.getId "models_iff")
-  let thmName := mkIdent (.str lawName.getId "models_iff")
   let mut is := #[]
   let t := tsyn.raw
   -- Collect all identifiers to introduce them as parameters
@@ -60,20 +41,7 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
       | some idx => `(FreeMagma.Leaf $(quote idx.val))
       | none => pure s
   let mut tl : Term := ⟨tl⟩
-  let freeMagmaSize := Syntax.mkNumLit (toString is.size)
-  -- define law over `Fin n`
-  elabCommand (← `(command| abbrev%$tk $finLawName : Law.MagmaLaw (Fin $freeMagmaSize) := $tl))
-  -- compatibility between the `finLaw` and the original equation
-  let modelsIffLemma : Ident := mkIdent (.mkSimple s!"models_iff_{is.size}")
-  elabCommand (← `(command| abbrev%$tk $finThmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $finLawName ↔ $eqName G := $modelsIffLemma $finLawName))
-  -- define the actual law over `Nat`
-  elabCommand (← `(command| abbrev%$tk $lawName : Law.NatMagmaLaw := $tl))
-  -- compatibility between the law and the original equation
-  elabCommand (← `(command| abbrev%$tk $thmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $lawName ↔ $eqName G :=
-                    fun G _ ↦ Iff.trans (Law.satisfies_fin_satisfies_nat G $finLawName).symm ($finThmName G)))
-  -- register the law
-  modifyEnv (magmaLawExt.addEntry · (lawName.getId, ← (mkNatMagmaLaw lawName.getId).run
-    { env := (← getEnv), opts := (← getOptions) }))
+  elabCommand (← `(command| abbrev%$tk $lawName : Law.MagmaLaw Nat := $tl))
   Command.liftTermElabM do
     let declMods ← elabModifiers mods
     -- Create a decl named `declName`

diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -63,10 +63,4 @@ theorem evalInMagma_comp {α β} {G} [Magma G] (f : α → β) (g : β → G) :
   intro x
   induction x <;> simp [fmapFreeMagma, evalInMagma, *]
 
-lemma Fin0_impossible (x : FreeMagma (Fin 0)) : False := by
-  induction x
-  case Leaf l =>
-    cases l; contradiction
-  case Fork => assumption
-
 end FreeMagma
diff --git a/equational_theories/Generated/All4x4Tables/src/check_correct.py b/equational_theories/Generated/All4x4Tables/src/check_correct.py
diff --git a/equational_theories/Generated/All4x4Tables/src/check_redundant.py b/equational_theories/Generated/All4x4Tables/src/check_redundant.py
diff --git a/equational_theories/Generated/All4x4Tables/src/double_check_3x3.py b/equational_theories/Generated/All4x4Tables/src/double_check_3x3.py
diff --git a/equational_theories/Generated/All4x4Tables/src/drive_c_parallel.py b/equational_theories/Generated/All4x4Tables/src/drive_c_parallel.py
diff --git a/equational_theories/Generated/All4x4Tables/src/dump_tables.py b/equational_theories/Generated/All4x4Tables/src/dump_tables.py
diff --git a/equational_theories/Generated/All4x4Tables/src/generate_combined_refutations.sh b/equational_theories/Generated/All4x4Tables/src/generate_combined_refutations.sh
diff --git a/equational_theories/Generated/All4x4Tables/src/generate_lean.py b/equational_theories/Generated/All4x4Tables/src/generate_lean.py
diff --git a/equational_theories/Generated/All4x4Tables/src/prune.py b/equational_theories/Generated/All4x4Tables/src/prune.py
diff --git a/equational_theories/Generated/All4x4Tables/src/write_equations.py b/equational_theories/Generated/All4x4Tables/src/write_equations.py
diff --git a/equational_theories/Generated/FinSearch/src/finite_magma.py b/equational_theories/Generated/FinSearch/src/finite_magma.py
diff --git a/equational_theories/Generated/FinSearch/src/finsearch.py b/equational_theories/Generated/FinSearch/src/finsearch.py
diff --git a/equational_theories/Generated/FinSearch/src/generate_lean.py b/equational_theories/Generated/FinSearch/src/generate_lean.py
diff --git a/equational_theories/Generated/FinSearch/src/parser.py b/equational_theories/Generated/FinSearch/src/parser.py
diff --git a/equational_theories/Generated/FinitePoly/src/finite_poly_generate_lean.py b/equational_theories/Generated/FinitePoly/src/finite_poly_generate_lean.py
diff --git a/equational_theories/Generated/FinitePoly/src/generate_refutations.py b/equational_theories/Generated/FinitePoly/src/generate_refutations.py
diff --git a/equational_theories/Generated/FinitePoly/src/utils.py b/equational_theories/Generated/FinitePoly/src/utils.py
diff --git a/equational_theories/Generated/LinearOps/src/check_correct.py b/equational_theories/Generated/LinearOps/src/check_correct.py
diff --git a/equational_theories/Generated/LinearOps/src/write_equations.py b/equational_theories/Generated/LinearOps/src/write_equations.py
diff --git a/equational_theories/Generated/SimpleRewrites/src/find_redundant.py b/equational_theories/Generated/SimpleRewrites/src/find_redundant.py
diff --git a/equational_theories/Generated/SimpleRewrites/src/find_simple_rewrites.py b/equational_theories/Generated/SimpleRewrites/src/find_simple_rewrites.py
diff --git a/equational_theories/Generated/SimpleRewrites/src/utils.py b/equational_theories/Generated/SimpleRewrites/src/utils.py
diff --git a/equational_theories/Generated/TrivialBruteforce/src/generate_refutations.py b/equational_theories/Generated/TrivialBruteforce/src/generate_refutations.py