metavariable bug

Stream: general

[Kevin Buzzard]

I tried to get a mathlib-free version but I need swap which is apparently not in core. The below code looks really innocent but honestly you might want to look away instead of at the tactic state after the dsimp.

import tactic.interactive -- needed for `swap`

example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  (∃ (U : set X), (P U ∧ U ⊆ S) ∧ x ∈ U) →
  (∃ (U : set X), P U ∧ U ⊆ S ∧ x ∈ U) :=
begin
  intro h,
  cases h with U hU,
  cases hU with h1 h2,
  cases h1 with h3 h4,
  split,
  swap,
  intro x,
  swap,
  dsimp at *, -- this causes the problem
  exact ⟨h3, h4, h2⟩,
end

[Arthur Paulino]

just dsimp does very little on the goal and is accepted. dsimp at * does much more unfolding on the goal and, naively looking at the goal state only, doesn't touch anything but the goal too (but is not accepted).

[Arthur Paulino]

More digging: if I extract the goal before split, the bug doesn't show up anymore:

example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X)
  (U : set X)
  (h2 : x ∈ U)
  (h3 : P U)
  (h4 : U ⊆ S) :
  ∃ (U : set X), P U ∧ U ⊆ S ∧ x ∈ U :=
begin
  split,
  swap,
  intro x,
  swap,
  dsimp at *, -- this no longer causes the problem
  exact ⟨h3, h4, h2⟩,
end

[Arthur Paulino]

So maybe the bug is either in intro, cases or dsimp

[Arthur Paulino]

This is the code that runs for the wildcard location of dsimp:

  do n ← revert_all,
     dsimp_target s u {zeta := ff ..cfg},
     intron n

If I change the order, as in:

  do n ← revert_all,
     intron n,
     dsimp_target s u {zeta := ff ..cfg}

The problem disappears. Is this approach problematic?

[Alex J. Best]

Doing revert and then intro is a no-op, the point of those lines is to move all hypotheses into the goal, dsimp the resulting thing and then extract all the hypotheses again. Maybe there is a better way to accomplish this though

[Alex J. Best]

It would be good to look at the git history why the wildcard case is special cased, and see if the mathlib build breaks if it is removed

[Arthur Paulino]

Hm, from the fact that it says "goals accomplished" but the kernel rejects it, can we conclude that the current way to do it is actually inconsistent?

[Arthur Paulino]

Alex J. Best said:

It would be good to look at the git history why the wildcard case is special cased, and see if the mathlib build breaks if it is removed

There's a comment on the wildcard code saying:

/- Remark: we cannot revert frozen local instances.
     We disable zeta expansion because to prevent `intron n` from failing.
     Another option is to put a "marker" at the current target, and
     implement `intro_upto_marker`. -/

[Alex J. Best]

I'd guess that there is in fact a deeper bug that should be found

[Alex J. Best]

I don't think the comment makes too much difference, even with zeta expansion enabled the bug still occurs

[Alex J. Best]

set_option trace.dsimplify true
example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  (∃ (U : set X), (P U)) →
  (∃ (U : set X), P U) :=
begin
  intro h,
  cases h with U hU,
  split,
  swap,
  intro x,
  swap,
  -- rw id,
  dsimp at *, -- this causes the problem
  exact hU,
end

is the best MWE I have

[Alex J. Best]

It seems to me that dsimp is removing an id application that is necessary to tell lean the types of everything involved

[Arthur Paulino]

set_option trace.dsimplify true
example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  (∃ (U : set X), (P U)) →
  (∃ (U : set X), P U) :=
begin
  intro h,
  cases h with U hU,
  split,
  work_on_goal 1 {intro x},
  dsimp at *, -- this causes the problem
  exact hU,
end

is just a tad smaller, but doesn't remove anything significant

[Arthur Paulino]

This is dsimp_target:

meta def dsimp_target (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit :=
do
  s ← get_simp_lemmas_or_default s,
  t ← target >>= instantiate_mvars,
  s.dsimplify u t cfg >>= unsafe_change

And this is unsafe_change:

/-- Change the target of the main goal.
   The input expression must be definitionally equal to the current target.
   The tactic does not check whether `e`
   is definitionally equal to the current target. The error will only be detected by the kernel type checker. -/
meta def unsafe_change (e : expr) : tactic unit :=
change e ff

[Alex J. Best]

Even using safe change (change e tt) it has the same behaviour

[Arthur Paulino]

So if change e tt is resulting on "goals accomplished", then is it safe to conclude that such change type checks at that point?

[Arthur Paulino]

If not, then we might need to dive in C code to find the bug

[Alex J. Best]

Weirdly enough running recover or even

  trace result

after the last exact line makes the proof succeed

[Arthur Paulino]

Okay this is beyond my understanding. I can only hope it won't happen in Lean 4 :sweat_smile:

[Arthur Paulino]

Even smaller #mwe:

example (P : set nat → Prop) :
  (∃ (U : set nat), P U) → (∃ (U : set nat), P U) :=
begin
  intro h,
  cases h with U hU,
  split,
  work_on_goal 1 {intro x},
  dsimp at *, -- this causes the problem
  exact hU,
end

[Mario Carneiro]

This is a very weird bug. Calling (() <$ tactic.result), alone fixes the issue, so it's almost certainly a bug in the C++ code

[Mario Carneiro]

Oh, this is even more fun:

open tactic
example (P : set nat → Prop) (h : ∃ U : set nat, P U) : ∃ U : set nat, P U :=
begin
  cases h with U hU,
  split,
  work_on_goal 1 {intro x},
  dsimp at *, -- this causes the problem
  -- result, -- (1)
  exact hU,
  -- result, -- (2)
end

You get an error iff (2) is enabled and (1) is disabled