# Zulip Chat Archive

## 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