Working with constants

Stream: lean4

[Tomas Skrivan]

I'm experimenting with using tactic mode to assemble programs given a specification. In my case, the specification is given by an expression containing non-computable functions. In the tactic mode, I want to eliminate these non-computable functions and produce runnable code.

Here is a bit silly minimal working example where I define an opaque function opaque_id and provide an axiom opaque_id_definition what the function actually does. In my real code, I have for example opaque function integrate with axiom defining what integrate does on continuous functions.

variable {β : Type} [Inhabited β]

constant opaque_id : β → β
axiom opaque_id_definition (b : β) : opaque_id b = b

inductive Impl : {α : Type _}  → (spec : α) → Type _
  | pure  {α : Type u}
          (impl : α) : Impl impl
  -- In my real code, I have more constructors like adding a runtime check.

def Impl.assemble {α} {a : α} : Impl a → α
  | Impl.pure impl => impl

def id_impl : Impl (opaque_id : β → β) :=
by
  conv => enter [1,n]
          rw [opaque_id_definition]

  apply Impl.pure

#eval (id_impl.assemble 42)

Unfortunately, (id_impl.assemble 42) evaluates to 0 and not 42.

Trying to prove that id_impl.assemble = id produces:

def id_impl_proof : id_impl.assemble = (λ x : β => x) :=
by
  simp [id_impl, Impl.assemble]

the goal is

(match opaque_id, Eq.mpr (_ : Impl opaque_id = Impl fun n => n) (Impl.pure fun n => n) :
      (a : β → β) → Impl a → β → β with
    | impl, Impl.pure .(impl) => impl) =
    fun x => x

Any idea how to change the setup to make (id_impl.assemble 42) to evaluate to 42 ?

[Tomas Skrivan]

Maybe the opaque_id should be stated as an axiom to be truly non-computable. Then #eval (id_impl.assemble 42) is giving somewhat expected error:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'opaque_id', and it does not have executable code

However, I thought that by the tactic rw [opaque_id_definition] I have eliminated the non-computable opaque_id from the definition and making the code runnable.

[Mac]

@Tomas Skrivan What you are doing confuses me so much and I have so many questions.

First, why are you using tactic mode to write code? That really is not what it is designed to do.

Second, opaque_id where β is a Nat is (code-wise) just def opaque_id (n : Nat) := 0. This is because0 is the default value for Nat in its Inhabited instance, and this is why #eval (id_impl.assemble 42) returns 0.

Also note that rw [opaque_id_definition] just affects the type, it doesn't change anything execution wise. This is because its type is a Prop and is thus completely erased at runtime.

[Tomas Skrivan]

I understand that it is confusing and tactic mode is designed to prove things. However, I have an idea how to use tactic mode to write programs(at least special parts of it) and I want to try it out.

I think the original question really should have had axiom instead of constant in the definition of opaque_id

axiom opaque_id : β → β

Then #eval (id_impl.assemble 42) does not evaluate at all, but I want it to evaluate to 42.

---

Anyway, I will try to explain my mental model about Impl:

The goal Impl (fun x => f x) means, please construct an implementation of function f. If f is already computable, you can finish the goal by apply Impl.pure that stores f into Impl (fun x => f x). If f is non-computable, you should first transform into computable g for which you know that f=g. Then calling Impl.pure will hopefully stores g into Impl (fun x => f x).

Once you have Impl (fun x => f x), you can use assemble to extract the computable function that you can execute.

[Tomas Skrivan]

An example why I'm doing this. I'm experimenting with automatic differentiation. I have postulated gradient operator ∇ and an opaque symbol and have bunch of theorems how to eliminate it. Example of computing gradient of x*x

def square_grad : Impl (∇ (λ x : ℝ => x*x)) :=
by
  simp [gradient]
  autograd

  finish_impl

After the tactic autograd the goal is Impl fun x => 1 * x + x * 1 where fun x => 1 * x + x * 1 is nice computable function. For now, the tactic finish_impl is just does apply Impl.pure, in the future I want to somehow check computability of the final term.

[Mario Carneiro]

