Eliminating cyclic equation

Stream: general

[Jannis Limperg]

Is there a tactic that can eliminate h in the following example?

example {n : ℕ} (h : n = nat.succ n) : false :=
begin
  cases h, -- fails
end

[Jason KY.]

I'm sure this should be in the library but library_search fails.
Anyway, I was able to prove it using induction:

example (n : ℕ) (h : n = nat.succ n) : false :=
begin
  induction n with k hk, linarith,
  apply hk, exact nat.succ_inj h
end

[Jannis Limperg]

Thanks. I should have mentioned this, but I'm looking for a tactic that will eliminate such 'cyclic' equations for any inductive type. There's a general principle behind this: x = C1 ... (C2 ... x ...) ..., where the Ci are constructors, is always false. I know how to write such a tactic (in principle); I'd just prefer not to. ;)

[Mario Carneiro]

I recall this coming up on the Isabelle list in the recent past. The suggested method, which would work here as well, is to prove that T.sizeof a < T.sizeof b if a is structurally contained in b, and deduce a != b

[Mario Carneiro]

For the special case of nat of course this isn't necessary, you can just apply ne_of_lt and apply lt_succ_self

[Mario Carneiro]

if you want something short and sweet that you can put in a tactic, it would be something like apply ne_of_sizeof_lt, simp_only [T.sizeof], linarith

[Jannis Limperg]

Ah, so we already have sizeof. Nice, the rest should be easy-ish. I'll put a tactic together.