proving (succ n) != n

Stream: general

[Hunter Freyer]

What tactic can I use to prove that inductive structures can't contain themselves?

[Yakov Pechersky]

You might like to read https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Simon Hudon]

I don't think that's going to be enough. You need induction to prove that. There's no automation specifically for that but it could be done.

[Hunter Freyer]

any ideas on the general approach?

[Hunter Freyer]

oh, I guess I can just do induction like you said. Rather tedious.

[Mario Carneiro]

You can use the autogenerated sizeof function to prove this kind of thing in many cases

[Mario Carneiro]

import tactic.linarith

inductive T
| leaf : ℕ → T
| node : T → T → T

theorem T_ne_left (x y) : T.node x y ≠ x :=
mt (congr_arg T.sizeof) $ ne_of_gt $
by rw [T.sizeof]; show sizeof x < _; linarith

[Yakov Pechersky]

inductive my_int
| zero : my_int
| succ : my_int → my_int
| pred : my_int → my_int

lemma pred_succ_eq {n : my_int} : n.pred.succ = n.succ.pred :=
begin
  sorry
end

example {n : my_int} : n ≠ n.succ :=
begin
  refine my_int.rec_on n _ _ _,
  { intro h, exact my_int.no_confusion h },
  { intros k h H, exact h (my_int.succ.inj H) },
  { intros k h H,
    rw pred_succ_eq at H,
    exact h (my_int.pred.inj H) }
end

[Jannis Limperg]

I have a tactic lying around that automates Mario's approach. Will get PR'd at some point. cases could also be extended to solve this sort of goal.