defining binary operations

Stream: new members

[Alena Gusakov]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Alena Gusakov]

Ah okay, thank you!

[Alena Gusakov]

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

[Mario Carneiro]

this should be a lemma about floor

[Mario Carneiro]

probably stated in the form x < floor x + 1

[Bryan Gin-ge Chen]

See src#fract_nonneg and src#fract_lt_one

[Bryan Gin-ge Chen]

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

[Alena Gusakov]

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

[Mario Carneiro]

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

[Alena Gusakov]

Ahh okay good to know

[Mario Carneiro]

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

[Alena Gusakov]

Gotcha, thanks!

[Bryan Gin-ge Chen]

@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]

:-(

[Scott Morrison]

Oh... does library_search! work?

[Bryan Gin-ge Chen]

Ooh, it does!

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

I guess suggest is still running on the higher settings.

[Bryan Gin-ge Chen]

Ah, I see.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Opinions welcome.

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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