FloatArray function bodies are not exposed from the module

Stream: lean4

[Pavel Perikov]

FloatArray is defined as a wrapper over Array Float(its data model), all the function bodies (like FloatArray.size or FloatArray.set are provided but not exposed, so module system prevents unfolding outside the model. If I get it right this prevents even the basic things to be proven (like "set doesn't change the size").

How things are supposed to be?

[Henrik Böving]

FloatArray has not yet shifted into the focus of verification work for Lean, these things might change in the future but they are not a top priority at the moment. In particular given that you can't prove things about float to begin with.

[Pavel Perikov]

I see. The question was about the simple fact: the bodies of the functions are not exposed (exposing them will automatically allow to prove trivial things that are available for Array). I can't prove things about floats, but I can prove things about Array Float (we have lemmas for this).

The difference is exposing FloatArray data model. Requires nothing, but the decision if this is a correct way to go.

I asked for the opinion "what's right and wrong" lacking enough experience with Lean4. I clearly see FloatArray is not the priority.

To me the difference is if I start using Lean4 as a "programming language with proof capabilities" in a pilot project will I:

• have to fork it
• have to provide my own FloatArray
• forget about it for now, until some areas will get some focus

[Markus Himmel]

You can use import all to get access to non-exposed definitions:

module

import all Init.Data.FloatArray.Basic

example {fs : FloatArray} : fs.size = fs.data.size := by
  rw [FloatArray.size]

The main downside of this is that your proofs will break if the standard library authors decide to change the definitions when they work on FloatArray, but that might be acceptable in your case.

[Pavel Perikov]

Markus Himmel said:

You can use import all to get access to non-exposed definitions:

module

import all Init.Data.FloatArray.Basic

example {fs : FloatArray} : fs.size = fs.data.size := by
  rw [FloatArray.size]

The main downside of this is that your proofs will break if the standard library authors decide to change the definitions when they work on FloatArray, but that might be acceptable in your case.

That's exactly what I needed. As I said my experience with Lean is very limited and I'm just exploring "how things work". AI doesn't help all the time, so sometimes it's simpler to use NI :)

Thank you!