Zulip Chat Archive

Stream: new members

Topic: unexpected "bit0", "bit1" etc


view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:31):

I'm getting a weird error message. The following code does not compile:

lemma modular_constraint (c n : )
(h1 : n = 10 * c + 6  6 * 10 ^ (nat.digits 10 c).length + c = 4 * n) :
(6 * 10 ^ (nat.digits 10 c).length) % 39 = 24 := sorry /- proof omitted for brevity -/

lemma alt_1_digit (c n : ) (h1 : (nat.digits 10 c).length = 1)
(h2 : n = 10 * c + 6  6 * 10 ^ (nat.digits 10 c).length + c = 4 * n) : false :=
begin
  have h3 : 6 * 10 ^ 1 % 39 = 24, from h1  (modular_constraint c n h2),
  norm_num at h3,
end

(The error is on the have h3... line.)

This surprised me because essentially the same code works when the constant is 0 instead of 1. The error message is:

87:43: "eliminator" elaborator type mismatch, term
  modular_constraint c n h2
has type
  6 * 10 ^ (10.digits c).length % 39 = 24
but is expected to have type
  bit0 (bit1 (10.digits c).length) * bit0 (bit1 (bit0 (10.digits c).length)) ^ (10.digits c).length %
      bit1 (bit1 (bit1 (bit0 (bit0 (10.digits c).length)))) =
    bit0 (bit0 (bit0 (bit1 (10.digits c).length)))

This seems like some mistyping to me - bit0 and bit1 appear to be library functions that manipulate binary numbers, but everything here is simple operations on naturals. Perhaps it's misinterpreting the ^ operator, automatically guessing what it is, and 0 and 1 are handled differently? Or am I barking up the wrong tree?

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:34):

The bit0 and bit1 are used for representing numerals

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:35):

why does it expect anything to have types involving them

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:35):

When you type 24, then Lean sees bit0 12, which is in fact bit0 (bit0 6) which is in fact ...

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:37):

So, when you substitute (nat.digits 10 c).length = 1 into some formula with numerals... it is trying to replace the 1 that is nested deeply inside a stack of bit0s and bit1 by (nat.digits 10 c).length

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:37):

Did you by chance mean h1.symm \t _

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:38):

no, like if i find and replace 1 with 0 it works

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:41):

24 is literally the expression bit0 (bit0 (bit0 (bit1 1))):

set_option pp.numerals false
#check 24
-- bit0 (bit0 (bit0 (bit1 has_one.one))) : ℕ

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:42):

Ok, I see... maybe the best thing to do is rw and use { occs := occurences.pos [3] } or something like that as rewrite config

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:43):

I think you should rewrite in the other direction

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:44):

what do you mean by that?

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:44):

Also, an #mwe suggestion: put sorry instead of /- proof omitted for brevity -/ so that it is syntactically correct

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:45):

fixed

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:46):

begin
  have h3 : 6 * 10 ^ 1 % 39 = 24,
  { have := modular_constraint c n h2,
    rwa h1 at this },
  norm_num at h3,
end

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:46):

when you use \t it rewrites in the reverse direction

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:47):

and it also rewrites the goal instead of the argument on the right of the \t

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:47):

rwa... there just never stop being more tactics that do slightly different things

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:48):

you can use rw h1 at this, assumption if you prefer

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:48):

that's just a bit shorter

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:48):

i also didnt know assumption :upside_down:

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:49):

okay rw h1 at this, exact this

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:49):

is assumption the same as exact this ?

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:49):

it is exact <one of my assumptions>

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:49):

it searches the context for something matching the goal

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:50):

hmm, i think iwas using finish for that

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:50):

heh that's a bit overkill

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:50):

it's fewer characters to type, seems like the simplest thing to do

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:50):

it's a big ol decision procedure

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:51):

when the actual proof term is just this you should probably use a lighter weight tactic

view this post on Zulip Kevin Lacker (Oct 06 2020 at 04:51):

I feel like it's essentially impossible to know which tactics are lightweight and which are not

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:51):

Not at all

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:52):

Anything which desugars to the core logic operations is cheap, everything that involves search of some kind is expensive

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:52):

as a rule of thumb

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:53):

so intro exact apply refine are cheap, simp cc finish tidy are expensive

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:53):

rw is relatively cheap although it has a slightly complicated desugaring

view this post on Zulip Mario Carneiro (Oct 06 2020 at 04:54):

assumption is usually cheap, although occasionally you can step on a defeq mine

view this post on Zulip Scott Morrison (Oct 06 2020 at 05:09):

you can also write show_term { some_tactic } to investigate the terms that a tactic is producing. It's often enlightening!


Last updated: May 12 2021 at 23:13 UTC