1
$\begingroup$

My understanding of dependent typing is that it allows typing functions to constrain their behavior. Say I have a Lean object

def halve  : ∀ a : xnat, ∃ half : xnat, add half half = a ∨ succ (add half half) = a := ...

to my eye the definition describes how to compute half. But if I try to run the function like halve zero, I get a Exists instance and don't know how to get the value from it.

Can I run this as a function (e.g. called by main), or can I make a different function that does this and is typed in a similar way?

$\endgroup$

1 Answer 1

5
$\begingroup$

It comes down to how you interpret your questions.

Can I run this as a function?

The main issue in this case is that in Lean uses Prop, and Prop in Lean erases the proof, effectively erasing the instructions on how you can get to the result. For a given a, just knowing there is a proof doesn't tell us the value of half we use. So it isn't possible to "run" the proof as a function. This "proof-irrelevance" is because Lean adopts the rule that two proofs of the same proposition are equal.

In some other dependent-type theories, which don't have that rule, it could be possible to extract the underlying function. (It is important here that one doesn't use axioms like the axiom of choice. This would ruin computation.)

Can I make a different function?

Yes, there are a number of ways in Lean which you can get what you want.

Seperate function and theorem

If the half function is independently important to you, then you can just define it, and separately prove it satisfies the property you want. This is the standard approach.

def half_aux : Nat -> Bool × Nat
| 0 => (true, 0)
| n+1 => match half_aux n with
  -- n is even
  | (true, m) => (false, m)
  -- n is odd
  | (false, m) => (true, m + 1)

def half (a : Nat) : Nat := (half_aux a).2

theorem half_is_half (a : Nat) : (half a) + (half a) = a ∨ (half a) + (half a) + 1 = a := sorry

Replace with Σ'.

Instead of , you can use PSigma, denoted Σ', which is a Type-valued version of which retains the relevant information. (The Σ' version allows the dependent second value to have a Prop sort, while the most common Sigma, Σ, doesn't.) By restricting the output to the first argument, we get the desired function.

def half_exists (a : Nat) : Σ' half : Nat, half + half = a ∨ half + half + 1 = a := sorry

def half (a : Nat) : Nat := (half_exists a).1

Further, if your construction is sufficiently computable, e.g. doesn't use the axiom of choice, then you can compute with your function. (And even the axiom of choice is used in half_exists in some essential way to choose the witness, you can still use half as a non-computable mathematical function in Lean.)

Classical.choose

If you don't care about computation, then you can use Classical.choose, a form of the axiom of choice, to get your function. Note, by using choice, you lose any ability to compute the function (and we mark it with noncomputable to signify that).

theorem half_exists  (a : Nat) : ∃ half : Nat, half + half = a ∨ half + half + 1 = a := sorry

noncomputable
def half (a : Nat) : Nat := Classical.choose (half_exists a)

Unique choice (not in Lean)

Notice, in this particular case there is only one possible value half satisfying half_exists. In some type theories, there is a weaker form of choice called "unique choice" which allows you to construct a function when you can prove it uniquely exists. In some of those type theories, like cubical type theory, it is even possible to compute with said extracted function. (Unique choice is not provable in Lean, except through the axiom of choice.)

Nat.find

If you have the proof that half exists, then for each a we can compute half a just by searching for the smallest number satisfying the predicate. So half : Nat -> Nat is a computable function. We are using that Nat is enumerable, and all the functions and relations are computable and decidable, respectively. There is a tool for exactly this in Lean, called Nat.find which is a computable version of the axiom of choice.

import Mathlib

...

def half (a : Nat) : Nat := Nat.find (half_exists a)

#eval half 2024  -- 1012

But note, the run time is at least O(n) since it searches starting from 0 every time, so it isn't very practical.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.