Stream: new members

Topic: function expected at ?

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


Johan Commelin (Jun 16 2020 at 20:33):

You want (h : a \in dyn).

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.

Johan Commelin (Jun 16 2020 at 20:34):

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

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}


Lucas Viana (Jun 16 2020 at 20:35):

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

Johan Commelin (Jun 16 2020 at 20:35):

(I didn't test it.)

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

Lucas Viana (Jun 16 2020 at 20:36):

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

Johan Commelin (Jun 16 2020 at 20:36):

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

Reid Barton (Jun 16 2020 at 20:36):

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

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 (-;

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