unexpected "bit0", "bit1" etc

Stream: new members

[Kevin Lacker]

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]

The bit0 and bit1 are used for representing numerals

[Kevin Lacker]

why does it expect anything to have types involving them

[Johan Commelin]

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

[Johan Commelin]

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]

Did you by chance mean h1.symm \t _

[Kevin Lacker]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

I think you should rewrite in the other direction

[Kevin Lacker]

what do you mean by that?

[Mario Carneiro]

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

[Kevin Lacker]

fixed

[Mario Carneiro]

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]

when you use \t it rewrites in the reverse direction

[Mario Carneiro]

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

[Kevin Lacker]

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

[Mario Carneiro]

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

[Mario Carneiro]

that's just a bit shorter

[Kevin Lacker]

i also didnt know assumption :upside_down:

[Mario Carneiro]

okay rw h1 at this, exact this

[Kevin Lacker]

is assumption the same as exact this ?

[Mario Carneiro]

it is exact <one of my assumptions>

[Mario Carneiro]

it searches the context for something matching the goal

[Kevin Lacker]

hmm, i think iwas using finish for that

[Mario Carneiro]

heh that's a bit overkill

[Kevin Lacker]

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

[Mario Carneiro]

it's a big ol decision procedure

[Mario Carneiro]

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

[Kevin Lacker]

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

[Mario Carneiro]

Not at all

[Mario Carneiro]

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

[Mario Carneiro]

as a rule of thumb

[Mario Carneiro]

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

[Mario Carneiro]

rw is relatively cheap although it has a slightly complicated desugaring

[Mario Carneiro]

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

[Scott Morrison]

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