Zulip Chat Archive

Stream: new members

Topic: idioms : f p = f (p.fst, p.snd), etc.


view this post on Zulip Jean Lo (Aug 23 2020 at 13:03):

Today I encountered the surprising-but-not-really fact that the following proof is not refl:

variables (f : α × β → β) (p : α × β)

example : f p = f (p.fst, p.snd) := congr_arg _ $ prod.ext rfl rfl

This does not seem incredibly awful, but it also comes up often enough that I'm finding it hard to believe that I haven't overlooked a lemma/tactic somewhere that will take care of it. Have I? What is the right way to go about this?


More context, possibly distracting: I'm attempting to write down some things about dynamical systems as an exercise, and the f : α × β → β business comes from the following definition obtained by naïvely copying out of a book:

(to_fun   : ℝ × X → X)
(cont     : continuous to_fun)
(map_zero : ∀ x, to_fun (0, x) = x)
(map_add  : ∀ x t₁ t₂, to_fun (t₁ + t₂, x) = to_fun (t₂, to_fun (t₁, x)))

(It does not invoke the relatively-recent mathlib add_torsor in part because I think it would be desirable to ultimately have a version of this for local flows, and it stops being a group action. Then again I don't know what the definition for the local version should look like either — carry around a U : set ℝ × X on which the function is defined, and qualify all the other fields with ∀ (x, t) ∈ U? Make the signature X → ℝ →. X instead and wrangle a lot of roptions? A lot of this seems vaguely familiar from struggles with homotopies circa #1160, and I was hoping I could maybe get some insights as to what people have learnt since.)

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:11):

This issue is sadly well-known.

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:12):

@Jean Lo why not use R -> X -> X

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:12):

and I was writing what Kenny wrote.

view this post on Zulip Jean Lo (Aug 23 2020 at 13:13):

ℝ × X → X and continuous (uncurry to_fun) ?

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:14):

oh, continuity

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:14):

let's look at how topological_group does this then

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:16):

src/topology/algebra/group.lean L33

class topological_group (α : Type*) [topological_space α] [group α]
  extends has_continuous_mul α : Prop :=
(continuous_inv : continuous (λa:α, a⁻¹))

src/topology/algebra/monoid.lean L27

class has_continuous_mul (α : Type*) [topological_space α] [has_mul α] : Prop :=
(continuous_mul : continuous (λp:α×α, p.1 * p.2))

view this post on Zulip Jean Lo (Aug 23 2020 at 13:16):

oh gee

class has_continuous_add (α : Type*) [topological_space α] [has_add α] : Prop :=
(continuous_add : continuous (λp:α×α, p.1 + p.2))

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:16):

yay I'm still faster

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:18):

src/topology/algebra/module.lean L43

class topological_semimodule (R : Type u) (M : Type v)
  [semiring R] [topological_space R]
  [topological_space M] [add_comm_monoid M]
  [semimodule R M] : Prop :=
(continuous_smul : continuous (λp : R × M, p.1  p.2))

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:18):

I think you need topological_mul_action

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:18):

that is topological_semimodule restricted to mul_action

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:18):

You could use has_uncurry here, but I think the PR got lost somehow.

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:19):

https://github.com/leanprover-community/mathlib/pull/3694

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:26):

It got stuck with Mario requiring mysterious priorities to be set (at don't know where or to what values), but you can still use it:

import topology.instances.real

section uncurry

variables {α β γ δ : Type*}

/-- Records a way to turn an element of `α` into a function from `β` to `γ`. -/
class has_uncurry (α : Type*) (β : out_param Type*) (γ : out_param Type*) := (uncurry : α  (β  γ))

notation ``:max x:max := has_uncurry.uncurry x

instance has_uncurry_base : has_uncurry (α  β) α β := id

instance has_uncurry_induction [has_uncurry β γ δ] : has_uncurry (α  β) (α × γ) δ :=
⟨λ f p, (f p.1) p.2

end uncurry

structure flow (X : Type*) [topological_space X] :=
(to_fun   :   X  X)
(cont     : continuous to_fun)
(map_zero :  x, to_fun 0 x = x)
(map_add  :  x t₁ t₂, to_fun (t₁ + t₂) x = to_fun t₂ (to_fun t₁ x))

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:30):

And now let's play with has_uncurry's real magic: how do you talk about a continuous family of flows of X parametrized by a topological space Y?

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:30):

variables {X Y : Type*} [topological_space X] [topological_space Y]

instance has_uncurry_flow : has_uncurry (flow X) ( × X) X := ⟨λ f p, f.to_fun p.1 p.2

variable (f : Y  flow X)

#check continuous f

view this post on Zulip Patrick Massot (Aug 23 2020 at 13:34):

Let's check it does its magic properly:

example : continuous f  continuous (λ z : Y ×  × X, (f z.1).to_fun z.2.1 z.2.2) :=
iff.rfl

view this post on Zulip Jean Lo (Aug 23 2020 at 13:39):

ooh, this is very cool. thanks for the pointers!

Maybe this even just works™ with the X → ℝ →. X signature, with pcontinuous instead of continuous?

Kenny Lau said:

I think you need topological_mul_action

oh, hmm. The Mathlib Generality version of this is probably, like, a not-necessarily-continuous semigroup act (but also not really, because partial functions)? and sometimes I want that semigroup to be additive ()? Additionally, I don't expect to use the + notation. After half an attempt I've not managed to convince myself that reusing the instances helps that much.

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:46):

I guess you need to make the priority of has_uncurry_base less than that of has_uncurry_induction?

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:46):

otherwise Lean will use has_uncurry_base for A -> B -> C to turn it into, well, A -> B -> C

view this post on Zulip Reid Barton (Aug 23 2020 at 13:49):

By the way, shouldn't it be has_curry? a -> b -> c is the curried form: docs#function.curry

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:50):

yeah so uncurry turns A -> B -> C into A x B -> C

view this post on Zulip Kenny Lau (Aug 23 2020 at 13:50):

which is what Patrick intended

view this post on Zulip Jean Lo (Aug 23 2020 at 13:59):

Kenny Lau reacted with :point_right:

(what is the meaning of this?)

view this post on Zulip Kenny Lau (Aug 23 2020 at 14:02):

"thanks for the pointers"

view this post on Zulip Patrick Massot (Aug 23 2020 at 14:08):

It's funny how people think there is a priority issue here, even when they see it working flawlessly.

view this post on Zulip Reid Barton (Aug 23 2020 at 16:11):

oh I see. Maybe the variable names are unhelpful or something but I find this confusing for some reason...


Last updated: May 12 2021 at 05:19 UTC