Vampire proof to cleaner proof

Stream: new members

[Michael Bucko]

I am trying to simplify this Vampire proof. What are your suggestions?

theorem Equation1294_implies_Equation2500 (G : Type*) [Magma G] (h : Equation1294 G) : Equation2500 G := by
  by_contra nh
  simp only [not_forall] at nh
  obtain ⟨sK0, sK1, sK2, nh⟩ := nh
  have eq9 (X0 X1 X2 X3 : G) : (X1 ◇ (((X0 ◇ X1) ◇ X2) ◇ X3)) = X0 := mod_symm (h ..)
  have eq10 : sK0 ≠ (sK1 ◇ ((sK0 ◇ sK0) ◇ sK2) ◇ sK1) := mod_symm nh
  have eq13 (X0 X1 X3 : G) : (X1 ◇ X3) = X0 := superpose eq9 eq9
  have eq14 (X1 X4 : G) : X1 = X4 := superpose eq9 eq13
  have eq21 (X0 : G) : sK0 ≠ X0 := superpose eq13 eq10

  subsumption eq21 eq14

[Rémy Degenne]

You should post a #mwe (including imports), so that people can get working code when they open your code block in the online editor.

[Daniel Weber]

Simplify in what way? You can replace all of the superpose with (congrArg motive (eq1 a1 a2 ...)).mpr (eq2 b1 b2 ...) (perhaps with symm for some), with appropriate motive, a1, a2, ..., b1, b2, ..., for some value of simplify

[Daniel Weber]

You could also replace subsumption with something similar, and mod_symm with either nothing or symm (I'm not sure which here)

[Michael Bucko]

@Daniel Weber Both of your suggestions are already very helpful!

Here's an example via @Mario Carneiro . He translated this

@[equational_result]
theorem Equation854_implies_Equation378 (G : Type*) [Magma G] (h : Equation854 G) : Equation378 G := by
  by_contra nh
  simp only [not_forall] at nh
  obtain ⟨sK0, sK1, nh⟩ := nh
  have eq9 (X0 X1 X2 : G) : (X0 ◇ ((X1 ◇ X2) ◇ (X0 ◇ X2))) = X0 := mod_symm (h ..)
  have eq10 : (sK0 ◇ sK1) ≠ ((sK0 ◇ sK1) ◇ sK1) := mod_symm nh
  have eq11 (X0 X1 X2 X3 : G) : (X3 ◇ (X0 ◇ (X3 ◇ ((X1 ◇ X2) ◇ (X0 ◇ X2))))) = X3 := superpose eq9 eq9 -- superposition 9,9, 9 into 9, unify on (0).2 in 9 and (0).1.2.1 in 9
  have eq13 (X0 X1 X2 X3 X4 : G) : (X3 ◇ (X4 ◇ (X3 ◇ (X0 ◇ (X4 ◇ ((X1 ◇ X2) ◇ (X0 ◇ X2))))))) = X3 := superpose eq9 eq11 -- superposition 11,9, 9 into 11, unify on (0).2 in 9 and (0).1.2.2.2.1 in 11
  have eq54 (X0 X1 X2 X3 : G) : (X1 ◇ (X0 ◇ ((X2 ◇ X3) ◇ (X0 ◇ X3)))) = ((X1 ◇ (X0 ◇ ((X2 ◇ X3) ◇ (X0 ◇ X3)))) ◇ X0) := superpose eq9 eq13 -- superposition 13,9, 9 into 13, unify on (0).2 in 9 and (0).1.2 in 13
  have eq62 (X0 X1 : G) : (X1 ◇ X0) = ((X1 ◇ X0) ◇ X0) := superpose eq9 eq54 -- forward demodulation 54,9
  have eq137 : (sK0 ◇ sK1) ≠ (sK0 ◇ sK1) := superpose eq62 eq10 -- superposition 10,62, 62 into 10, unify on (0).2 in 62 and (0).2 in 10
  subsumption eq137 rfl

into this

def G := FreeMagmaWithLaws ℕ {Law854}
instance : Magma G := inferInstanceAs (Magma (FreeMagmaWithLaws ..))

theorem law : ∀ (x y z : G), x = x ◇ ((y ◇ z) ◇ (x ◇ z)) :=
  Law854.models_iff.1 <| FreeMagmaWithLaws.isModel _ _ _ rfl

theorem l378 (x y : G) : x ◇ y = (x ◇ y) ◇ y := by
  have yy := (law y y ((y ◇ y) ◇ (y ◇ y))).symm; rw [← law y y y] at yy
  exact (law _ y (y ◇ y)).trans (by rw [yy, ← law])

The way I see it (please correct me if I am wrong) is that FreeMagma gets a law (through FreeMagmaWithLaws), and that eventually leads to a have (via symm)-rw-exact line.

If I could get enough laws like this, I could probably translate all (or many of) the Vampire proofs into something simpler (@Mario Carneiro suggested I should have a look into this).

(The long-term solution could be to use diffusion models to dream up higher-order concepts, a'la FreeMagmaWithLaws with special laws; the short-term solution could be learning how to construct those higher-order objects -- apparently those Vampire proofs in this case (almost) always are by contra (through the derivation of equations using mostly mod_symm and superpose))

[Michael Bucko]

Rémy Degenne schrieb:

You should post a #mwe (including imports), so that people can get working code when they open your code block in the online editor.

Here's the code, but I guess it's specific to the ET project (importing Magma and Equations):

import Mathlib.Tactic
import Mathlib.Data.Nat.Defs
import equational_theories.Equations.All
import equational_theories.Magma
import Mathlib.Tactic.Simp

theorem Equation1294_implies_Equation2500 (G : Type*) [Magma G] (h : Equation1294 G) : Equation2500 G := by
  by_contra nh
  simp only [not_forall] at nh
  obtain ⟨sK0, sK1, sK2, nh⟩ := nh
  have eq9 (X0 X1 X2 X3 : G) : (X1 ◇ (((X0 ◇ X1) ◇ X2) ◇ X3)) = X0 := mod_symm (h ..)
  have eq10 : sK0 ≠ (sK1 ◇ ((sK0 ◇ sK0) ◇ sK2) ◇ sK1) := mod_symm nh
  have eq13 (X0 X1 X3 : G) : (X1 ◇ X3) = X0 := superpose eq9 eq9
  have eq14 (X1 X4 : G) : X1 = X4 := superpose eq9 eq13
  have eq21 (X0 : G) : sK0 ≠ X0 := superpose eq13 eq10

  subsumption eq21 eq14