If you want opaque_id to evaluate, then shouldn't you give it a definition? An axiom about a constant is not a definition, it does not have any computational content and lean has no idea how to turn it into running code

[Mario Carneiro]

that is, use constant opaque_id : β → β := id if you want it to #eval

[Tomas Skrivan]

The thing is that I want to write ∇ f for any function without having to supply proof that f is differentiable. If f is not differentiable then ∇ f is just not defined but if it is differentiable then ∇ f expands to the standard definition.

This is the reason to split opaque_id into two axioms, just postulating the existence of the symbol and then the actual definition.

[Sebastien Gouezel]

And how should Lean know if your function is differentiable or not?

[Tomas Skrivan]

I have definitions and proof automation for that already.

[Tomas Skrivan]

I'm using typeclass system to automatically prove that a function is differentiable. So I have bunch of instances like:

instance (f : Y → Z) (g : X → Y) [IsDiff f] [IsDiff g] : IsDiff (comp f g) := ...

composition of two differentiable functions is a differentiable one

[Sebastien Gouezel]

I don't get it. Determining if a function is differentiable is probably undecidable algorithmically (since even determining if two reals numbers are equal is undecidable algorithmically), so you can not hope Lean to make the right decision all the time.

[Sebastien Gouezel]

What you describe is a procedure that, sometimes, will determine that the function is differentiable. But what if it is differentiable but your procedure is not able to show it?

[Tomas Skrivan]

I'm not saying I can prove differentiability about anything. But I can do it automatically for certain class of functions.

[Tomas Skrivan]

But what if it is differentiable but your procedure is not able to show it?

Then I have to prove it manually.

[Tomas Skrivan]

Or more precisely, I'm not saying I can decide differentiability of every function. But if I can prove differentiability then I also have bunch of reduction rules for the differential like the chain rule:

δ (comp f g) x dx = δ f (g x) (δ g x dx)

[Mario Carneiro]

In theory, the following should work (I think it does in lean 3), but something seems to be different about the noncomputable checker and neither the second def nor the #eval works. But it doesn't evaluate the wrong thing at least

variable {β : Type} [Inhabited β]

axiom opaque_id : β → β
axiom opaque_id_definition (b : β) : opaque_id b = b

inductive Impl {α : Type _} : (spec : α) → Type _
  | pure (impl : α) : Impl impl

def Impl.assemble {α} {a : α} : Impl a → α
  | Impl.pure impl => impl

theorem opaque_id_eq : @opaque_id α = id := by
  funext x; rw [opaque_id_definition]; rfl

def id_impl : Impl (opaque_id : β → β) := opaque_id_eq ▸ ⟨_⟩

def Impl.mk {α} {a : α} : (impl : α) → a = impl → Impl a
  | _, rfl => ⟨_⟩

def id_impl' : Impl (opaque_id : β → β) := Impl.mk _ opaque_id_eq

#eval (id_impl.assemble 42)

[Mac]

@Mario Carneiro I was trying a similar thing and was also confused why it wasn't working

[Mario Carneiro]

I guess the issue is that in the signature of

def Impl.mk {α} {a : α} : (impl : α) → a = impl → Impl a

there is nothing to indicate to the compiler that impl is computationally relevant but a isn't, so the noncomputable checker demands that the a input is computable too, which fails because it is instantiated to opaque_id in id_impl'

[Mario Carneiro]

I think you need to do something similar to docs#erased to launder the value a through a Type argument

[Mac]

Here is what I was trying:

variable {β : Type} [Inhabited β]

constant opaque_id : β → β
axiom opaque_id_definition (b : β) : opaque_id b = b

inductive Impl : {α : Type _}  → (spec : α) → Type _
  | pure  {α : Type u}
          (impl : α) : Impl impl
  -- In my real code, I have more constructors like adding a runtime check.

def Impl.assemble {α} {a : α} : Impl a → α
  | Impl.pure impl => impl

theorem opaque_id_eq_id [Inhabited β ] : opaque_id (β := β) = id := by
  funext x; rw [opaque_id_definition]; rfl

