Stream: general

Topic: Eliminating cyclic equation

Jannis Limperg (May 29 2020 at 16:44):

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. (May 29 2020 at 17:02):

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 (May 29 2020 at 17:12):

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 (May 29 2020 at 22:08):

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 (May 29 2020 at 22:09):

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 (May 29 2020 at 22:11):

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 (Jun 01 2020 at 16:13):

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

Last updated: May 18 2021 at 17:44 UTC