Zulip Chat Archive

Stream: general

Topic: dot notation


view this post on Zulip Yury G. Kudryashov (May 23 2020 at 21:25):

I've tried to convert some lemmas about eq_on_source in local_equiv to use dot notation, and in many cases I can't use dot notation due to an issue illustrated by the following #mwe

def nat.same_parity (a b : ) : Prop := a % 2 = b % 2

instance nat.same_parity_setoid : setoid  :=
{ r := nat.same_parity,
  iseqv := ⟨λ n, rfl, λ a b h, h.symm, λ a b c hab hbc, hab.trans hbc}

axiom nat.same_parity.add {a b : } (h : a  b) (c : ) : a + c  b + c

lemma nat.same_parity.add_one {a b : } (h : a  b) : a + 1  b + 1 :=
nat.same_parity.add h 1 -- works

lemma nat.same_parity.add' {a b : } (h : a  b) (c : ) : a + c  b + c :=
h.add c -- fails

lemma nat.same_parity.add_one' {a b : } (h : a  b) : a + 1  b + 1 :=
h.add_one -- works

view this post on Zulip Yury G. Kudryashov (May 23 2020 at 21:26):

Is there any good way to fix this?

view this post on Zulip Yury G. Kudryashov (May 23 2020 at 21:26):

I mean, make h.add c in this example work.

view this post on Zulip Sebastien Gouezel (May 30 2020 at 20:23):

Dot notation has become ubiquitous in the goal state recently, and this is in general very nice, but it is very hard to parse expressions such as

p * (x.log * (p - 1)).exp = (x.log * p).exp * (x⁻¹ * p)

Is there a trick to tell Lean that, for some functions, it should not use the dot notation?

view this post on Zulip Patrick Massot (May 30 2020 at 20:25):

Ouch, this is even worse than the f.ker example.

view this post on Zulip Alex J. Best (May 30 2020 at 20:25):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_matrix.20change/near/197841073

view this post on Zulip Johan Commelin (May 30 2020 at 20:28):

set_option rtl true [/joking]

view this post on Zulip Sebastien Gouezel (May 30 2020 at 20:30):

I want @[please_dont_use_polish_notation] def exp := ... :)

view this post on Zulip Gabriel Ebner (May 30 2020 at 20:31):

Please file an issue so that we don't forget this.

view this post on Zulip Sebastien Gouezel (May 30 2020 at 20:36):

Done.

view this post on Zulip Kenny Lau (May 30 2020 at 20:37):

it isn't so hard to parse for me

view this post on Zulip Kevin Buzzard (May 30 2020 at 20:38):

Maybe you know python?

view this post on Zulip Kenny Lau (May 30 2020 at 20:39):

I do know Python

view this post on Zulip Chris Hughes (May 30 2020 at 20:47):

Could we have a rule like don't use dot notation if the namespace is already open?


Last updated: May 16 2021 at 21:11 UTC