# Zulip Chat Archive

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

s? 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.)

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

This issue is sadly well-known.

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

?

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

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]
[topological_space M] [add_comm_monoid M]
[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