You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
How hard would it be to check whether negation is proven instead? #23
Hi! As it happens we just merged in a PR by @Paul-Lez that adds this feature. It is a --disproofs CLI flag. We still need to update the Readme, but it is in main now and you can try it out! Let us know if any issues arise.
@Paul-Lez I am sorry I changed the message abruptly, I thought I was fast enough :D
The implementation looks very similar to what I did for our internal fork indeed but I decided to allow only the "canonical negation" form in my version, meaning that everything has to be wrapped in for all if there are args and then we do not (forall (args) : P)
I thought it's hard to cover all cases because negation can be written in many ways so I decided to only allow the canonical form. From what I understand your implementation also permits (there exists (args) : not P) as a negation of (args) : P, does it also permit stuff like (args) : P -> False and perhaps some other ways of writing the negation?
@mertunsall Fair question. The idea of the implementation wasn't to be exhaustive about all possible ways of writing the negation, but instead to take the "pushed negation" (roughly speaking, the output of the push_neg tactic on the negated goal) as the "canonical form". For example,
theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := by
sorry
theorem foo.disproof : ∃ x : Nat, ¬ (¬ 1 + 1 = 2) := by
use 0
simp
isn't allowed in this setup. In your use case, do you need to be able to vary what forms are considered?
The reason for this set up is that some other users have taken "pushed negation" as the canonical form. Is that form of negation fine for you? Alternatively, once could add a flag to the negation mode for users to be able to use the form you had in mind.
I see. We're training our models to obey the format where everything is placed inside a forall and negated inside (or if there is there exists you don't need to add for all, you can just negate). I think it would be nice if the official safeverify covered that too.
Activity
GasStationManager commentedon Apr 22, 2026
Hi! As it happens we just merged in a PR by @Paul-Lez that adds this feature. It is a --disproofs CLI flag. We still need to update the Readme, but it is in main now and you can try it out! Let us know if any issues arise.
mertunsall commentedon Apr 23, 2026
How does this make sure all negation cases are covered?
mertunsall commentedon Apr 23, 2026
@Paul-Lez I am sorry I changed the message abruptly, I thought I was fast enough :D
The implementation looks very similar to what I did for our internal fork indeed but I decided to allow only the "canonical negation" form in my version, meaning that everything has to be wrapped in for all if there are args and then we do
not (forall (args) : P)mertunsall commentedon Apr 23, 2026
This helped me keep my PR significantly shorter. (I am really not that good at Lean so I wanted to ensure not to make mistakes)
Paul-Lez commentedon Apr 23, 2026
@mertunsall Is the concern that the mechanism that pushes the
notthrough the quantifiers may not cover all possible cases?mertunsall commentedon Apr 23, 2026
I thought it's hard to cover all cases because negation can be written in many ways so I decided to only allow the canonical form. From what I understand your implementation also permits
(there exists (args) : not P)as a negation of(args) : P, does it also permit stuff like(args) : P -> Falseand perhaps some other ways of writing the negation?Paul-Lez commentedon Apr 26, 2026
@mertunsall Fair question. The idea of the implementation wasn't to be exhaustive about all possible ways of writing the negation, but instead to take the "pushed negation" (roughly speaking, the output of the
push_negtactic on the negated goal) as the "canonical form". For example,isn't allowed in this setup. In your use case, do you need to be able to vary what forms are considered?
mertunsall commentedon Apr 28, 2026
I see. In my use case, I only allow one form and make it clear to the consumer of safe verify
Paul-Lez commentedon Apr 28, 2026
The reason for this set up is that some other users have taken "pushed negation" as the canonical form. Is that form of negation fine for you? Alternatively, once could add a flag to the negation mode for users to be able to use the form you had in mind.
mertunsall commentedon May 4, 2026
I see. We're training our models to obey the format where everything is placed inside a
foralland negated inside (or if there is there exists you don't need to add for all, you can just negate). I think it would be nice if the official safeverify covered that too.