Efficent representation of refutations

Stream: Equational

[Joachim Breitner]

Ah, I missed your message above, sorry!

Yes, something like that would help a lot. I think this ties into the wider question of what the “interface” between the individual lean files and the tools that scrape them for proven facts should be. Also see the topic #Equational > Where to store the ground truth of implications? and maybe open a new topic for this discussion.

[Vlad Tsyrklevich]

Just for future reference, here is something that I've been working on that does just this:

theorem multi_eq1 : ∃ (G: Type) (_: Magma G), (Equation8 G ∧ Equation99 G ∧ Equation359 G ∧ Equation411 G ∧ Equation817 G ∧ Equation1020 G ∧ Equation1223 G ∧ Equation1832 G ∧ Equation3253 G ∧ Equation3659 G ∧ Equation3862 G ∧ Equation4065 G) ∧ ¬ Equation3 G ∧ ¬ Equation23 G ∧ ¬ Equation47 G ∧ ¬ Equation151 G ∧ ¬ Equation203 G ∧ ¬ Equation255 G ∧ ¬ Equation307 G ∧ ¬ Equation614 G ∧ ¬ Equation1426 G ∧ ¬ Equation1629 G ∧ ¬ Equation2035 G ∧ ¬ Equation2238 G ∧ ¬ Equation2441 G ∧ ¬ Equation2644 G ∧ ¬ Equation2847 G ∧ ¬ Equation3050 G ∧ ¬ Equation3456 G ∧ ¬ Equation4380 G := by
  let hG : Magma Nat := {
    op := fun x y => if x = 0 ∧ y = 0 then 1 else x
  }
  use ℕ, hG

  apply And.intro
  focus
    repeat' apply And.intro
    all_goals {
      focus
        intro x;
        simp [hG];
        split_ifs <;> simp_all
    }

  repeat' apply And.intro
  all_goals {
    by_contra h
    specialize h 0
    dsimp [hG] at h
    linarith
  }

[Joachim Breitner]

Indeed, with this format every file could be a single theorem that doesn’t even mention the monoid, e.g.

theorems someFacts: ∃ (G: Type) (_: Magma G), Equation1 G ∧  Equation3 G ∧ ¬ Equation3 G ∧ ¬ Equation4 G

that can be proven in one go with by decide (or maybe by native_decide)

[Notification Bot]

3 messages were moved here from #Equational > Resolving >60% of cases with non-implications automatically by Joachim Breitner.

[Joachim Breitner]

Moved this to a new topic

[Vlad Tsyrklevich]

But yes, I agree it has to do with project structure. There is no way to maintain this project with 4700**2 theorems so I figured we must do something like this, and nicely, it works well with proving non-implies cases which are plentiful letting us cut the size of the project down

[Joachim Breitner]

We could even define a function

Refutations : List Nat → List Nat → Prop

for this theorem statement, which would make the lemma statement much shorter and easier to parse:

theorem multi_eq1 : Refutations [8,99,359] [2847,3050]

(for this we have to store the list of quations as a list, but that’s a good idea anyways, probably.)

[Joachim Breitner]

Actually, I like that. Let me implement that.

[Vlad Tsyrklevich]

There could be the same thing for implies, e.g. if EqA implies B,C,D,E, etc. I'm working on something like that as well at the moment. This does make introspecting on these proofs more difficult without a tool to print the list of implications/non-implications, but that's already a given with size of the search-space

[Joachim Breitner]

Not sure if this will scale to 4000 entries, but as a POC for the syntax this seems to work:

syntax (name := refutes)
  "Facts " ident " [" num,* "] " " [" num,* "]" : term

open Lean Elab in
macro_rules
  | `(Facts $G [$s:num, $ss,*] [$rs,*]) =>  do
    let i : Ident := mkIdent (.mkSimple s!"Equation{s.getNat}")
    `($i $G ∧ Facts $G [$ss,*] [$rs,*])
  | `(Facts $G [$s:num] [$rs,*]) =>  do
    let i : Ident := mkIdent (.mkSimple s!"Equation{s.getNat}")
    `($i $G ∧ Facts $G [] [$rs,*])
  | `(Facts $G [] [$r, $rs,*]) =>  do
    let i : Ident := mkIdent (.mkSimple s!"Equation{r.getNat}")
    `(¬ $i $G ∧ Facts $G [] [$rs,*])
  | `(Facts $G [] [$r]) =>  do
    let i : Ident := mkIdent (.mkSimple s!"Equation{r.getNat}")
    `(¬ $i $G)

