Contradiction fails when context contains proof of false

Stream: new members

[Josiah Eldon Bills]

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]

Does exact h_1.elim work at that point?

[Damiano Testa]

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

[Josiah Eldon Bills]

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]

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

[Damiano Testa]

or apply false.elim,?

[Josiah Eldon Bills]

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]

Here is the theorem:

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

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,
    contradiction,
    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,
      contradiction,
      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,
      contradiction,
      exact h_2,
    },
    let induction := ih tl this (eq.refl _),
    rw ←list.split_on,
    cases (list.split_on a tl),
    simp at induction,
    contradiction,
    simp at induction,
    simp [induction],
  },
  intros lol lol_size_2,
  cases lol,
  simp at lol_size_2,
  contradiction,
  cases lol_tl,
  simp at lol_size_2,
  contradiction,
  simp [list.intercalate],
end

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

[Josiah Eldon Bills]

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

[Josiah Eldon Bills]

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]

what happens if you type intros first?

[Damiano Testa]

This works:

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

I used have instead of let.

[Damiano Testa]

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]

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]

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]

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]

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]

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

[Damiano Testa]

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