Equations command modification (#427)

This PR modifies the `equation` command to automatically generate the corresponding law with variables over `Fin n` (in addition to the law with variables over `Nat` that is already being generated). This is used to show that the automatically generated laws are equivalent to the original equation in terms of satisfiability. Additionally, this PR introduces an environment extension to store all the equational laws, which can be used to export laws as described in #142. This PR also modifies a result transporting laws from `Fin n` to `Nat` to omit the `n != 0` hypothesis. --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
teorth · Oct 9, 2024 · adc92cb · adc92cb
1 parent 534ac2f
commit adc92cb
Show file tree

Hide file tree

Showing 6 changed files with 226 additions and 12 deletions.
diff --git a/blueprint/src/chapter/metatheorems_from_invariants.tex b/blueprint/src/chapter/metatheorems_from_invariants.tex
@@ -171,6 +171,23 @@ \section{Proving metatheorems from invariants in Lean}
 	This offers a way of generating examples of lifting magma families with good computational properties for computing invariants of expressions.
 \end{remark}
 
+\section{Generating laws from equations}
+
+The invariants defined in this chapter are properties of the \emph{syntax} of the equations being considered. In other words, they are properties of the laws associated with the equations, rather than of the equations themselves. Proving non-implications using invariants requires a way to operate on the syntax of the equations and then translate the reasoning back to results about the original equations.
+
+A magma law can be generated from an equation by accessing the syntax used in its definition and converting it to a declaration representing a magma law through metaprogramming. There is a choice in the variable set of the magma law -- one one hand, it can be a finite set whose size matches the number of variables, and on the other hand, it can be the set of natural numbers. The advantage of the former is that one can generate proofs that the satisfiability of the magma law is equivalent to the satisfiability of the original equation (this only needs to be done for variable sets of size upto six, since that is the maximum size currently being considered in the project; it's convenient to prove individual lemmata for each variable set size establishing this equivalence). The advantage of the latter is that it bypasses the need to cast between various finite sets while constructing a model as a counter-example.
+
+One approach is to generate both forms of the law, using the first to establish the equisatisfiability of the law and the equation and then transporting this result to the second form of the law. The conversion from the first form to the second is summarised in the lemma below.
+
+\begin{lemma}\lean{Law.satisfies_fin_satisfies_nat}\leanok[Compatibility between magma laws over finite sets and the natural numbers]\label{compatibility-between-magma-laws}
+	Let $E$ be a magma law defined over $n$ variables and let $\tilde{E}$ be the same equation with variables ranging over the natural numbers (formally, $\tilde{E}$ is the image of $E$ under the canonical map from the finite set with $n$ elements to the natural numbers). Then any magma $M$ satisfies $E$ if and only if it satisfies $\tilde{E}$.
+\end{lemma}
+
+\begin{proof}
+	In the forward direction, suppose $\phi : \mathbb{N} \to M$ is a substitution. Then the restriction of $\phi$ to the first $n$ natural numbers is a substitution for the variables of $E$, and since $M$ satisfies $E$, the law $E$ is true in $M$ under this substitution. Since $\tilde{E}$ is the same as $E$ under the substitution $\phi$, $M$ satisfies $\tilde{E}$.
+
+	In the reverse direction, suppose $\phi : \{0, 2, \ldots, n-1\} \to M$ is a substitution. Then $\phi$ can be extended to a substitution $\tilde{\phi} : \mathbb{N} \to M$ by setting $\tilde{\phi}(i) = \phi(i)$ for $i \leq n$ and $\tilde{\phi}(i) = 0$ for $i \geq n$. Since $M$ satisfies $\tilde{E}$ under the substitution $\tilde{\phi}$, it satisfies $E$ under the restriction of $\tilde{\phi}$ to the first $n$ natural numbers, which is precisely $\phi$. The special case where $n = 0$ is in fact impossible, since there cannot be an expression with no variables.
+\end{proof}
 
 \section{Conclusion: Beyond Invariants}
 We are still lacking:

diff --git a/equational_theories/EquationLawConversion.lean b/equational_theories/EquationLawConversion.lean
@@ -0,0 +1,142 @@
+import equational_theories.MagmaLaw
+
+open Law
+
+/-! Zero variables -/
+
+@[simp] theorem Fin0.match_eq (X : Sort _) (f : Fin 0 → X) : Fin.elim0 = f := by
+  funext i
+  cases i
+  contradiction
+
+theorem Fin0.uncurry {X : Type _} (P : (Fin 0 → X) → Prop) : (∀ f : Fin 0 → X, P f) ↔
+      P Fin.elim0 := by
+  constructor
+  · intro h
+    apply h
+  · intro h f
+    simpa only [← match_eq]
+
+theorem models_iff_0 (law : MagmaLaw (Fin 0)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    satisfiesPhi (Fin.elim0 (α := G)) law := by
+  rw [satisfies, Fin0.uncurry]
+
+/-! One variable -/
+
+@[simp] theorem Fin1.match_eq (X : Sort _) (f : Fin 1 → X) : (fun | 0 => f 0) = f := by
+  funext i
+  match i with
+  | 0 => rfl
+
+theorem Fin1.uncurry {X : Type _} (P : (Fin 1 → X) → Prop) : (∀ f : Fin 1 → X, P f) ↔
+      ∀ x : X, P (fun | 0 => x) := by
+  constructor
+  · intro h _
+    apply h
+  · intro h f
+    have := h (f 0)
+    simpa only [match_eq]
+
+theorem models_iff_1 (law : MagmaLaw (Fin 1)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x : G, satisfiesPhi (fun | 0 => x) law := by
+  rw [satisfies, Fin1.uncurry]
+
+/-! Two variables -/
+
+@[simp] theorem Fin2.match_eq (X : Sort _) (f : Fin 2 → X) : (fun | 0 => f 0 | 1 => f 1) = f := by
+  funext i
+  match i with
+  | 0 | 1 => rfl
+
+theorem Fin2.uncurry {X : Type _} (P : (Fin 2 → X) → Prop) : (∀ f : Fin 2 → X, P f) ↔
+      ∀ x y : X, P (fun | 0 => x | 1 => y) := by
+  constructor
+  · intro h _ _
+    apply h
+  · intro h f
+    have := h (f 0) (f 1)
+    simpa only [match_eq]
+
+theorem models_iff_2 (law : MagmaLaw (Fin 2)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x y : G, satisfiesPhi (fun | 0 => x | 1 => y) law := by
+  rw [satisfies, Fin2.uncurry]
+
+/-! Three variables -/
+
+@[simp] theorem Fin3.match_eq (X : Sort _) (f : Fin 3 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2) = f := by
+  funext i
+  match i with
+  | 0 | 1 | 2 => rfl
+
+theorem Fin3.uncurry {X : Type _} (P : (Fin 3 → X) → Prop) : (∀ f : Fin 3 → X, P f) ↔
+    ∀ x y z : X, P (fun | 0 => x | 1 => y | 2 => z) := by
+  constructor
+  · intro h _ _ _
+    apply h
+  · intro h f
+    have := h (f 0) (f 1) (f 2)
+    simpa only [match_eq]
+
+theorem models_iff_3 (law : MagmaLaw (Fin 3)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x y z : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z) law := by
+  rw [satisfies, Fin3.uncurry]
+
+/-! Four variables -/
+
+@[simp] theorem Fin4.match_eq (X : Sort _) (f : Fin 4 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3) = f := by
+  funext i
+  match i with
+  | 0 | 1 | 2 | 3 => rfl
+
+theorem Fin4.uncurry {X : Type _} (P : (Fin 4 → X) → Prop) : (∀ f : Fin 4 → X, P f) ↔
+    ∀ x y z w : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w) := by
+  constructor
+  · intro h _ _ _ _
+    apply h
+  · intro h f
+    have := h (f 0) (f 1) (f 2) (f 3)
+    simpa only [match_eq]
+
+theorem models_iff_4 (law : MagmaLaw (Fin 4)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x y z w : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w) law := by
+  rw [satisfies, Fin4.uncurry]
+
+/-! Five variables -/
+
+@[simp] theorem Fin5.match_eq (X : Sort _) (f : Fin 5 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3 | 4 => f 4) = f := by
+  funext i
+  match i with
+  | 0 | 1 | 2 | 3 | 4 => rfl
+
+theorem Fin5.uncurry {X : Type _} (P : (Fin 5 → X) → Prop) : (∀ f : Fin 5 → X, P f) ↔
+    ∀ x y z w v : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v) := by
+  constructor
+  · intro h _ _ _ _ _
+    apply h
+  · intro h f
+    have := h (f 0) (f 1) (f 2) (f 3) (f 4)
+    simpa only [match_eq]
+
+theorem models_iff_5 (law : MagmaLaw (Fin 5)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x y z w v : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v) law := by
+  rw [satisfies, Fin5.uncurry]
+
+/-! Six variables -/
+
+@[simp] theorem Fin6.match_eq (X : Sort _) (f : Fin 6 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3 | 4 => f 4 | 5 => f 5) = f := by
+  funext i
+  match i with
+  | 0 | 1 | 2 | 3 | 4 | 5 => rfl
+
+theorem Fin6.uncurry {X : Type _} (P : (Fin 6 → X) → Prop) : (∀ f : Fin 6 → X, P f) ↔
+    ∀ x y z w v u : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v | 5 => u) := by
+  constructor
+  · intro h _ _ _ _ _ _
+    apply h
+  · intro h f
+    have := h (f 0) (f 1) (f 2) (f 3) (f 4) (f 5)
+    simpa only [match_eq]
+
+theorem models_iff_6 (law : MagmaLaw (Fin 6)) (G  : Type _) [Magma G] : G ⊧ law ↔
+    ∀ x y z w v u : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v | 5 => u) law := by
+  rw [satisfies, Fin6.uncurry]
diff --git a/equational_theories/EquationsCommand.lean b/equational_theories/EquationsCommand.lean
@@ -1,8 +1,24 @@
 import Lean
 import equational_theories.Magma
 import equational_theories.MagmaLaw
+import equational_theories.EquationLawConversion
 
-open Lean Elab Command
+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)
 
 /--
 For a more concise syntax, but more importantly to speed up elaboration (where type inference
@@ -14,8 +30,12 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
   let inst := mkIdent (← MonadQuotation.addMacroScope `inst)
   let eqName := .mkSimple s!"Equation{i.getNat}"
   let eqIdent := mkIdent eqName
+  let finLawName := .mkSimple s!"FinLaw{i.getNat}"
+  let finLawIdent := mkIdent finLawName
   let lawName := .mkSimple s!"Law{i.getNat}"
   let lawIdent := mkIdent lawName
+  let finThmName := mkIdent (.str finLawName "models_iff")
+  let thmName := mkIdent (.str lawName "models_iff")
   let mut is := #[]
   let t := tsyn.raw
   -- Collect all identifiers to introduce them as parameters
@@ -53,7 +73,20 @@ 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⟩
-  elabCommand (← `(command| abbrev%$tk $lawIdent : Law.MagmaLaw Nat := $tl))
+  let freeMagmaSize := Syntax.mkNumLit (toString is.size)
+  -- define law over `Fin n`
+  elabCommand (← `(command| abbrev%$tk $finLawIdent : 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 ⊧ $finLawIdent ↔ $eqIdent G := $modelsIffLemma $finLawIdent))
+  -- define the actual law over `Nat`
+  elabCommand (← `(command| abbrev%$tk $lawIdent : Law.NatMagmaLaw := $tl))
+  -- compatibility between the law and the original equation
+  elabCommand (← `(command| abbrev%$tk $thmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $lawIdent ↔ $eqIdent G :=
+                    fun G _ ↦ Iff.trans (Law.satisfies_fin_satisfies_nat G $finLawIdent).symm ($finThmName G)))
+  -- register the law
+  modifyEnv (magmaLawExt.addEntry · (lawName, ← (mkNatMagmaLaw lawName).run
+    { env := (← getEnv), opts := (← getOptions) }))
   Command.liftTermElabM do
     -- TODO: This will go wrong if we are in a namespace. Is this really needed, or is there
     -- a way to pass the current position already to the `(command|` above?

diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -17,6 +17,15 @@ instance (α : Type u) : Coe α (FreeMagma α) where
 
 instance {n : Nat} : OfNat (FreeMagma ℕ) n := ⟨FreeMagma.Leaf n⟩
 
+open Lean in
+def FreeMagma.toJson {α} [ToJson α] : FreeMagma α → Json
+  | FreeMagma.Leaf x => .mkObj [("leaf", Lean.toJson x)]
+  | FreeMagma.Fork x y => .mkObj [("left", toJson x), ("right", toJson y)]
+
+open Lean in
+instance {α} [ToJson α] : ToJson (FreeMagma α) where
+  toJson := FreeMagma.toJson
+
 infixl:65 " ⋆ " => FreeMagma.Fork
 
 @[simp]
@@ -63,6 +72,12 @@ 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
+
 def length {α : Type} : FreeMagma α → Nat
   | .Leaf _ => 1
   | .Fork m1 m2 => FreeMagma.length m1 + FreeMagma.length m2

diff --git a/equational_theories/MagmaLaw.lean b/equational_theories/MagmaLaw.lean
@@ -12,6 +12,8 @@ deriving DecidableEq
 
 infix:60 " ≃ " => MagmaLaw.mk
 
+abbrev NatMagmaLaw := MagmaLaw Nat
+
 end Law
 
 open Law
@@ -141,15 +143,20 @@ private def fin_split {n} {α} (hn : n ≠ 0) (f : Fin n → α) : ∃ g : ℕ
       unfold g
       simp
 
-theorem satisfies_fin_satisfies_nat {n : Nat} (hn : n ≠ 0) (G : Type) [Magma G] (E : MagmaLaw (Fin n))
+theorem satisfies_fin_satisfies_nat {n : Nat} (G : Type) [Magma G] (E : MagmaLaw (Fin n))
     : G ⊧ E ↔ G ⊧ E.fmap Fin.val := by
     apply Iff.intro <;> intro h φ; simp only [ne_eq, satisfies, satisfiesPhi, MagmaLaw.fmap] at *
     · repeat rw [← evalInMagma_comp Fin.val φ]
       exact h (φ ∘ Fin.val)
     · simp only [ne_eq, satisfies, satisfiesPhi, MagmaLaw.fmap] at *
-      obtain ⟨φ', hφ'_val_eq_phi⟩ := fin_split hn φ
-      have hφ' := h φ'
-      repeat rw [← evalInMagma_comp Fin.val φ', hφ'_val_eq_phi] at hφ'
-      exact hφ'
+      if hn:n=0 then
+        subst hn
+        have := FreeMagma.Fin0_impossible E.lhs
+        contradiction
+      else
+        obtain ⟨φ', hφ'_val_eq_phi⟩ := fin_split hn φ
+        have hφ' := h φ'
+        repeat rw [← evalInMagma_comp Fin.val φ', hφ'_val_eq_phi] at hφ'
+        exact hφ'
 
 end Law
diff --git a/equational_theories/Preorder.lean b/equational_theories/Preorder.lean
@@ -71,15 +71,15 @@ instance : Preorder (MagmaLaw α) where
 theorem implies_eq_singleton_models {l₁ l₂ : MagmaLaw α} : l₁ ≤ l₂ ↔ {l₁} ⊧ l₂ := by
   simp only [LE.le, implies, models, satisfiesSet, Ctx, Set.mem_singleton_iff, forall_eq]
 
-theorem Law.implies_fin_implies_nat {n : Nat} (hn : n ≠ 0) {l₁ l₂ : MagmaLaw (Fin n)}
+theorem Law.implies_fin_implies_nat {n : Nat} {l₁ l₂ : MagmaLaw (Fin n)}
     (h : l₁.implies l₂) : (l₁.fmap Fin.val).implies (l₂.fmap Fin.val) := by
   intro G inst hG
-  rw [← satisfies_fin_satisfies_nat hn G l₂]
-  rw [← satisfies_fin_satisfies_nat hn G l₁] at hG
+  rw [← satisfies_fin_satisfies_nat G l₂]
+  rw [← satisfies_fin_satisfies_nat G l₁] at hG
   exact h hG
 
-theorem Law.leq_fin_leq_nat {n : Nat} (hn : n ≠ 0) {l₁ l₂ : MagmaLaw (Fin n)} (h : l₁ ≤ l₂) :
+theorem Law.leq_fin_leq_nat {n : Nat} {l₁ l₂ : MagmaLaw (Fin n)} (h : l₁ ≤ l₂) :
     l₁.fmap Fin.val ≤ l₂.fmap Fin.val :=
-  implies_fin_implies_nat hn h
+  implies_fin_implies_nat h
 
 end Law.MagmaLaw