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

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