Zulip Chat Archive

Stream: general

Topic: Tactic to avoid `classical.some`


view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:16):

My goal was this:

⊢ comm_ring.zero (ring_completion (valuation_field (out (⟨⟨v, _⟩, _⟩.val)))) =
    domain.zero (ring_completion (valuation_field (out (⟨⟨v, _⟩, _⟩.val))))

and I tried dunfold out. This took me to the following slightly scary goal:

 comm_ring.zero (ring_completion (valuation_field (classical.some _))) =
    domain.zero (ring_completion (valuation_field (classical.some _)))

I don't like classical.somes in my term. They come with a corresponding very helpful classical.some_spec which is hard to keep track of if you have proof terms turned off. Was dunfold out an incorrect move? How can I get the correct some_specs into my context somehow?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:21):

what about generalize : (out (⟨⟨v, _⟩, _⟩.val)) = k?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:22):

A tactic like split_ifs for classical.some would be nice

view this post on Zulip Simon Hudon (Apr 21 2019 at 05:33):

I think you will find such a tactic here: https://github.com/unitb/lean-lib/blob/master/src/util/classical.lean

view this post on Zulip Simon Hudon (Apr 21 2019 at 05:50):

I can PR it tomorrow. Or if you need it urgently, feel free to take it

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 07:05):

I can't get it to work :-/

generalize tactic failed, result is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
state:
4 goals
A : Huber_pair,
v : ↥A → ↥A → Prop,
Γ : Type u_1,
_inst_2 : linear_ordered_comm_group Γ,
v₀ : valuation ↥A Γ,
h : ∀ (r s : ↥A), ⇑v₀ r ≤ ⇑v₀ s ↔ v r s,
h1 : is_continuous ⟨v, _⟩,
h2 : ∀ (r : ↥A), r ∈ (λ (A : Huber_pair), A.Rplus) A → ⇑⟨v, _⟩ r ≤ 1
⊢ comm_ring.zero (ring_completion (valuation_field (classical.some _))) =
    domain.zero (ring_completion (valuation_field (classical.some _)))

Should I be applying the tactic before or after the state looks like this? I just dunfolded something and they all appeared.


Last updated: May 15 2021 at 02:11 UTC