Propagate Tags

Stream: mathlib4

[Ian Benway]

I've been working on writing propagate_tags when I've had time over the last week. I think I've written a pretty faithful translation, but I didn't realize until testing that there are some relevant differences between 3 and 4. For example

--Lean 3
example : ∀(x : ℕ), x ≥ 0 ∧ x + 1 ≥ 0 :=
begin
  intro a,
  induction' a,
  apply and.intro,
  /-
  ⊢ 0 ≥ 0
  ⊢ 0 + 1 ≥ 0
  case nat.succ
  a: ℕ
  ih: a ≥ 0 ∧ a + 1 ≥ 0
  ⊢ a.succ ≥ 0 ∧ a.succ + 1 ≥ 0
  -/
  case nat.zero {
    --no tag found
  }
end

and

--Lean 4
example : ∀(x : Nat), x ≥ 0 ∧ x + 1 ≥ 0 := by
  intro a
  induction a
  apply And.intro
  /-
  case zero.left
  ⊢ Nat.zero ≥ 0

  case zero.right
  ⊢ Nat.zero + 1 ≥ 0

  case succ
  n✝ : Nat
  n_ih✝ : n✝ ≥ 0 ∧ n✝ + 1 ≥ 0
  ⊢ Nat.succ n✝ ≥ 0 ∧ Nat.succ n✝ + 1 ≥ 0
  -/
  case zero.right => {
    simp
  }
  case zero.left => {
    simp
  }
  case succ => {
    sorry
  }

So in Lean 3, apply doesn't immediately propagate the tags, but in Lean 4 it seems like it does(?). And so I can do propagate_tags {apply and.intro} in Lean 3 to get the nat.zero case. But then what's the intended use in Lean 4?

[Mario Carneiro]

why would you need to use propagate_tags apply e in lean 4 if it's already propagating tags?

[Mario Carneiro]

lean 4 is generally a lot better at propagating tags for everything since they were built in from the start

[Ian Benway]

Oh right—so are there any simple examples of when propagate_tags can be used in Lean 4? I'm looking for tests, and the examples I'm getting from Lean 3 are deep in more complicated tactics

[Mario Carneiro]

this seems like a pretty clear (lean 3) example:

example (h : nat → nat → nat) : nat := begin
  cases tt,
  -- case bool.ff
  -- h: ℕ → ℕ → ℕ
  -- ⊢ ℕ
  -- case bool.tt
  -- h: ℕ → ℕ → ℕ
  -- ⊢ ℕ
  propagate_tags { apply h },
  -- case bool.ff
  -- h: ℕ → ℕ → ℕ
  -- ⊢ ℕ
  -- h: ℕ → ℕ → ℕ
  -- ⊢ ℕ
  -- case bool.tt
  -- h: ℕ → ℕ → ℕ
  -- ⊢ ℕ
end

[Mario Carneiro]

I'm not sure it's a particularly useful behavior, but what it is doing is copying the tag from the main goal to the first subgoal generated after focusing on the main goal, if it is not already labeled

[Mario Carneiro]

you will need to use a different tactic to generate unlabeled goals in lean 4

[Mario Carneiro]

I wasn't able to find any tactics that don't preserve or create tags, but you can make one pretty easily, and use it to test propagate_tags:

import Lean
open Lean Meta Elab Tactic

elab "retag" x:(ident <|> "_") : tactic => liftMetaTactic1 fun g => do
  let g2 ← mkFreshExprMVar (← getMVarType g) (userName := x.getId)
  assignExprMVar g g2
  pure g2.mvarId!

example (h : Nat → Nat → Nat) : Nat := by
  cases true
  propagate_tags
    apply h; retag _; rotate_left; retag _; rotate_right

[Mario Carneiro]

I probably should have marked propagate_tags as /- S -/ since the need for it is drastically reduced in lean 4

[Ian Benway]

Ooo yes, this is exactly the kind of testing tactic I needed, thank you! I think I have a working version: mathlib4#258 . I'm not sure if it needs more tests, though