Injection failing

Stream: new members

[Marcus Rossel]

I can't finish this trivial goal:

l r : ℕ,
h : ∃ (m : ℕ × ℕ), true,
h' : (l, r) = classical.some h
⊢ l = (classical.some h).fst

MWE:

example (l r : ℕ) (h : ∃ m : ℕ × ℕ, true) (h' : (l, r) = classical.some h) : l = (classical.some h).fst :=
begin
  injection h', -- error
end

The injection tactic doesn't work here, but I don't know how else to solve this.

[Kevin Buzzard]

Does rw \l h', refl work?

[Marcus Rossel]

Yeah that works. Unfortunately in my real-world scenario the goal state doesn't show classical.some h (for some h), but instead classical.some _. I think this is messing with the rewriting somehow, so it doesn't work there.

[Yakov Pechersky]

Can you share the larger state? It is 'messing' with the rewrite because your proof might contain the term you're rewriting also.

[Yakov Pechersky]

Like Eric said in another thread, if you really need to work with such a state, the generalize family of tactics helps. But I think trying to work with classical.some values is an antipattern, you probably care more about the spec that the value

[Marcus Rossel]

Here's an example where the goal state shows classical.some _ instead of classical.some h:

lemma some_lemma (s : set ℕ) (h : true) : ∃ r, s = {r} := sorry

noncomputable def some_element (s : set ℕ) (h : true) : ℕ :=
  classical.some (some_lemma s h)

example {s : set ℕ} (h : true) : some_element s h = 0 :=
begin
  unfold some_element,
  -- ...
end

(The lemmas/definitions here are not intended to make any sense.)

[Yakov Pechersky]

import tactic.basic
import data.set.basic

lemma some_lemma (s : set ℕ) (h : true) : ∃ r, s = {r} := sorry

noncomputable def some_element (s : set ℕ) (h : true) : ℕ :=
  classical.some (some_lemma s h)

lemma some_element_spec (s : set ℕ) (h : true) :
  s = {some_element s h} :=
classical.some_spec (some_lemma s h)

example {s : set ℕ} (h : true) : some_element s h = 0 :=
begin
  rw ←set.singleton_eq_singleton_iff,
  rw ←some_element_spec s h,
  sorry
end

[Yakov Pechersky]

Inlined:

import tactic.basic
import data.set.basic

lemma some_lemma (s : set ℕ) (h : true) : ∃ r, s = {r} := sorry

noncomputable def some_element (s : set ℕ) (h : true) : ℕ :=
  classical.some (some_lemma s h)

example {s : set ℕ} (h : true) : some_element s h = 0 :=
begin
  rw ←set.singleton_eq_singleton_iff,
  rw some_element,
  generalize_proofs h',
  rw ←classical.some_spec h',
  sorry
end

[Marcus Rossel]

Thanks! generalize_proofs was what I needed :)

[Kyle Miller]

Marcus Rossel said:

Yeah that works. Unfortunately in my real-world scenario the goal state doesn't show classical.some h (for some h), but instead classical.some _. I think this is messing with the rewriting somehow, so it doesn't work there.

Lean by default doesn't pretty print proof terms, and instead it writes them as _. Put this at the top level to override this behavior:
set_option pp.proofs true