Track checking function in Pantograph

Stream: Machine Learning for Theorem Proving

[Leni Aniva]

Hi people! I noticed that many people didn't know about the track checking function in Pantograph. It is useful for testing whole-file proofs.

It checks whether a proof conforms to a spec file:

src = """
def f : Nat -> Nat := sorry
theorem property (n : Nat) : f n = n + 1 := sorry
"""
dst = """
def f (x : Nat) := x + 1
theorem property (n : Nat) : f n = n + 1 := rfl
"""
await server.check_track_async(src, dst)

it detects tampering of definitions and introduction of additional axioms, but axioms that are present in both files are fine.

[Eric Wieser]

Does it allow this?

src = """
import Mathlib

theorem foo : { (x, y) | x * y < 0} = ∅ := by
  sorry
"""
dst = """
import Mathlib

def bar := { (x, y) | x * y < 0}

theorem foo : { (x, y) | x * y < 0} = ∅ := by
  simp
"""
await server.check_track_async(src, dst)

[Leni Aniva]

Eric Wieser said:

Does it allow this?

src = """
import Mathlib

theorem foo : { (x, y) | x * y < 0} = ∅ := by
  sorry
"""
dst = """
import Mathlib

def bar := { (x, y) | x * y < 0}

theorem foo : { (x, y) | x * y < 0} = ∅ := by
  simp
"""
await server.check_track_async(src, dst)

Yes. You're free to introduce as many non-axiom definitions as you want. Auxiliary inductives and structures are allowed too

[Eric Wieser]

Right, the key thing there is that the meaning of the | changes as a result of the added bar

[Leni Aniva]

Eric Wieser said:

Right, the key thing there is that the meaning of the | changes as a result of the added bar

if it maps to a different symbol then check track will raise an error about tampering

[Eric Wieser]

So just to check, that's "yes, I checked", and not "yes, I'd hope so"?

[Leni Aniva]

Eric Wieser said:

So just to check, that's "yes, I checked", and not "yes, I'd hope so"?

There are unit tests in the Pantograph repo concerning this use case if you're interested

[Eric Wieser]

To be super clear; in the first case the theorem is about foo._match_1, in the second case it is about bar._match_1. The two are equal, but not without agressive (and possibly in more contrived examples, recursive) unfolding

[Leni Aniva]

It is possible to do such unfolding but it is not enabled for this use case. Any divergence in the symbol representation will lead to an error

[Eric Wieser]

So for my code sample above I guess the answer is "no, it rejects it"

[Leni Aniva]

Eric Wieser said:

So for my code sample above I guess the answer is "no, it rejects it"

Yes. It is rejected. I'm testing if the existing matcher unfolding function can make it an acceptance instead

[Jason Rute]

The two are equal

To be clear, you are saying the two versions of foo are definitionally equal? Or something a bit nicer than that? And to check this this, you would have to check for such equality between the before and after terms. It is not enough alone to look just at the terms because one term has foo._match_1 and the other has bar._match_1, right?

@GasStationManager How does SafeVerify behave on this example? @Henrik Böving how will your upcoming tool behave on this example?

[Jason Rute]

@Leni Aniva Is this tool similar to those two tools I just mentioned? Can it verify multi-file proofs (something the current version of SafeVerify can't do)?

[Leni Aniva]

Jason Rute said:

Leni Aniva Is this tool similar to those too I mentioned above. Can it verify multi-file proofs (something the current version of SafeVerify can't do).?

No it cannot verify multifile proofs because it would mean importing two Lean repos with the same name at the same time. I don't think Lean will allow this kind of operation.

[Henrik Böving]

Jason Rute said:

The two are equal

To be clear, you are saying the two versions of foo are definitionally equal? Or something a bit nicer than that? And to check this this, you would have to check for such equality between the before and after terms. It is not enough alone to look just at the terms because one term has foo._match_1 and the other has bar._match_1, right?

GasStationManager How does SafeVerify behave on this example? Henrik Böving how will your upcoming tool behave on this example?

reject

[Henrik Böving]

SafeVerify will reject too

[Henrik Böving]

And they are not definitionally equal, they are at best provably equal. This kind of side effect from introducing other definitions is a bit tricky.

[Leni Aniva]

Maybe aggressive matcher unfolding can lead to these two exprs being equal

[Henrik Böving]

Note that you should not unfold using matchMatcherApp? if you want to be a trustworthy checker, it relies on unverified informations from env extensions

[Leni Aniva]

Henrik Böving said:

Note that you should not unfold using matchMatcherApp? if you want to be a trustworthy checker, it relies on unverified informations from env extensions

Then how can this system unfold matchers in this case?

Maybe the checker should just unfold every definition that is not present in the spec file.

[Henrik Böving]

With my OpenBSD-paranoia-hat on I would say just don't do anything clever and reject, tricks like this will likely bite a trustworthy checker somewhere down the line. If you really want to unfold and avoid looking at env extensions at the same time you can just inspect the definition of the matcher from the environment.

[Leni Aniva]

Henrik Böving said:

With my OpenBSD-paranoia-hat on I would say just don't do anything clever and reject, tricks like this will likely bite a trustworthy checker somewhere down the line. If you really want to unfold and avoid looking at env extensions at the same time you can just inspect the definition of the matcher from the environment.

What if I just make unfolding of matchers an optional feature? All the constants still have to go through replay so they'll be checked for their type correctness

[Leni Aniva]

Pantograph's definition unfolding function could make this example into an accept

[Leni Aniva]

I found a way to achieve acceptance of this example without querying env extensions. The method is to unfold all definitions which are not in the intersection of spec and proof files.

[Jason Rute]

With my OpenBSD-paranoia-hat on

I'm constantly trying to balance being paranoid of AI hacks and paranoid that I'm being too paranoid of AI hacks and thereby rejecting perfectly good code. (Maybe I just need to switch to Metamath. :joy:)

[Marcelo Fornet]

Eric Wieser said:

To be super clear; in the first case the theorem is about foo._match_1, in the second case it is about bar._match_1. The two are equal, but not without agressive (and possibly in more contrived examples, recursive) unfolding

Can you elaborate a bit more on what are the differences here?

the meaning of the | changes as a result of the added bar

In which way does the meaning changes due to adding bar?

[Leni Aniva]

Marcelo Fornet said:

Eric Wieser said:

To be super clear; in the first case the theorem is about foo._match_1, in the second case it is about bar._match_1. The two are equal, but not without agressive (and possibly in more contrived examples, recursive) unfolding

Can you elaborate a bit more on what are the differences here?

the meaning of the | changes as a result of the added bar

In which way does the meaning changes due to adding bar?

Adding the bar definition changes how Lean internally represents foo

[Marcelo Fornet]

Leni Aniva said:

Marcelo Fornet said:

Eric Wieser said:

To be super clear; in the first case the theorem is about foo._match_1, in the second case it is about bar._match_1. The two are equal, but not without agressive (and possibly in more contrived examples, recursive) unfolding

Can you elaborate a bit more on what are the differences here?

the meaning of the | changes as a result of the added bar

In which way does the meaning changes due to adding bar?

Adding the bar definition changes how Lean internally represents foo

why is that the case?

sorry for being annoying, I'm genuinely curious about it

[Leni Aniva]

it has something to do with the elaborator generating auxiliary definitions. im not sure whats the exact process

[Eric Wieser]

Auxiliary definitions are cached within a file based on their value, I think

[Henrik Böving]

Note that one can work around this by keeping the target statement in a separate file as a definition that you just don't touch.