weird tactic bug

Stream: mathlib4

[Yuyang Zhao]

import Mathlib.Tactic.Tauto

open Classical in
lemma foo (hp : p) (hq : q) : (if p ∧ q then 1 else 0) = 1 := by
  by_cases h : p ∧ q <;> simp only [if_pos h]
  simp only at h -- do nothing (?)
  tauto -- fails if no previous line

[Kyle Miller]

Even set_option pp.all true shows that nothing is changing. Here's the goal state before and after the simp

p q : Prop
hp : p
hq : q
h : Not (And p q)
⊢ @Eq.{1} Nat
  (@ite.{1} Nat (And p q) (@instDecidableAnd p q (Classical.propDecidable p) (Classical.propDecidable q))
    (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
  (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))

[Yakov Pechersky]

Could simp only at h be clearing away some sort of .mdata?

[Kyle Miller]

No mdata, but it is instantiating a metavariable:

import Mathlib.Tactic.Tauto

open Lean Elab.Tactic
elab "print_term" t:term : tactic => withMainContext do
  let t := (← elabTerm t none)
  let ty := (← Meta.inferType t)
  Lean.logInfo s!"{t} : {ty}"

open Classical in
lemma foo (hp : p) (hq : q) : (if p ∧ q then 1 else 0) = 1 := by
  by_cases h : p ∧ q <;> simp only [if_pos h]
  print_term h -- _uniq.2545 : ?_uniq.2544
  simp only at h
  print_term h -- _uniq.2545 : Not (And _uniq.2515 _uniq.2516)
  tauto

[Thomas Murrills]

Metaprogramming consists of only three tasks:

1. remembering withMainContext
2. remembering whnf
3. remembering instantiateMVars

[Scott Morrison]

So this is bug with tauto not calling instantiateMVars somewhere? Do we know where / have a fix?

[Kyle Miller]

I'm working on it

[Mario Carneiro]

Thomas Murrills said:

Metaprogramming consists of only three tasks:

1. remembering withMainContext
2. remembering whnf
3. remembering instantiateMVars

Based on prior evidence I would say that metaprogramming seems to consist of:

1. forgetting withMainContext and bugfixing it later
2. forgetting whnf and bugfixing it later
3. forgetting instantiateMVars and bugfixing it later

[Heather Macbeth]

I prefer to think of them as the three patron saints of metaprogramming https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20error.20in.20structured.20proof/near/322950305

[David Renshaw]

I think in the successful case, this happens:

1. distrib_not_once_at rewrites h with Decidable.not_and'
2. casesMatching splits the resulting Or.
3. solve_by_elim closes both the resulting branches

[David Renshaw]

And in the unsuccessful case, (1) does not happen for some reason

[Kyle Miller]

I've done my genuflection to two of the three patron saints. #5565

[Kyle Miller]

Never mind, it was just to one of them. It turned out the problem was entirely that the Prop check was using docs4#Lean.Expr.isProp rather than docs4#Lean.Meta.isProp and the latter knows about instantiating metavariables. (These function names are a little confusing in relation to each other: Expr.isProp e is whether the expression e is literally Sort 0, and Meta.isProp e is whether e : Sort 0 is true.)

[Kyle Miller]

I didn't realize that Qq match expressions already do their matching up to reducible defeq, if I understand it correctly, so there's no need to do things like whnfR or cleanupAnnotations when using them.

[Sebastian Ullrich]

Yes, this is not documented in the quote4 readme, so I can never remember whether I should recommend it to people facing these issues