Clearing obvious contradictions in cases of goals

Stream: general

[l1mey]

For context, poison and bitvec are part of the inductive type iN, which is:

/--
LLVM-style integers with poison value.
-/
inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

I'm currently in the middle of a proof that has a couple obvious contradictions in the cases that simp hasn't cleaned out. Things like heq✝ : poison = bitvec b✝ and heq✝ : poison = bitvec a✝ in the first and second case should cause both of these cases to clear, but right now simp isn't doing much.

theorem comm_nsw {n} (x y : iN n)
    : x +nsw y <~> y +nsw x := by

  simp [iN_unwrap_poison]
  repeat' split; <;> try simp
  /-
  case h_3
  n : Nat
  x✝³ x✝² x✝¹ x✝ : iN n
  a✝ b✝ : BitVec n
  heq✝ : poison = bitvec b✝
  ⊢ poison <~> iN.addNswBV a✝ b✝

  case h_3
  n : Nat
  x✝⁴ x✝³ x✝² x✝¹ : iN n
  a✝ b✝ : BitVec n
  heq✝ : poison = bitvec a✝
  x✝ : bitvec b✝ = poison → False
  ⊢ poison <~> iN.addNswBV a✝ b✝

  case h_3
  n : Nat
  x✝¹ x✝ : iN n
  a✝ b✝ : BitVec n
  ⊢ iN.addNswBV a✝ b✝ <~> iN.addNswBV b✝ a✝
  -/

I've created this simp lemma and it didn't work, but I never expected it to:

@[simp]
theorem iN_contra {n} {a : BitVec n}
    {h : (poison : iN n) = (bitvec a : iN n)} : False := by

  cases h

[l1mey]

Using a custom tactic, I'm able to extract out the contradictions:

elab "clear_poison_eq" : tactic => do
  withMainContext do
    let goals ← getGoals
    goals.forM $ fun goal => do
      let ctx ← getLCtx
      ctx.forM (fun (decl : Lean.LocalDecl) => do
        -- local decl: name: heq._@.theorems.iN_normal.tilde._hyg.67
        -- expr: _uniq.1235
        -- type: Eq.{1} (iN _uniq.221) (iN.poison _uniq.221) (iN.bitvec _uniq.221 _uniq.1202)

        let declExpr := decl.toExpr
        let declType ← Lean.Meta.inferType declExpr
        let (fn, args) := declType.getAppFnArgs

        let isPoison (e : Expr) : Bool :=
          match e.getAppFn.constName? with
          | some nm => nm == ``iN.poison
          | none    => false

        match fn, args with
        | `Eq, #[_, lhs, rhs] =>

          if isPoison lhs || isPoison rhs then
            dbg_trace f!"clearing poison eq: {lhs} {rhs}"

            let idStx := mkIdent decl.userName
            let stx := mkNode ``Lean.Parser.Tactic.cases #[mkNullNode #[mkAtom "cases"], idStx]
            try Elab.Tactic.evalTactic stx catch _ => pure ()

        | _, _ => pure ()
      )

This has output:

clearing poison eq: iN.poison _uniq.221 iN.bitvec _uniq.221 _uniq.1202
clearing poison eq: iN.poison _uniq.221 iN.bitvec _uniq.221 _uniq.1202
clearing poison eq: iN.poison _uniq.221 iN.bitvec _uniq.221 _uniq.1202

But I can't seem to clear the goal using the cases? It prints without doing anything. Help would be very appreciated.

[Robin Arnez]

Hmm? simp_all should be able to handle this with reduceCtorEq:

/--
LLVM-style integers with poison value.
-/
inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

example (h : iN.poison = iN.bitvec b) : 1 = 2 := by
  simp only [reduceCtorEq] at h

[Robin Arnez]

But looking at your metaprogram:

1. Don't forget to use docs#Lean.MVarId.withContext​! So just use fun goal => goal.withContext do
2. The right syntax for cases is

let null := mkNullNode #[]
let elimTarget := mkNode `Lean.Parser.Tactic.elimTarget #[null, idStx]
let tactic : Syntax := mkNode `Lean.Parser.Tactic.cases #[mkAtom "cases", mkNullNode #[elimTarget], null, null]

I don't want you remember that though, just

let tactic ← `(tactic| cases $idStx:ident)

Also, many tactics can also be found as functions on MVarIds; so you can simply do goal.<tactic> sometimes. cases is one of them!

let #[] ← goal.cases decl.fvarId | throwError "could not solve goals with `cases`"

So here's a corrected version of your tactic:

import Lean

/--
LLVM-style integers with poison value.
-/
inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

open Lean Meta Elab Tactic

elab "clear_poison_eq" : tactic => do
  let goals ← getGoals
  goals.forM $ fun goal => goal.withContext do
    let ctx ← getLCtx
    for decl in ctx do
      let declType ← whnf decl.type

      let isPoison (e : Expr) : Bool :=
        match e.getAppFn.constName? with
        | some nm => nm == ``iN.poison
        | none    => false

      match_expr declType with
      | Eq _ lhs rhs =>
        if isPoison lhs || isPoison rhs then
          Lean.logInfo m!"clearing poison eq: {lhs} {rhs}"
          let #[] ← goal.cases decl.fvarId | throwError "could not solve goals with `cases`"
      | _ => pure ()

example (h : iN.poison = iN.bitvec 3#4) : Nat := by
  clear_poison_eq

[Aaron Liu]

Try using simp_all

[Aaron Liu]

or contradiction