Stream: new members

Topic: Contradiction fails when context contains proof of false

Josiah Eldon Bills (Oct 04 2022 at 04:59):

I am working on a fairly complex proof where in part of the proof I get a contradiction by simplifying using x=a at a hypothesis not (a = x), thus yielding a term of type false. Normally I can just close the current goal with contradiction, but in this case I get an error. Below you can see my context, my goal, and the (quite unhelpful) error I get:

contradiction tactic failed
state:
4 goals
case or.inl
α : Type u_1,
_inst_1 : decidable_eq α,
a : α,
this : ∀ (l : list (list α)), l.length > 1 → [a].intercalate [l.head, [a].intercalate l.tail] = [a].intercalate l,
hd : α,
tl : list α,
ih :
∀ (l : list α),
a ∈ l → (let s : list α × list α := list.split_on_first a l in l = tl → (list.split_on a tl).length > 1),
l : list α,
s : list α × list α := list.split_on_first a l,
h : l = hd :: tl,
list_contains : a ∈ hd :: tl,
or : a = hd,
h_1 : false
⊢ (let or : a = hd ∨ a ∈ tl := list.eq_or_mem_of_mem_cons list_contains in a ∈ tl) (_root_.or.inl or)


I can post the full context if need be, but it is quite long.

Damiano Testa (Oct 04 2022 at 05:12):

Does exact h_1.elim work at that point?

Damiano Testa (Oct 04 2022 at 05:14):

(At least for me, a #mwe, even if not too minimized), would be helpful.)

Josiah Eldon Bills (Oct 04 2022 at 05:18):

I get the following error when I try that. Similarly, if I try to use exact absurd:

infer type failed, function expected at
(let or : a = hd ∨ a ∈ tl := list.eq_or_mem_of_mem_cons list_contains in a ∈ tl) (or.inl hypothesis)
term
let or : a = hd ∨ a ∈ tl := _
in a ∈ tl
has type
Prop


Damiano Testa (Oct 04 2022 at 05:21):

and also refine false.elim _,  gives an error?

Damiano Testa (Oct 04 2022 at 05:21):

or apply false.elim,?

Josiah Eldon Bills (Oct 04 2022 at 05:23):

The former gives

infer type failed, function expected at
(let or : a = hd ∨ a ∈ tl := list.eq_or_mem_of_mem_cons list_contains in a ∈ tl) (or.inl hypothesis)
term
let or : a = hd ∨ a ∈ tl := _
in a ∈ tl
has type
Prop


again, while the latter gives

invalid apply tactic, failed to unify
(let or : a = hd ∨ a ∈ tl := list.eq_or_mem_of_mem_cons list_contains in a ∈ tl) (or.inl hypothesis)
with
?m_1


Josiah Eldon Bills (Oct 04 2022 at 05:25):

Here is the theorem:

def list.split_on_first {α: Type*} [decidable_eq α] (a: α) (l: list α) : list α × list α :=
let s := l.split_on a in

theorem list.split_on_first.infix {α: Type*} [decidable_eq α] (a: α) (l: list α) : a ∈ l → let s := list.split_on_first a l in l = s.1 ++ [a] ++ s.2 :=
begin
intros list_contains s,
suffices : [a].intercalate [s.1, s.2] = l,
{
let intercalate_append : [a].intercalate [s.1, s.2] = s.1 ++ [a] ++ s.2 := by simp [list.intercalate],
rw ←intercalate_append,
symmetry,
exact this,
},
suffices : ∀l: list (list α), l.length > 1 → [a].intercalate [l.head, [a].intercalate l.tail] = [a].intercalate l,
{
suffices split_len : (list.split_on a l).length > 1,
{
specialize this (list.split_on a l) split_len,
rw list.intercalate_split_on l a at this,
exact this
},

induction h: l generalizing l,
simp [h] at list_contains,
simp only [list.split_on, list.split_on_p_cons],
split_ifs,
{
simp [list.split_on_p_ne_nil],
cases th: list.split_on_p (λ (_x : α), _x = a) tl,
simp [list.split_on_p_ne_nil] at th,
simp [th]
},
rw h at list_contains,
let : a ∈ tl,
{
let or := list.eq_or_mem_of_mem_cons list_contains,
cases or with hypothesis,
simp [hypothesis] at h_1,
exact h_2,
},
let induction := ih tl this (eq.refl _),
rw ←list.split_on,
cases (list.split_on a tl),
simp at induction,
simp at induction,
simp [induction],
},
intros lol lol_size_2,
cases lol,
simp at lol_size_2,
cases lol_tl,
simp at lol_size_2,
simp [list.intercalate],
end


The error occurs in the proof of let : a ∈ tl,.

Josiah Eldon Bills (Oct 04 2022 at 05:27):

I found that if you use cases dont_care: or with hypothesis, then this works just fine.

Josiah Eldon Bills (Oct 04 2022 at 05:28):

If you do this then the goal remains a ∈ tl, while if you don't then the goal gets a whole bunch of garbage thrown in it.

Damiano Testa (Oct 04 2022 at 05:29):

what happens if you type intros first?

Damiano Testa (Oct 04 2022 at 05:32):

This works:

    {
have or := list.eq_or_mem_of_mem_cons list_contains,
cases or with hypothesis,
simp [hypothesis] at h_1,
exact or,
},


I used have instead of let.

Damiano Testa (Oct 04 2022 at 05:33):

Even though this does not seem to be causing problems, I am very skeptical about calling a variable with the name of an existing function such as or...

Damiano Testa (Oct 04 2022 at 05:35):

Briefly, let is for introducing "shorthand" notation for something, while have is for introducing extra hypotheses. In your situation, I think that you used let to mean "let us call or the hypothesis a = hd ∨ a ∈ tl". In Lean, this is done by using have, not let.

Josiah Eldon Bills (Oct 04 2022 at 05:37):

The name point is well made, I will change it. It isn't the cause of the issue though. Why does this bubble down to cause issues in cases?

Damiano Testa (Oct 04 2022 at 05:48):

I do not know, but the cases on the let mangles the type of the target. I am actually not sure about what the precise effect is, but Lean is not very happy with it either.

Damiano Testa (Oct 04 2022 at 06:37):

When you use let you are informing Lean that you will use or to mean whatever you say it is. At this stage, I suspect that lean thinks that or is the Prop that it displays, not its proof.

I imagine that, to Lean, what you wrote was not very different than let or := A ∨ B, with A B : Prop completely arbitrary, with no indication that actually at least one of them is true.

Kevin Buzzard (Oct 04 2022 at 07:36):

let changes the goal. It's not the correct tactic to use when defining a proof, have is.

Damiano Testa (Oct 04 2022 at 07:45):

Indeed, here is a smaller version of the same issue as above:

import logic.basic

example {p : Prop} : true :=
begin
let or1 : p ∨ ¬ p := em p,
cases or1,
trivial,  -- fails
end


Last updated: Dec 20 2023 at 11:08 UTC