Using noConfusion in apply

Stream: lean4

[Leni Aniva]

Consider

example : ∀ (n: Nat), 0 = n + 1 → False := λ _ h => Nat.noConfusion h

if I were to write this in tactic form

example : ∀ (n: Nat), 0 = n + 1 → False := by
  intro n h
  apply Nat.noConfusion

The apply tactic fails since noConfusionType cannot be unified with False. Is there a way to invoke the Nat.noConfusion theorem without explicitly writing down Nat.noConfusion h like apply Nat.noConfusion h?

[Kyle Miller]

I doubt it. refine Nat.noConfusion ?_ doesn't work either.

The noConfusion mechanism really needs h to see if it's type correct.

[Kyle Miller]

If you want to play around with this, here's a simplified version of Nat.noConfusion:

def Nat.noConfusionType'.{u} (P : Sort u) (a b : Nat) : Sort u :=
  Nat.casesOn a
    (zero := Nat.casesOn b (P → P) (fun _ => P))
    (succ := fun _ => Nat.casesOn b P (fun _ => P → P))

def Nat.noConfusion'.{u} {P : Sort u} {a b : Nat} (h : a = b) : Nat.noConfusionType' P a b :=
  Eq.recOn h (Nat.casesOn a (zero := id) (succ := fun _ => id))

example : ∀ (n : Nat), 0 = n + 1 → False := by
  intro n h
  exact Nat.noConfusion' h

[Tom Kranz]

If you really want to avoid passing the witness for 0 = n + 1 in the tactic application, you can just leave it in the goal and it'll fall into place:

example : ∀ (n: Nat), 0 = n + 1 → False := by
  intro n
  exact Nat.noConfusion

Although this is of course not exactly what you wrote in term form, it is just an η-reduction away from the original:

example : ∀ (n: Nat), 0 = n + 1 → False := λ _ => Nat.noConfusion

[François G. Dorais]

The contradiction tactic will do it:

example : ∀ (n: Nat), 0 = n + 1 → False := by
  intros; contradiction

[Alexandre Rademaker]

Following up on this thread...

image.png

The complete proof I was looking for uses the noConfusion.

example {α : Type} (a : α)
  : ∀ (t₁ t₂ : Tree α), Tree.nil = Tree.node a t₁ t₂ → False :=
  λ _ _ h => Tree.noConfusion h

Why does noConfusion not show up in the autocomplete?

[Kyle Miller]

There are higher-level interfaces to this, e.g.

example : ∀ (n: Nat), 0 = n + 1 → False := nofun

Using nofun is fun but with zero match alternatives. It's the same as

example : ∀ (n: Nat), 0 = n + 1 → False := fun n h => nomatch h