Zulip Chat Archive

Stream: Is there code for X?

Topic: (list.cons a l) ≠ l


view this post on Zulip 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]...

view this post on Zulip Chris Wong (Jul 27 2020 at 12:56):

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

view this post on Zulip Mario Carneiro (Jul 27 2020 at 12:58):

no

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:02):

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

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:03):

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

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:03):

unless this exact lemma already exists with @[simp]

view this post on Zulip Eric Wieser (Jul 27 2020 at 13:04):

I was expecting that this lemma might already exist.

view this post on Zulip 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.

view this post on Zulip 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 _

view this post on Zulip Eric Wieser (Jul 27 2020 at 13:34):

Can list.no_confusion be used here?

view this post on Zulip Ruben Van de Velde (Jul 27 2020 at 13:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 27 2020 at 14:06):

maybe try not using example?

view this post on Zulip Gabriel Ebner (Jul 27 2020 at 14:08):

Wow, I never realized you could have recursive examples.

view this post on Zulip Utensil Song (Jul 27 2020 at 14:12):

Oh then Lean demands a using_well_founded.

view this post on Zulip Eric Wieser (Jul 27 2020 at 14:18):

Pr'd as #3584

view this post on Zulip 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
}

view this post on Zulip Utensil Song (Jul 27 2020 at 14:34):

Why would this lead to 0 < 0?

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 27 2020 at 14:37):

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

view this post on Zulip Mario Carneiro (Jul 27 2020 at 14:39):

try simp [cons_ne_self h t]

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 27 2020 at 15:19):

list and nat are two faces of the same coin

view this post on Zulip Utensil Song (Jul 27 2020 at 15:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Utensil Song (Jul 27 2020 at 15:22):

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

view this post on Zulip Utensil Song (Jul 27 2020 at 15:23):

Not so sure in the library itself though

view this post on Zulip Mario Carneiro (Jul 27 2020 at 15:23):

In isolation, sure

view this post on Zulip 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

view this post on Zulip 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