# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: (list.cons a l) ≠ l

#### Eric Wieser (Jul 27 2020 at 11:57):

The statement appears trivial, but I was surprised that `simp`

couldn't solve it for me

```
@[simp] lemma cons_ne_self {α : Type u} (a : α) (l : list α) : (list.cons a l) ≠ l := begin
induction l,
{ simp },
simp only [not_and, ne.def],
rintro ⟨⟩,
exact l_ih,
end
```

Does this belong in mathlib, or is it too trivial? I note that `nat.succ_ne_self`

exists, but isn't tagged as `@[simp]`

...

#### Chris Wong (Jul 27 2020 at 12:56):

Does `simp`

work for ≠? I've only seen it for `=`

and `<->`

#### Mario Carneiro (Jul 27 2020 at 12:58):

no

#### Mario Carneiro (Jul 27 2020 at 12:58):

however you can mark any theorem `T`

as a simp lemma and it will treat it as a proof of `T = true`

#### Eric Wieser (Jul 27 2020 at 13:01):

Does that mean that almost all non-equality / iff lemmas with no implications should be marked simp?

#### Mario Carneiro (Jul 27 2020 at 13:02):

almost all lemmas *could* be marked simp, that doesn't make it a good idea

#### Mario Carneiro (Jul 27 2020 at 13:03):

In this case, I'm not sure why you thought simp would solve the theorem

#### Mario Carneiro (Jul 27 2020 at 13:03):

unless this exact lemma already exists with `@[simp]`

#### Eric Wieser (Jul 27 2020 at 13:04):

I was expecting that this lemma might already exist.

#### Utensil Song (Jul 27 2020 at 13:07):

This doesn't feel `simp`

. But I did try other automatic tactics and none kills it in one line.

#### Mario Carneiro (Jul 27 2020 at 13:25):

```
@[simp] lemma cons_ne_self {α} (a : α) (l : list α) : list.cons a l ≠ l :=
mt (congr_arg list.length) $ ne_of_gt $ nat.lt_succ_self _
```

#### Eric Wieser (Jul 27 2020 at 13:34):

Can `list.no_confusion`

be used here?

#### Ruben Van de Velde (Jul 27 2020 at 13:38):

I don't think so - `l`

could be a `list.cons`

#### Eric Wieser (Jul 27 2020 at 13:58):

Can also get it with

```
@[simp] theorem cons_ne_self {α : Type u} : ∀ (a : α) (l : list α), (a :: l) ≠ l
| a nil := list.cons_ne_nil a list.nil
| a (h :: t) := λ hyp, cons_ne_self h t $ (cons.inj hyp).right
```

which doesn't rely on `list.length`

#### Utensil Song (Jul 27 2020 at 14:06):

```
import tactic
universe u
open list
example {α : Type u} : ∀ (a : α) (l : list α), (cons a l) ≠ l
| a nil := by simp
| a (cons h t) := begin
solve_by_elim,
end
```

Weird, this closes the goals but

```
equation compiler failed to create auxiliary declaration '_example._main._pack.equations._eqn_2'
nested exception message:
invalid equation lemma, unexpected form
```

#### Reid Barton (Jul 27 2020 at 14:06):

maybe try not using `example`

?

#### Gabriel Ebner (Jul 27 2020 at 14:08):

Wow, I never realized you could have recursive examples.

#### Utensil Song (Jul 27 2020 at 14:12):

Oh then Lean demands a `using_well_founded`

.

#### Eric Wieser (Jul 27 2020 at 14:18):

Pr'd as #3584

#### Utensil Song (Jul 27 2020 at 14:34):

```
/-
failed to prove recursive application is decreasing, well founded relation
@has_well_founded.r (Σ' (a : α), list α)
(@psigma.has_well_founded α (λ (a : α), list α) (@has_well_founded_of_has_sizeof α (default_has_sizeof α))
(λ (a : α), @has_well_founded_of_has_sizeof (list α) (@list.has_sizeof α (default_has_sizeof α))))
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
invalid apply tactic, failed to unify
0 < 0
with
?m_1 < ?m_1 + ?m_2
state:
α : Type u,
cons_ne_self : ∀ (_p : Σ' (a : α), list α), _p.fst :: _p.snd ≠ _p.snd,
a h : α,
t : list α,
a : α,
l : list α
⊢ 0 < 0
-/
lemma cons_ne_self {α : Type u} : ∀ (a : α) (l : list α), (cons a l) ≠ l
| a nil := by simp
| a (cons h t) := by simp [cons_ne_self]
using_well_founded {
dec_tac := well_founded_tactics.default_dec_tac
}
```

#### Utensil Song (Jul 27 2020 at 14:34):

Why would this lead to `0 < 0`

?

#### Reid Barton (Jul 27 2020 at 14:37):

`simp`

probably just used the lemma to prove itself directly, and then obviously wasn't able to prove that the call was on something smaller

#### Reid Barton (Jul 27 2020 at 14:37):

This is a common annoyance when using "apply anything" tactics in conjunction with the equation compiler.

#### Mario Carneiro (Jul 27 2020 at 14:39):

try `simp [cons_ne_self h t]`

#### Utensil Song (Jul 27 2020 at 14:43):

Beautiful, it works!

(Lean is right to complain, without the proper hint (i.e. `h t`

), this is really not "decreasing")

#### Eric Wieser (Jul 27 2020 at 15:13):

Mario Carneiro said:

`@[simp] lemma cons_ne_self {α} (a : α) (l : list α) : list.cons a l ≠ l := mt (congr_arg list.length) $ ne_of_gt $ nat.lt_succ_self _`

```
@[simp] lemma cons_ne_self {α} (a : α) (l : list α) : list.cons a l ≠ l :=
mt (congr_arg list.length) (nat.succ_ne_self _)
```

is better than that proof, if we really want the proof to depend on `list.length`

#### Utensil Song (Jul 27 2020 at 15:19):

list and nat are two faces of the same coin

#### Utensil Song (Jul 27 2020 at 15:19):

such a basic theorem probably should not depend on length or nat

#### Mario Carneiro (Jul 27 2020 at 15:20):

I don't see why, this is what libraries are for - you don't have to prove everything from the axioms

#### Eric Wieser (Jul 27 2020 at 15:22):

Turns out I'm wrong anyway, `list.length`

is defined within `lean`

itself, not within mathlib where our lemmas are

#### Utensil Song (Jul 27 2020 at 15:22):

I like the proof in another context because it's the most intuitive proof for me.

#### Utensil Song (Jul 27 2020 at 15:23):

Not so sure in the library itself though

#### Mario Carneiro (Jul 27 2020 at 15:23):

In isolation, sure

#### Mario Carneiro (Jul 27 2020 at 15:24):

but when it comes to minimizing the sum of the sizes of all proofs through reordering, this looks like an improvement

#### Eric Wieser (Jul 27 2020 at 19:11):

Note my claim about reordering in the PR was actually wrong anyway.

Last updated: May 17 2021 at 14:12 UTC