## Stream: new members

### Topic: defining binary operations

#### Alena Gusakov (Jun 24 2020 at 00:13):

So I'm trying to work through Dummit and Foote using Lean and I've been wrestling with this issue for a little bit. The problem I'm working on is, if you have the interval [0, 1) in the reals, and a binary operation  x ⋆ y = x + y - ⌊ x + y ⌋, prove that this is a group. Here's what I have so far:

import algebra.group.basic
import data.real.basic

noncomputable theory
open_locale classical

--namespace group

def star_set := { x : ℝ | 0 ≤ x ∧ x < 1}

#check star_set

section star_group

--instance : floor star_set := ⟨ℝ.floor⟩

#check has_coe_to_sort
#check semigroup

def star : ℝ → ℝ → ℝ
| x y := x + y - ⌊ x + y ⌋

notation x⋆y := star x y
variables (x y : ℝ) (A : Type*)

#check star_set

lemma star_closed {a b : star_set} (a b : ℝ) : (a ⋆ b) ∈ star_set :=
begin
unfold star,
unfold star_set,
split,
sorry,
end

lemma star_assoc {a b c : star_set} : (a ⋆ b ⋆ c) = (a ⋆ (b ⋆ c)) :=
begin
sorry,
end

end star_group


#### Alena Gusakov (Jun 24 2020 at 00:16):

Basically, the problem that I'm having now is, if I don't have (a b : ℝ) declared in the assumptions, then the goal looks like ⊢ ↑a + ↑b - ↑⌊↑a + ↑b⌋ ∈ {x : ℝ | 0 ≤ x ∧ x < 1}

#### Alena Gusakov (Jun 24 2020 at 00:17):

I think it's probably a casting problem, I just don't know how to define things to fix it

#### Bryan Gin-ge Chen (Jun 24 2020 at 00:18):

This is almost surely not what you want:

lemma star_closed {a b : star_set} (a b : ℝ) : (a ⋆ b) ∈ star_set :=


This gives you two as and two bs of different types:

1 goal
a b : ↥star_set,
a b : ℝ
⊢ (a⋆b) ∈ star_set


#### Bryan Gin-ge Chen (Jun 24 2020 at 00:20):

You'll want something like this instead:

lemma star_closed {a b : ℝ} (ha : a ∈ star_set) (hb : b ∈ star_set) :
(a ⋆ b) ∈ star_set :=


#### Bryan Gin-ge Chen (Jun 24 2020 at 00:22):

Also, you can define star_set using src#set.Ico and I suspect that some Ico lemmas will come in handy.

#### Alena Gusakov (Jun 24 2020 at 00:22):

Ah okay, thank you!

#### Alena Gusakov (Jun 24 2020 at 00:23):

Actually wait - I still have this problem: ⊢ a + b - ↑⌊a + b⌋ < 1

#### Mario Carneiro (Jun 24 2020 at 00:26):

this should be a lemma about floor

#### Mario Carneiro (Jun 24 2020 at 00:26):

probably stated in the form x < floor x + 1

#### Bryan Gin-ge Chen (Jun 24 2020 at 00:28):

suggest can find these, but library_search doesn't for some reason.

#### Alena Gusakov (Jun 24 2020 at 00:29):

I mean the problem is the up arrow ↑⌊a + b⌋

#### Mario Carneiro (Jun 24 2020 at 00:29):

there is no problem, the up arrow also appears in these theorems about floor and fract

#### Alena Gusakov (Jun 24 2020 at 00:29):

Ahh okay good to know

#### Mario Carneiro (Jun 24 2020 at 00:29):

because floor returns an int and it needs to be coerced back to the base ring

Gotcha, thanks!

#### Bryan Gin-ge Chen (Jun 24 2020 at 00:35):

@Scott Morrison : MWE:

import data.real.basic

noncomputable def star : ℝ → ℝ → ℝ
| x y := x + y - ⌊ x + y ⌋

lemma star_closed {a b : ℝ}
(ha : a ∈ set.Ico (0:ℝ) 1) (hb : b ∈ set.Ico (0:ℝ) 1) :
(star a b) ∈ set.Ico (0:ℝ) 1 :=
begin
unfold star,
split,
{ try { library_search }, -- library_search fails
suggest, -- but suggest works: Try this: exact fract_nonneg (a + b)
sorry },
{ try { library_search },
suggest,
sorry },
end


:-(

#### Scott Morrison (Jun 24 2020 at 00:36):

Oh... does library_search! work?

Ooh, it does!

#### Scott Morrison (Jun 24 2020 at 00:37):

We made library_search _less powerful_ recently, in order to get it to produce more useful results.

#### Scott Morrison (Jun 24 2020 at 00:37):

(We reduced the level of irreducibility that apply is allowed to blast through.)

#### Scott Morrison (Jun 24 2020 at 00:37):

I guess suggest is still running on the higher settings.

Ah, I see.

#### Scott Morrison (Jun 24 2020 at 00:37):

I considered have library_search always run in library_search! mode if the first pass failed.

#### Scott Morrison (Jun 24 2020 at 00:38):

But I had so few test cases where it was failing at all I decided not to do this.

#### Scott Morrison (Jun 24 2020 at 00:38):

Given that library_search timing out is scarcely worse than it failing, perhaps we should always do the second pass.

#### Scott Morrison (Jun 24 2020 at 00:39):

Opinions welcome.

#### Scott Morrison (Jun 24 2020 at 00:39):

It is a bit of hassle to remember to have to try again with !.

#### Bryan Gin-ge Chen (Jun 24 2020 at 00:39):

How is doing a first weaker pass and then a second stronger pass different from always just doing the stronger pass?

#### Bryan Gin-ge Chen (Jun 24 2020 at 00:41):

Nevermind, I see, probably the weaker pass often gives something more useful which occurs later in the search with the stronger pass.

#### Alex J. Best (Jun 24 2020 at 00:49):

Yeah I've felt library search be a bit weaker recently, but wondered if it was just me being silly / asking it harder questions than I used to, I had no idea it had actually changed in this way. I think either a second pass, or at least a message "failed: try library_search!" rather than just "failed" would be good.

#### Scott Morrison (Jun 24 2020 at 02:06):

(I've moved the tail end of this thread, which turned into a discussion of library_search` to another thread.)

Last updated: May 16 2021 at 05:21 UTC