def id_impl : Impl (opaque_id : β → β) :=
  cast (by rw [opaque_id_eq_id]) <| Impl.pure id

#eval id_impl.assemble 42 -- 0 (why????)

[Mario Carneiro]

I really hope lean 4 gets direct support for erasure, because the lean 3 erased has a bunch of unnecessary overhead

[Tomas Skrivan]

@Mario Carneiro The example unfortunately does not work under lean 4.

[Mario Carneiro]

my example should work up to the last two commands, like I said

[Mario Carneiro]

in particular id_impl works (passes the noncomputable checker)

[Mario Carneiro]

but Impl.assemble doesn't, so the #eval fails

[Mac]

@Mario Carneiro I think Lean 4 is being too smart and reducing id_impl.assemble to just opaque_id.

[Mario Carneiro]

I don't see how that is legal under the execution semantics

[Tomas Skrivan]

@Mac I don't think so, try proving id_impl.assemble = (λ x : β => x)

[Mac]

@Tomas Skrivan I mean at a codegen level not a type level

[Tomas Skrivan]

Ohh, ok that might be.

[Mac]

Observe that:

set_option trace.compiler.ir true
def test :=
  id_impl.assemble 42
/--
....
def test : obj :=
  let x_1 : obj := 0;
  ret x_1
...

[Mario Carneiro]

yes, that's definitely the code of opaque_id you are seeing. I'm just not sure how the compiler decides to do that

[Mario Carneiro]

it's not like opaque_id_definition is a csimp lemma

[Mario Carneiro]

and the cast points straight to the id definition

[Mario Carneiro]

Impl.assemble is indeed the culprit for selecting the wrong implementation. Take a look that this:

set_option trace.compiler true in
def Impl.assemble {α} {a : α} : Impl a → α
  | Impl.pure impl => impl

[compiler.input] >> Impl.assemble
fun {α} {a} x =>
  match a, x with
  | impl, Impl.pure .(impl) => impl
[compiler.eta_expand] >> Impl.assemble
fun {α} {a} x =>
  match a, x with
  | impl, Impl.pure .(impl) => impl
[compiler.lcnf] >> Impl.assemble
fun {α} {a} x =>
  let _x_1 := fun impl => impl;
  match a, x with
  | impl, Impl.pure .(impl) => _x_1 impl
[compiler.cce] >> Impl.assemble
fun {α} {a} x =>
  let _x_1 := fun impl => impl;
  match a, x with
  | impl, Impl.pure .(impl) => _x_1 impl
[compiler.inline] Impl.assemble.match_1
[compiler.simp] >> Impl.assemble
fun {α} {a} x => a

[Mac]

Even wierder:

set_option trace.compiler.ir true

def id_impl : Impl (opaque_id : β → β) :=
  cast (by rw [opaque_id_eq_id]) <| Impl.pure id

/-
def id_impl._elambda_1._rarg (x_1 : @& obj) : obj :=
  inc x_1;
  ret x_1
def id_impl._elambda_1 (x_1 : ◾) : obj :=
  let x_2 : obj := pap id_impl._elambda_1._rarg._boxed;
  ret x_2
def id_impl (x_1 : ◾) (x_2 : @& obj) : obj :=
  let x_3 : obj := pap id_impl._elambda_1._rarg._boxed;
  ret x_3
def id_impl._elambda_1._rarg._boxed (x_1 : obj) : obj :=
  let x_2 : obj := id_impl._elambda_1._rarg x_1;
  dec x_1;
  ret x_2
def id_impl._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : obj := id_impl x_1 x_2;
  dec x_2;
  ret x_3
-/

[Mario Carneiro]

It is supposed to be matching on the x argument and passing the contents, and instead it takes the a argument which is the erased one

[Mario Carneiro]

the match desugaring gives a hint as to why

fun {α} {a} x =>
  match a, x with
  | impl, Impl.pure .(impl) => impl

[Mac]

@Mario Carneiro is this a bug?

[Mario Carneiro]

It's actually really tough to find a way to write the match to extract impl and not reuse a. Using casesOn directly works, though:

