rw for inequalities

Stream: metaprogramming / tactics

[Robert Maxton]

It'd be cool to have a 'rw' for inequalities. Say we have a goal a ≤ b and a hypothesis h : c ≤ d. The minimal useful product would basically be a macro that tries to unify a with c and b with d, and then chooses between refine le_trans h ?_, refine le_trans ?_ h, and refine h depending on the results.

[Robert Maxton]

In fact I've written that much already:

import Mathlib.Tactic.Basic
import Mathlib.Tactic.SimpRw
import Mathlib.Order.Defs.PartialOrder
import Batteries.Lean.Expr
import Qq

#check Lean.Elab.Tactic.withRWRulesSeq

namespace Mathlib.Tactic

open Lean Elab Meta Tactic Qq
open Parser.Tactic (optConfig rwRuleSeq location getConfigItems)

#check 1 ≤ 2

def relRewriteTarget (stx : Syntax) : TacticM Unit := do
  Term.withSynthesize <| withMainContext do
    let goal ← getMainGoal
    let ⟨1, ~q(Prop), ~q(@LE.le $α $inst $lhs $rhs)⟩ ← inferTypeQ (← goal.getType)
      | throwAbortTactic
    let e ← elabTerm stx none true
    if e.hasSyntheticSorry then
      throwAbortTactic
    -- let α ← Meta.inferType e
    forallTelescopeReducing (← Meta.inferType e) fun args body ↦ do
      let ⟨1, ~q(Prop), ~q(@LE.le «$α» «$inst» $h_lhs $h_rhs)⟩ ← inferTypeQ body | throwAbortTactic
      -- let stx ← lambdaTelescope
      if ← isDefEq h_lhs lhs then
        if ← isDefEq h_rhs rhs then
          evalTactic (← `(tactic| refine $(⟨stx⟩)))
        else
          evalTactic (← `(tactic| refine le_trans $(⟨stx⟩) ?_))
      else
        evalTactic (← `(tactic| refine le_trans ?_ $(⟨stx⟩)))
      -- if let ~q(@LE.le $α $inst $lhs $rhs) := body then _

elab s:"rel_rw" rws:rwRuleSeq g:(location)? : tactic => do
  withSimpRWRulesSeq s rws fun _ term => do
    let loc := expandOptLocation <| g.map (TSyntax.raw) |>.getD Syntax.missing
    withLocation loc
      (fun _ ↦ throwAbortTactic)
      (relRewriteTarget term)
      (throwTacticEx `rel_rw · "did not find instance of the pattern in the current goal")

example {α : Type*} [Preorder α] (a b c : α) (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := by
  rel_rw [h₁, h₂]

[Jovan Gerbscheid]

The more general concept is called generalized rewriting, which allows rewriting with inequalities, but also with e.g. equivalence relations. We've been wanting to have such a tactic for a long time, but looking at the PR it seems like we might get it soon: #8167

[Robert Maxton]

ooh, that would be nice

[Robert Maxton]

I cut myself off because I thought I might have found an answer to my question but apparently I might just get an entire tactic for it instead

[Robert Maxton]

Neat!

[Jovan Gerbscheid]

@Robert Maxton, thank you for reminding me about the need for this tactic. I've made an announcement at #mathlib4 > Announcement: New `grw` tactic that the tactic is now available in mathlib.