# Zulip Chat Archive

## 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
(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 (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,
contradiction,
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