push_neg behavior

Stream: mathlib4

[Alice Laroche]

In lean3 mathlib, push_neg use classical logic to be able to rewrite var in the context.
I made a port of push_neg that only use constructive logic and then is only able to change the goal.
So i was wondering if we should make two tactic :
One that act on the goal and only use constructive logic, and one that can act on the context and use classical logique

[Mario Carneiro]

why would the constructive version be limited to just the goal? Anyway the whole point of this tactic was to do classical rewrites, I'm sure @Patrick Massot can tell the story better than I. We have a precedent for using ! in tactics to enable "classical mode" but I'm not sure how acceptable that is to the people that use this tactic a lot

[Mario Carneiro]

Relevant: is push_neg classical?

[Patrick Massot]

Of course push_neg is classical. But anyone is welcome to write another tactic half_push_neg or masochistic_push_neg that is intuistionistic. You can even write a don't_push_neg tactic that simply write an error message "You seem to have too much fun, you should remove a couple more axioms".

[Alice Laroche]

Mario Carneiro said:

why would the constructive version be limited to just the goal? Anyway the whole point of this tactic was to do classical rewrites, I'm sure Patrick Massot can tell the story better than I. We have a precedent for using ! in tactics to enable "classical mode" but I'm not sure how acceptable that is to the people that use this tactic a lot

Well, the constructive version would be limited because you loose some equivalence so you can't do the same thing on the goal and on the var

[Mario Carneiro]

I assume you are only doing bidirectional rewrites here, because otherwise it could potentially make the goal unprovable

[Mario Carneiro]

in which case you can do the same thing on the goal and on the hypotheses (which is to say, not much)

[Mario Carneiro]

I kind of agree with Patrick here. Pushing negations isn't really a thing you can do in general intuitionistically, so presenting a tactic that fails half the time seems like a poor user experience

[Mario Carneiro]

It's like if we had a prenex tactic to put things in prenex normal form, but because it only does intuitionistic rewrites it just fails in all nontrivial cases

[Wrenna Robson]

It would be quite nice to know when something I'm doing with push_neg can be done in a constructive way, but I'm not sure your idea helps with that...

[Yury G. Kudryashov]

Hi, I have two more push_neg failures (possibly, the same bug):

import Mathlib.Order.Basic

variable [LinearOrder α] [One α] [Mul α]

example (x : α) : x ≤ 1 := by
  set a := x * x
  by_contra' h
  guard_hyp h : 1 < x -- works


example (x : α) : x ≤ 1 := by
  let a := x * x
  by_contra' h
  guard_hyp h : 1 < x -- fails

example (x : α) : x ≤ 1 := by
  set a := x * x
  have : a ≤ a := le_rfl
  by_contra' h
  guard_hyp h : 1 < x -- fails

[Damiano Testa]

I think that in the match, the presence of the let messes up one of the cases extracting the \not. I'm seeing if I can add a letE match to fix the issue.

[Damiano Testa]

There seems to be some mdata embedded in the term. I do not think that mdata was a thing in Lean3, which might explain why this fails now, but was not failing before.

[Damiano Testa]

If you add

  let ex := ex.consumeMData

just above the match on this line, your examples seem to parse.

[Damiano Testa]

I can PR this "fix", but I do not really understand the consequences of it.

However, since mdata was not a field of expr in Lean3, it should not be a big deal for the port anyway... :upside_down:

[Damiano Testa]

EDIT: permalink fixed above.

[Damiano Testa]

#5082, in case you want to experiment (and to check that it does not break more than it fixes).

[Damiano Testa]

This is very cool: the PR had a failure at a porting note and now a rw [not_not] can go away!

[Ruben Van de Velde]

That's !4#5082

[Damiano Testa]

This PR is very satisfying: every time that CI failed to build with the change has been an improvement! I'm going to stop for the day, but if someone else wants to see if there are further errors and fix them, it is very gratifying!

[Ruben Van de Velde]

I'll take a look now

[Damiano Testa]

Maybe all issues have been resolved?

[Damiano Testa]

One thing that may be worth checking is that with the current "fix", stripping annotations happens after taking whnf. I do not know if there is the need to take whnf of the un-annotated Expr.

[Ruben Van de Velde]

It's rebuilding the world because you touched the tactic, but it's up to 2805/3256. Still a few hundred files that could be broken :)

[Damiano Testa]

Alright!

[Damiano Testa]

It might be interesting to grep around contra/push_negs, searching for porting notes or not... and see if there are more regressions.

[Patrick Massot]

Damiano Testa said:

If you add

  let ex := ex.consumeMData

just above the match on this line, your examples seem to parse.

I've being writing this kind of consumeMDatalines in my meta-code as well, but I'd be interested to know if @Gabriel Ebner or @Sebastian Ullrich think this is a dangerous "blind fix".

[Damiano Testa]

Yes, I would like to know that as well. In this situation, it seems to have resolved several porting notes, so maybe it is an ok fix.

This seems like another one of these "blanket" debugging checklists: have you instantiated metavars? Have you focused? Have you whnfed? Have you withContexted?

Now, have you consumed annotations?

[Ruben Van de Velde]

Nope, looks like it's going to be all green!

[Damiano Testa]

I added tests that passed to by_contra, but have not thought of looking at push_neg: there is still some possibility of failure!

[Damiano Testa]

I labeled the PR as awaiting review, and would be very happy to receive further comments about whether the current version is suitable!