## Stream: new members

### Topic: unexpected "bit0", "bit1" etc

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

#### Johan Commelin (Oct 06 2020 at 04:34):

The bit0 and bit1 are used for representing numerals

#### Kevin Lacker (Oct 06 2020 at 04:35):

why does it expect anything to have types involving them

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

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

#### Johan Commelin (Oct 06 2020 at 04:37):

Did you by chance mean h1.symm \t _

#### Kevin Lacker (Oct 06 2020 at 04:38):

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

#### 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))) : ℕ


#### Johan Commelin (Oct 06 2020 at 04:42):

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

#### Mario Carneiro (Oct 06 2020 at 04:43):

I think you should rewrite in the other direction

#### Kevin Lacker (Oct 06 2020 at 04:44):

what do you mean by that?

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

fixed

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


#### Mario Carneiro (Oct 06 2020 at 04:46):

when you use \t it rewrites in the reverse direction

#### Mario Carneiro (Oct 06 2020 at 04:47):

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

#### Kevin Lacker (Oct 06 2020 at 04:47):

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

#### Mario Carneiro (Oct 06 2020 at 04:48):

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

#### Mario Carneiro (Oct 06 2020 at 04:48):

that's just a bit shorter

#### Kevin Lacker (Oct 06 2020 at 04:48):

i also didnt know assumption :upside_down:

#### Mario Carneiro (Oct 06 2020 at 04:49):

okay rw h1 at this, exact this

#### Kevin Lacker (Oct 06 2020 at 04:49):

is assumption the same as exact this ?

#### Mario Carneiro (Oct 06 2020 at 04:49):

it is exact <one of my assumptions>

#### Mario Carneiro (Oct 06 2020 at 04:49):

it searches the context for something matching the goal

#### Kevin Lacker (Oct 06 2020 at 04:50):

hmm, i think iwas using finish for that

#### Mario Carneiro (Oct 06 2020 at 04:50):

heh that's a bit overkill

#### Kevin Lacker (Oct 06 2020 at 04:50):

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

#### Mario Carneiro (Oct 06 2020 at 04:50):

it's a big ol decision procedure

#### Mario Carneiro (Oct 06 2020 at 04:51):

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

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

Not at all

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

#### Mario Carneiro (Oct 06 2020 at 04:52):

as a rule of thumb

#### Mario Carneiro (Oct 06 2020 at 04:53):

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

#### Mario Carneiro (Oct 06 2020 at 04:53):

rw is relatively cheap although it has a slightly complicated desugaring

#### Mario Carneiro (Oct 06 2020 at 04:54):

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

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