defeq

Stream: general

[Sebastien Gouezel]

In the following snipper, I don't get why refl is not able to close the goal:

lemma linear_map.with_bound (f : E →ₗ[k] F) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[k] F :=
{ cont := linear_map.continuous_of_bound f C h,
  ..f }

@[simp] lemma linear_map_with_bound_coe (f : E →ₗ[k] F) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
  ((f.with_bound C h) : E →ₗ[k] F) = f :=
begin
  ext,
  -- dunfold linear_map.with_bound,
  refl }

Here, E →ₗ[k] F is the space of linear maps from E to F, and E →L[k] F is the space of continuous linear maps (it extends linear maps, with just one additional field cont : continuous to_fun requiring the continuity of the function). Obviously, the to_funfields of f and f.with_bound C h are the same by construction, but still something is preventing Lean from computing just by itself. If I uncomment the line with dunfold, everything is OK.

[Mario Carneiro]

it's a lemma

[Mario Carneiro]

that defines data

[Sebastien Gouezel]

Ah, thanks! Stupid me.

[Kevin Buzzard]

I have run into this in the past, and I think Lean should tell me whenever I do it.

[Mario Carneiro]

It really should. You will actually get a (very confusing and misattributed) error message if you try to use it to define a def

[Kevin Buzzard]

"You just wrote lemma X : Y := Zbut Y isn't a Prop."

[Kevin Buzzard]

This issue often manifests itself in some "VM can't compute this" error

[Mario Carneiro]

lemma foo : ℕ := 1
def bar := foo
-- failed to generate bytecode for 'bar'
-- code generation failed, VM does not have code for 'foo'

[Kevin Buzzard]

I have done it often enough to know that this error means I did it, but Sebastien just managed to get a different manifestation of the issue. Yes, that's the error.

[Wojciech Nawrocki]

I ran into the "VM does not have code for" error using eq:

def one := @eq.rec
def two := @eq.drec
/- failed to generate bytecode for 'two'
code generation failed, VM does not have code for 'eq.drec' -/

Why is rec okay, but drec not? Is it because the induction motive C in drec also consumes a proof n: a = a_1?

[Mario Carneiro]

This seems like a bug. eq.drec is autogenerated, and it's a def, and it has target sort Sort l so it should have code

[Mario Carneiro]

You can copy and paste the proof of eq.drec to get code

protected def {u l} two : Π {α : Sort u} {a : α} {C : Π (a_1 : α), a = a_1 → Sort l}, C a rfl → Π {a_1 : α} (n : a = a_1), C a_1 n :=
λ {α : Sort u} {a : α} {C : Π (a_1 : α), a = a_1 → Sort l} (e_1 : C a _) {a_1 : α} (n : a = a_1),
  eq.rec (λ («_» : a = a), e_1) n n

[Wojciech Nawrocki]

Here is an even stranger instance. I define eql to be exactly the same as eq and then define something like path induction (HoTT 1.12.2) on it. Code generation fails, but it works for eq:

inductive eql {α : Sort u} (a : α) : α → Prop
| refl : eql a

def eql.path_ind {α: Type*} (C : Π x y : α, eql x y → Type*) (c: Π x: α, C x x (eql.refl x))
  : Π x y : α, Π p : eql x y, C x y p :=
λ x, @eql.drec α x (C x) (c x)
/- failed to generate bytecode for 'eql.path_ind'
code generation failed, inductive predicate 'eql' is not supported -/

def path_ind {α: Type*} (C: Π x y: α, x = y → Type*) (c: Π x: α, C x x rfl)
  : Π x y: α, Π p: x = y, C x y p :=
λ x, @eq.drec α x (C x) (c x)

[Mario Carneiro]

I think lean's support for inductive predicates is incomplete, and eq is being hard coded

[Wojciech Nawrocki]

I'm getting the same error elsewhere now, even though I'm not trying to define any code (but omega is, probably?):

example : 0 = 0 := by omega /- fine -/
example (n: ℕ) : n = n := begin
  cases n,
  { refl },
  { omega },
end /- fine -/
example (n: ℕ) : n = n := begin
  cases n,
  { omega },
  { refl },
end /- VM does not have code for 'nat.zero' -/

Does anyone know if this is expected to happen with omega? Is there a way around it?

[Mario Carneiro]

To make things more confusing:

example (n: ℕ) : n = n := begin
  cases n,
  { change 0 = 0, omega },
  { refl },
end -- fine

[Mario Carneiro]

compare:

example : nat.zero = nat.zero := by omega
-- VM does not have code for 'nat.zero'

[Wojciech Nawrocki]

Ah, so the VM has code for typeclass-0 but not nat-0. I can backport the change to fix where I originally encountered this :)

[Mario Carneiro]

No, it's a bug in eval_expr

[Mario Carneiro]

Of course the VM has code for nat.zero, it's a constructor of a data type. But it doesn't like it when you call eval_expr nat `(nat.zero); eval_expr nat `(id nat.zero) works fine

[Mario Carneiro]

this is a known bug, and mathlib has eval_expr' for this, but omega forgot to use it

[Wojciech Nawrocki]

Ah, grep tells me almost no tactics that use eval_expr use the primed version. Should they all use it instead?

[Mario Carneiro]

#1711

[Mario Carneiro]

Actually, I think that omega should probably not be using eval_expr' nat here at all, and instead it should use expr.to_nat, which more accurately detects numerals