## Stream: new members

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

#### 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.)

#### Kenny Lau (Aug 23 2020 at 13:12):

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

#### Patrick Massot (Aug 23 2020 at 13:12):

and I was writing what Kenny wrote.

#### Jean Lo (Aug 23 2020 at 13:13):

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

oh, continuity

#### Kenny Lau (Aug 23 2020 at 13:14):

let's look at how topological_group does this then

#### 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))


#### 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))


#### Kenny Lau (Aug 23 2020 at 13:16):

yay I'm still faster

#### 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]
[semimodule R M] : Prop :=
(continuous_smul : continuous (λp : R × M, p.1 • p.2))


#### Kenny Lau (Aug 23 2020 at 13:18):

I think you need topological_mul_action

#### Kenny Lau (Aug 23 2020 at 13:18):

that is topological_semimodule restricted to mul_action

#### Patrick Massot (Aug 23 2020 at 13:18):

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

#### Patrick Massot (Aug 23 2020 at 13:19):

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

#### 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))


#### 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?

#### 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


#### 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


#### 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.

#### 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?

#### 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

#### 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

#### Kenny Lau (Aug 23 2020 at 13:50):

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

#### Kenny Lau (Aug 23 2020 at 13:50):

which is what Patrick intended

#### Jean Lo (Aug 23 2020 at 13:59):

Kenny Lau reacted with :point_right:

(what is the meaning of this?)

#### Kenny Lau (Aug 23 2020 at 14:02):

"thanks for the pointers"

#### 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.

#### 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