(list.cons a l) ≠ l

Stream: Is there code for X?

[Eric Wieser]

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]

Does simp work for ≠? I've only seen it for = and <->

[Mario Carneiro]

no

[Mario Carneiro]

however you can mark any theorem T as a simp lemma and it will treat it as a proof of T = true

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

unless this exact lemma already exists with @[simp]

[Eric Wieser]

I was expecting that this lemma might already exist.

[Utensil Song]

This doesn't feel simp. But I did try other automatic tactics and none kills it in one line.

[Mario Carneiro]

@[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]

Can list.no_confusion be used here?

[Ruben Van de Velde]

I don't think so - l could be a list.cons

[Eric Wieser]

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]

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]

maybe try not using example?

[Gabriel Ebner]

Wow, I never realized you could have recursive examples.

[Utensil Song]

Oh then Lean demands a using_well_founded.

[Eric Wieser]

Pr'd as #3584

[Utensil Song]

/-
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]

Why would this lead to 0 < 0?

[Reid Barton]

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]

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

[Mario Carneiro]

try simp [cons_ne_self h t]

[Utensil Song]

Beautiful, it works!

(Lean is right to complain, without the proper hint (i.e. h t), this is really not "decreasing")

[Eric Wieser]

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]

list and nat are two faces of the same coin

[Utensil Song]

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

[Mario Carneiro]

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

[Eric Wieser]

Turns out I'm wrong anyway, list.length is defined within lean itself, not within mathlib where our lemmas are

[Utensil Song]

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

[Utensil Song]

Not so sure in the library itself though

[Mario Carneiro]

In isolation, sure

[Mario Carneiro]

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

[Eric Wieser]

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