Creating opaque definition for the kernel

Stream: lean4

[Yann Herklotz]

We are using dependent types which may be quite expensive if they are ever unfolded. We found that even just elaborating an identifier of that type would mean the type would be normalised to find out if it is a function type or not, regardless of if it is being applied or not. To work around this, we then just wanted to make the definition of our type irreducible so that this check wouldn't start reducing our term.

However, it seems like some tactics use isTypeCorrect to do type checking at the Meta level. This function sets Transparency.all, meaning the definition will be reducible again, and we then get timeouts again during whnf.

import Mathlib -- needed for whnf tactic

def type' : Nat → Type
  | 0 => Nat
  | n+1 => type' n

seal type' in
example : ∀ (a : type' 1000), ∃ (a:Nat), True := by?
  intro a
  -- simulating a call to `isTypeCorrect` which times out.
  with_unfolding_all whnf at a
  exists a

In the above, I would like whnf to not do anything, because I would like type' to stay sealed. Is this something that is possible? I guess the definition should also be opaque to the kernel when it is doing type-checking as well to avoid reduction there as well.

[Henrik Böving]

You can use opaque instead of def to make something that is truly not unfoldable

[Yann Herklotz]

Oh cool, is there a way to make it semireducible in certain scenarios? For certain specific inputs we would like to be able to reduce them (in a separate theorem maybe) but in general (in the final proof) we know we don't even want to try to reduce them.

[Henrik Böving]

opaque means truly untouchable, you can't do anything to it under any circumstances

[Yann Herklotz]

Hmm, so you can't prove any properties about it then either I guess.

[Henrik Böving]

You can prove lot's of properties about them, just not any properties that concern their definition. But e.g. if you have an opaque Foo : Fin 10 you will still be able to show that it is less than 10 and so on.

[Henrik Böving]

It's not really easy to tell what exactly you are looking for based on your example though

[Yann Herklotz]

Ah yes, that's true. In our case the interesting properties are more computational and you get them out when you reduce the type. However, due to the normalisation during elaboration and isTypeCorrect checks we want to avoid doing that in most proofs, so that we limit where we actually reduce them.

For example, we might build up a type like the following, and prove a property about it in example. However, in the final theorem we would like comp_type to be completely opaque to avoid any expensive reduction.

import Lean
import Batteries

def comp_type (T:Type) ident :=
  (((Batteries.RBMap.ofList [(1, T), (2, T), (3, T), (4, T), (5, T)] Ord.compare).mergeWith (λ _ a _ => a)
          (Batteries.RBMap.ofList [(1, T), (2, T)] Ord.compare)).find? ident)

example (T:Type) : comp_type T 1 = some T := by rfl

seal comp_type in
theorem prop (t:(comp_type T 1).getD Nat) : True := True.intro

Note that the rfl proof already takes 7 seconds but kernel type-checking is near instant, and it's mainly due to this that we get performance issue with Meta level reduction on our types.

[Yann Herklotz]

We discuss this a bit in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Reduction.20of.20terms.20with.20free.20variables.20is.20expensive/near/469077847 as well, and are now using kernel reduction at the Meta level like @Kyle Miller had suggested.

However, maybe this is just the wrong approach, and we should rethink how our types are generated and represented.

[Mario Carneiro]

One way you can avoid unfolding in types is to make structure newtype wrappers around those types. The resulting type is isomorphic to the original but not defeq, and it is opaque and will not reduce in any way (but you can use the projection/constructor to get at the contained value)

[Yann Herklotz]

Interesting, thank you both for the insights, I'll try that out!

[Mario Carneiro]

structure Wrapper (T : Type) where get : T
theorem prop {T} (t: Wrapper ((comp_type T 1).getD Nat)) : True := True.intro

[Yann Herklotz]

Thanks, I think this will work quite well for us in practice too, it avoids the inherent reduction nicely.

theorem is_t (T:Type) : comp_type T 1 = some T := by rfl
theorem prop {T} (t: Wrapper ((comp_type T 1).getD Nat)) : ∃ (a : T), True := by
  rw [is_t] at t; exists t.get

[Yann Herklotz]

I've continued to run into reduction issues actually, even when the type is Wrapped. In the following (Link to web version), I would ideally like to define a Prop similar to abc, which also should be safe and avoid reducing type', but I now run into a the delaborator trying to show the goal created by constructor, meaning it tries to reduce type'.

axiom P {A} : A → Prop

structure abc (A) : Prop where
  a : ∀ (n : Wrapper A), P n.get

-- Delaborator seems to error out after `constructor`.  It seems to try and reduce `type'`,
-- maybe when it encounters `n.get`?
-- seal type' in
example : abc (type' 10000) := by
  constructor
  intro H

Instead, defining the structure explicitly runs into the same issue as before I think. Because I use n.get, it will try and reduce type' to figure out if it is a function or not (which is why I preferred the previous solution).

axiom P' : type' 10000 → Prop
-- `n.get` elaboration times out, because it tries to reduce `type'`
-- seal type' in
structure abc' : Prop where
  a : ∀ (n : Wrapper <| type' 10000), P' n.get

It seems like in both cases I need to seal type' as well as wrap it to try and avoid all the implicit reduction that goes on when elaborating and delaborating terms. Is there any way we could avoid doing this? Is it uncommon in Lean to want to compute types in this way? We are essentially building a map of types by recursively merging them, but it seems like we have to tread extremely carefully when we have such a type anywhere, because Lean might try to reduce it.

[Kyle Miller]

Interesting, this tries to reduce type', causing a "max recursion depth" error:

def a (n : Wrapper (type' 10000)) := Wrapper.get n

Tip for dealing with delaborator failures: you can do set_option pp.raw true to turn it off, and it prints some representation of the raw expressions.

[Yann Herklotz]

Ah yes, I did have that locally (doesn't seem to work in the online version), but I thought I couldn't continue with the proof, but it seems to be possible, but as expected quite hard to read. Ah sorry I had pp.rawOnError, I didn't know pp.raw turned off the delaborator, that's helpful, thanks!

And yeah I guess I don't understand exactly why type' is reduced in your example.

[Kyle Miller]

(I'm not sure if it's possible, but maybe rawOnError should be able to catch runtime errors too.)

[Kyle Miller]

I've tried looking through set_option trace.Meta.isDefEq true, but I'm not seeing where type' would be unfolded, but set_option diagnostics true shows it definitely is.

My current guess is that isDefEq's check that the type is a forall is causing it to unfold. I think there is a lot of code that assumes reducing types is relatively cheap.

[Yann Herklotz]

Yeah I knew this check happened during elaboration of identifiers, but I was hoping it wouldn't get triggered here. It seems like isDefEq shouldn't have to unfold anything, as the types should be structurally equal. But yeah somewhere it is probably reducing the type to check for a forall again. Tracing trace.Meta.whnf shows that too like the diagnostics. In some of these cases it seems like this check is unnecessary, but you may be right that too much code assumes types can be reduced.

set_option maxHeartbeats 100
set_option trace.Meta.whnf true in
def a (n : Wrapper (type' 10000)) := Wrapper.get n

We may have to try a different representation then to avoid creating types that are performing too much computation.

[Kyle Miller]

Oh right, more likely are the pervasive telescope calculations, which are used to analyze the parameters to functions.

For example, the delaboration issue is probably from this calculation, which is also looking for the types of parameters after all the supplied arguments, because that is used to analyze how to pretty print applications.

[Yann Herklotz]

Yeah thanks, it does make sense that assuming types will be cheap to reduce could lead to better user experiences. I think ideally using seal to completely hide the implementation of our types so it is never reduced would work well for us. We unfortunately still seem to hit some cases where reduction is forced with withTransparency .all, which I'm assuming is coming from isTypeCorrect, and I'm not sure I understand exactly why it's needed, although removing it breaks everything.