set_option trace.compiler true in
def Impl.assemble {α} {a : α} (i : Impl a) : α :=
  i.casesOn (motive := fun _ _ => α) fun impl => impl

[compiler.simp] >> Impl.assemble
fun α a x => x

[Mario Carneiro]

Tough to say. It seems more like an unfortunate combination of features

[Mario Carneiro]

The pattern matching syntax makes it impossible to distinguish impl from a, and after all why would you, they are equal

[Mario Carneiro]

I think the correct way to solve problems of this sort is with a first class erased type

[Mac]

@Mario Carneiro the computable/noncomputable distinction seems like a very good reason to distinguish them (also possibly implementation wise for constants).

[Mac]

also @Mario Carneiro what version of Lean 4 are you on?

[Mario Carneiro]

a relatively old one, why?

[Mac]

Your example does not work for me:

variable {β : Type} [Inhabited β]

constant opaque_id : β → β
axiom opaque_id_definition (b : β) : opaque_id b = b

inductive Impl : {α : Type _}  → (spec : α) → Type _
  | pure {α : Type u} (impl : α) : Impl impl
  -- In my real code, I have more constructors like adding a runtime check.

def Impl.assemble {α} {a : α} (i : Impl a) : α :=
  i.casesOn (motive := fun _ _ => α) fun impl => impl
/--
type mismatch
  impl
has type
  α✝ : Type ?u.210
but is expected to have type
  (fun {α_1} x x => α) impl (pure impl) : Type ?u.202
-/

[Mario Carneiro]

oops, I changed the definition of Impl, look up

[Mac]

ah

[Mario Carneiro]

@Tomas Skrivan 's version has an unnecessary universe bump

[Mario Carneiro]

turns out that where you place the colon still matters in inductives

[Tomas Skrivan]

Unnecessary in this definition of Impl. My actual definition of Impl is:

inductive Impl : {α : Type _}  → (spec : α) → Type _
  | pure  {α : Type u}
          (impl : α) : Impl impl

  | limit {α : Type u} {spec : α} [Vec α]
          (lim_spec : Nat → α)
          (n : Nat)
          (impl : Impl (lim_spec n))
          (h : spec = limit lim_spec)
          (help : String) : Impl spec

  | check {α : Type u} {spec : α} {P : Prop} [Decidable P]
          (impl : P → Impl spec)
          (help : String) : Impl spec

  | assumption {α : Type u} {spec : α} {P : Prop}
          (impl : P → Impl spec)
          (help : String) : Impl spec

[Tomas Skrivan]

This definition does not work with Impl {α : Type _} : (spec : α) → Type _

[Mac]

So a full functioning example, @Tomas Skrivan , is now:

variable {β : Type} [Inhabited β]

axiom opaque_id : β → β
axiom opaque_id_definition (b : β) : opaque_id b = b

inductive Impl.{u} {α : Type u} : (spec : α) → Type u
| pure (impl : α) : Impl impl

def Impl.assemble {α} {a : α} (i : Impl a) : α :=
  i.casesOn (motive := fun _ _ => α) fun impl => impl

theorem opaque_id_eq_id : opaque_id (β := β) = id := by
  funext x; rw [opaque_id_definition]; rfl

def id_impl : Impl (opaque_id : β → β) :=
  cast (by rw [opaque_id_eq_id]) <| Impl.pure id

#eval id_impl.assemble 42 -- 42 (yay!)

[Mario Carneiro]

To review re: erased, in lean 3 erased A is a type that is classically isomorphic to A, with functions in and out, but the function out is noncomputable, and the compiler (is supposed to) have special support for this type, such that anything of type erased A is replaced by _neutral, in the same way as proofs and types

[Mario Carneiro]

In this context, we would want Impl.assemble to have the type

def Impl.assemble {α} {a : Erased α} (i : Impl a.out) : α

[Mario Carneiro]

Then this would allow the noncomputable checker to know that elements that are passed to the a argument of Impl.assemble are allowed to be noncomputable without tainting the computation

[Mario Carneiro]

and you would get better codegen too, basically fun () () i => i