example (G : Type _) [Magma G] :
   Facts G [1, 2] [4, 5] ↔ (Equation1 G ∧ Equation2 G ∧ ¬ Equation4 G ∧ ¬ Equation5 G) :=
   Iff.rfl

[Joachim Breitner]

Ok, that runs into “deep recursion” :sweat_smile:

[Vlad Tsyrklevich]

Copying your code (getting rid of mathlib, Type* -> Type _) significantly improved my runtime for some brute force scripts locally. Running ~5k test theorems still takes almost a minute on my laptop though. It would be great if we could run these even faster, though as the graph gets filled out this will matter less.

[Daniel Weber]

Perhaps we could do something like docs#List.TFAE, but with two lists?

[Joachim Breitner]

Ok, this elaborates fast enough:

syntax "Facts " term:max " [" num,* "] " " [" num,* "]" : term

open Lean Meta Elab Term Tactic Parser.Term in
elab_rules : term | `(Facts $G [ $sats,* ] [ $refs,*]) => do
  let G ← elabTerm G none
  let some u := (← getLevel G).dec | throwError "expected G to be a type"
  let inst ← synthInstance (mkApp (mkConst ``Magma [u]) G)
  let s := sats.getElems.map fun ⟨s⟩ =>
    let n := .mkSimple s!"Equation{s.toNat}"
    mkApp2 (mkConst n [u]) G inst
  let r := refs.getElems.map fun ⟨s⟩ =>
    let n := .mkSimple s!"Equation{s.toNat}"
    mkApp (mkConst ``Not)  (mkApp2 (mkConst n [u]) G inst)
  let e := mkAndN (s ++ r).toList
  return e

[Vlad Tsyrklevich]

Perhaps you have the answer for what I'm hitting now then? I am hitting deep recursion now as well. Eq4 implies 1212 other equations by trivial rewriting, but trying to prove the conjunction of 1212 equations fails. I assume that it is better to prove them all at once then having individual implies. Example code here https://gist.github.com/vlad902/bec06a595758bf18569252177afef79a I'm not sure if your fix is different than what I am hitting.

[Joachim Breitner]

My file now looks like this, but with larger lists:

-- This is an example file, repesenting the generated files, but with shorter lists


import equational_theories.FinitePoly.Common
import equational_theories.FinitePoly.DecideBang
import equational_theories.FinitePoly.FactsSyntax

/-!
This file is generated from the following refutation as produced by
random generation of polynomials:
'(4 * x**2 + 4 * y**2 + 4 * x + 4 * y + 0 * x * y) % 5' (0, 42, 3252, 3318, 3341, 3455, 3521, 3544, 3861, 3914, 3963, 4064, 4117, 4166, 4282, 4357, 4379, 4397, 4404, 4434, 4441, 4481, 4530, 4543, 4634, 4676)

-/

set_option maxRecDepth 10000000
set_option maxHeartbeats 200000000
set_option synthInstance.maxHeartbeats 200000000


/-! The magma definition -/
def «FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y» : Magma (Fin 5) where
  op x y := 4 * x*x + 4 * y*y + 4 * x + 4 * y

/-! The facts -/
theorem «Facts from FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y» :
  ∃ (G : Type) (_ : Magma G), Facts G [1, 43, 3253] [2, 3, 4] := by
    refine ⟨Fin 5, «FinitePoly 4 * x² + 4 * y² + 4 * x + 4 * y», ?_⟩
    decide!

and I am getting

equational_theories/FinitePoly/Refutation0.lean:25:4: error: failed to synthesize

:confused:
(For smaller lists it works.)

[Joachim Breitner]

Progress using

    apply_rules only [And.intro]
    all_goals decide!

so that we don’t do the conjunction within decide

[Joachim Breitner]

Success! I had to write some meta code for this, but now one file is 28k, all files 3,5M, and each file takes 25s to process (which certainly can be sped up)