Zulip Chat Archive

Stream: new members

Topic: defining binary operations


view this post on Zulip 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```

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 :=

view this post on Zulip 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.

view this post on Zulip Alena Gusakov (Jun 24 2020 at 00:22):

Ah okay, thank you!

view this post on Zulip Alena Gusakov (Jun 24 2020 at 00:23):

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

view this post on Zulip Mario Carneiro (Jun 24 2020 at 00:26):

this should be a lemma about floor

view this post on Zulip Mario Carneiro (Jun 24 2020 at 00:26):

probably stated in the form x < floor x + 1

view this post on Zulip Bryan Gin-ge Chen (Jun 24 2020 at 00:26):

See src#fract_nonneg and src#fract_lt_one

view this post on Zulip Bryan Gin-ge Chen (Jun 24 2020 at 00:28):

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

view this post on Zulip Alena Gusakov (Jun 24 2020 at 00:29):

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

view this post on Zulip Mario Carneiro (Jun 24 2020 at 00:29):

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

view this post on Zulip Alena Gusakov (Jun 24 2020 at 00:29):

Ahh okay good to know

view this post on Zulip Mario Carneiro (Jun 24 2020 at 00:29):

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

view this post on Zulip Alena Gusakov (Jun 24 2020 at 00:30):

Gotcha, thanks!

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:36):

:-(

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:36):

Oh... does library_search! work?

view this post on Zulip Bryan Gin-ge Chen (Jun 24 2020 at 00:36):

Ooh, it does!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:37):

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

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:37):

I guess suggest is still running on the higher settings.

view this post on Zulip Bryan Gin-ge Chen (Jun 24 2020 at 00:37):

Ah, I see.

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:39):

Opinions welcome.

view this post on Zulip Scott Morrison (Jun 24 2020 at 00:39):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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