[Mario Carneiro]

@Tomas Skrivan I don't understand why your Impl type is so complex. You should have no need for anything other than the first constructor, which already expresses everything that needs to be said about "computable program that calculates a noncomputable value"

[Tomas Skrivan]

Ohh I do need the others. I want to implement numerical algorithms that implement the specification only in a certain limit. e.g. I can replace derivative by limit of finite difference. Then I want to erase the limit from implementation and continue working.

[Tomas Skrivan]

Also I will not be able to prove that certain limits actually exists. Proving that certain PDE's have solution or that their finite element discretization actually converges is super hard. I want lean to help me to create implementation of such discrete solution and then list all the assumptions I took.

[Mario Carneiro]

Another expression, less fraught because it uses a predicate for an argument (which is always trivially computable), is:

inductive Impl {α : Type _} (pred : α → Prop) : Type _
  | pure (impl : α) : pred impl → Impl pred

[Tomas Skrivan]

@Mario Carneiro Yes, I'm typing something along similar lines now :)

[Mac]

@Tomas Skrivan fyi, id_impl can be generalized as follows:

def impl {α : Type u} (a b : α) (h : a = b) : Impl a :=
  cast (by rw [h]) <| Impl.pure b

def id_impl' : Impl (opaque_id : β → β) :=
  impl opaque_id id opaque_id_eq_id

[Tomas Skrivan]

Then define axiom Erased {α} : α → Prop
and the goal would be Impl (Erased opaqud_id)

[Mario Carneiro]

This all goes much smoother:

inductive Impl {α : Type _} (pred : α → Prop) : Type _
  | pure (impl : α) : pred impl → Impl pred

axiom opaque_id : Nat → Nat
axiom opaque_id_definition (b : Nat) : opaque_id b = b

set_option trace.compiler true in
def Impl.assemble {pred : α → Prop} : Impl pred → α
  | ⟨a, _⟩ => a

theorem opaque_id_eq : opaque_id = id := by
  funext x; rw [opaque_id_definition]; rfl

def id_impl : Impl (Eq opaque_id) := ⟨id, opaque_id_eq⟩

#eval id_impl.assemble 42 -- 42

[Mario Carneiro]

Note that Erased is supposed to have the type Type u -> Type u, and ideally it should at the logic level look just like this inductive:

inductive Erased (α : Type u) : Type u
  | mk : α → Erased α

except that Erased.casesOn is magically noncomputable

[Mac]

@Mario Carneiro I think that opaque_id (and like functions) really should be a noncomputable constant -- that way you don't accidently add an inconsistent axiom or produce improper code

[Mario Carneiro]

sure, this was just for the demo

[Mac]

it wasn't a criticism XD I was more asking for conformation that the idea was reasonable :P

[Tomas Skrivan]

Mac said:

Mario Carneiro I think that opaque_id (and like functions) really should be a noncomputable constant -- that way you don't accidently add an inconsistent axiom or produce improper code

Yeah, for some time I had axiom invert : (α → β) → (β → α) and only recently realized that it is a bad idea :)

[Mario Carneiro]

indeed, noncomputable constant opaque_id : Nat → Nat works, which is different from lean 3, which knows exactly what is noncomputable and what isn't and won't take a different answer

[Tomas Skrivan]

Mario Carneiro said:

This all goes much smoother:

inductive Impl {α : Type _} (pred : α → Prop) : Type _
  | pure (impl : α) : pred impl → Impl pred

axiom opaque_id : Nat → Nat
axiom opaque_id_definition (b : Nat) : opaque_id b = b

set_option trace.compiler true in
def Impl.assemble {pred : α → Prop} : Impl pred → α
  | ⟨a, _⟩ => a

theorem opaque_id_eq : opaque_id = id := by
  funext x; rw [opaque_id_definition]; rfl

def id_impl : Impl (Eq opaque_id) := ⟨id, opaque_id_eq⟩

#eval id_impl.assemble 42 -- 42

Anyway, this looks great! I think I will experiment with it and see if I can achieve what I want.

Thanks a bunch to both of you!