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

Stream: new members

[Jean Lo]

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

[Patrick Massot]

This issue is sadly well-known.

[Kenny Lau]

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

[Patrick Massot]

and I was writing what Kenny wrote.

[Jean Lo]

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

[Kenny Lau]

oh, continuity

[Kenny Lau]

let's look at how topological_group does this then

[Kenny Lau]

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]

oh gee

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

[Kenny Lau]

yay I'm still faster

[Kenny Lau]

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]

I think you need topological_mul_action

[Kenny Lau]

that is topological_semimodule restricted to mul_action

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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

[Kenny Lau]

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

[Reid Barton]

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

[Kenny Lau]

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

[Kenny Lau]

which is what Patrick intended

[Jean Lo]

Kenny Lau reacted with :point_right:

(what is the meaning of this?)

[Kenny Lau]

"thanks for the pointers"

[Patrick Massot]

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

[Reid Barton]

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