Zulip Chat Archive

Stream: maths

Topic: leaking construction


view this post on Zulip Patrick Massot (Sep 09 2018 at 19:46):

Sometimes I see things like: quot.lift (λ (a₁ : cau_seq ℚ abs), quotient.lift (has_lt.lt a₁) _ ε) _ in my tactic state when playing with real numbers. It looks like internal details of the constructions are leaking. What does it mean? Can I avoid that?

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:52):

how are you "playing"?

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:52):

if you unfold stuff you can see this

view this post on Zulip Patrick Massot (Sep 09 2018 at 19:54):

More precisely, I have:

α : Type u_2,
_inst_1 : metric_space α,
β : Type u_3,
u : β  α,
f : filter β,
ε : ,
this : ball a ε  (map u f).sets

If I do have:= mem_map.2 this then the new this is the horror

quot.lift (λ (a₁ : cau_seq  abs), quotient.lift (has_lt.lt a₁) _ ε) _    (map (λ (y : α), dist y a) (map u f)).sets

but I can do instead have : {b | u b ∈ ball a ε} ∈ f.sets := mem_map.2 this, and Lean won't unfold it

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:57):

You are going the wrong way

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:57):

use mem_map.1 this

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:58):

(it works because the two sides are defeq so it doesn't really matter if you apply it, but then the matching goes crazy)

view this post on Zulip Patrick Massot (Sep 09 2018 at 19:58):

oh

view this post on Zulip Patrick Massot (Sep 09 2018 at 19:58):

weird

view this post on Zulip Patrick Massot (Sep 09 2018 at 19:59):

That's biconditional in action: try one direction at random and, if Lean is willing to apply it, never look back

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:59):

notice that you have another map in the result

view this post on Zulip Mario Carneiro (Sep 09 2018 at 19:59):

(map (λ (y : α), dist y a) (map u f)).sets

view this post on Zulip Patrick Massot (Sep 09 2018 at 19:59):

true

view this post on Zulip Mario Carneiro (Sep 09 2018 at 20:00):

so it tried to figure out how to read ball a ε as {x | m x ∈ t} for some m, t and chaos ensues

view this post on Zulip Patrick Massot (Sep 09 2018 at 20:01):

That's wonderful. In the proof I posted earlier:

example (u :   α) (a : α) : tendsto u at_top (nhds a) 
   ε > 0,  (N : ),  {n}, n  N  dist (u n) a < ε :=
⟨λ H ε εpos, mem_at_top_sets.1 $ mem_map.2 $ H (ball_mem_nhds _ εpos),
 λ H s s_nhd, let ε, εpos, sub := mem_nhds_iff_metric.1 s_nhd in
   let N, H' := H ε εpos in mem_at_top_sets.2 N, λ n nN,
   sub $ mem_ball.2 $ H' nN⟩⟩

There is a $ mem_map.2 $ . You can change 2 into 1, it still works. Then you can remove that bit entirely and it still works!

view this post on Zulip Mario Carneiro (Sep 09 2018 at 20:01):

because the proof is rfl

view this post on Zulip Patrick Massot (Sep 09 2018 at 20:01):

Yeah, I understand

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 02:08):

simp can do this:

lemma tendsto_at_top_nhds_metric [metric_space α] {f :   α} {a : α} :
  tendsto f at_top (nhds a)  (ε>0, N, nN, dist (f n) a < ε) :=
by simp [tendsto_infi, tendsto_principal, nhds_eq_metric]

The trick is to unfold nhds_eq_metric and rhen focus on the right side: An infimum is equal to a quantifier around the tendsto, until it reaches principal, then it is reduced to membership in at_top.
Other examples

lemma tendsto_at_top_at_top {f :   } :
  tendsto f at_top at_top  (M, N, nN, M  f n) :=
by conv { to_lhs, congr, skip, skip, rw [at_top] }; simp [tendsto_infi, tendsto_principal]

or

lemma tendsto_nhds_metric_nhds_metric [metric_space α] [metric_space β]
  {f : α  β} {a : α} {b : β}:
  tendsto f (nhds a) (nhds b)  (ε>0, δ>0, x, dist x a < δ  dist (f x) b < ε) :=
begin
  conv { to_lhs, congr, skip, skip, rw [nhds_eq_metric] },
  simp [tendsto_infi, tendsto_principal, mem_nhds_iff_metric, set.subset_def]
end

Here the annoying part is that we need to focus on the right nhds or at_top.


Last updated: May 14 2021 at 20:13 UTC