Zulip Chat Archive

Stream: new members

Topic: function expected at ?


view this post on Zulip Lucas Viana (Jun 16 2020 at 20:32):

On the last line of this #mwe, a is of type M → M. But then lean complains it has type m_1 and is not a function! why is that? :anguished:

import group_theory.subgroup
open function
variables (M : Type*)

instance endo_monoid : monoid (M  M) := begin
  fapply monoid.mk,
  use comp,
  intros, refl,
  use id,
  intro, refl,
  intro, refl,
end
instance endo_hasid : has_one (M  M) := by apply_instance
instance endo_semigroup : semigroup (M  M) := by apply_instance

definition dynamical_system := submonoid (M  M)

instance dyn_mem : has_mem (M  M) (dynamical_system M) := submonoid.has_mem

def orbit (x : M) (dyn : dynamical_system M) :=
{p : M | (a : M  M) (a  dyn), p = a x} -- ??

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:33):

You want (h : a \in dyn).

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:34):

Also, if you didn't use a as variable, you would have gotten a more useful error message.

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:34):

This is a very frustrating bug... the a-bug.

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:35):

With a bit of luck, this would also do what you want:

def orbit (x : M) (dyn : dynamical_system M) :=
{p : M |  f  dyn, p = f x}

view this post on Zulip Lucas Viana (Jun 16 2020 at 20:35):

so I always need to name my hypothesis when writing "exists..."?

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:35):

(I didn't test it.)

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:36):

In your initial code, change the a to f, and then look at the tactic state before the error message...

view this post on Zulip Lucas Viana (Jun 16 2020 at 20:36):

your last example does not work (I tried it before)

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:36):

You will see that there are two fs and an a.

view this post on Zulip Reid Barton (Jun 16 2020 at 20:36):

I don't think it's the a bug here--it would be the H bug.

view this post on Zulip Johan Commelin (Jun 16 2020 at 20:36):

Ok, too bad... if the short versions don't work, then you need to give more names (-;

view this post on Zulip Lucas Viana (Jun 16 2020 at 20:38):

ok, thank you :slight_smile: we could have a list of those strange bugs and their common symptoms


Last updated: May 15 2021 at 23:13 UTC