# Zulip Chat Archive

## Stream: general

### Topic: How to simplify inner let?

#### Michael Burge (Dec 09 2021 at 18:06):

How do I simplify the inner recursive `let`

in this lean4 snippet?

```
def evenq (n: Nat) : Bool := Nat.mod n 2 = 0
partial def pack (n: Nat) : List Nat :=
let next (n: Nat) := n / 2;
let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
match n with
| Nat.zero => List.cons acc accs
| n => match evenq n with
| true => loop (next n) 0 (List.cons acc accs)
| false => loop (next n) (acc+1) accs
loop n 0 []
#eval pack 0
theorem pack_zero_nonempty : pack 0 ≠ [] := by
simp [pack]
intro
simp [pack.loop] -- Doesn't simplify
```

Ideally I'd want to run the tactic equivalent of #eval to get `[0] \neq []`

as my goal, but `simpl`

or `delta`

don't seem to be able to reduce `pack.loop`

.

#### Mario Carneiro (Dec 09 2021 at 18:12):

You can't prove anything about a `partial def`

#### Michael Burge (Dec 09 2021 at 18:14):

Is that because the type-checker is guaranteed to complete in finite time, and "just run it" can run for unbounded time?

#### Michael Burge (Dec 09 2021 at 18:19):

It seems like `#eval pack 0`

terminating with value `[0]`

should constitute a proof that `pack 0 = [0]`

. Why is the calculation `#eval`

can do inaccessible to proofs?

#### Mario Carneiro (Dec 09 2021 at 18:23):

`partial def`

uses a `constant`

to shield the unsafe implementation details of unbounded evaluation from the kernel. This is needed because you can prove false using general recursion: `unsafe def foo : false := foo`

#### Mario Carneiro (Dec 09 2021 at 18:24):

a side effect of this is that the kernel loses the ability to prove any fact about the def except that it is type correct

#### Mario Carneiro (Dec 09 2021 at 18:25):

In principle, the "just run it" method could be used to derive proofs, but lean isn't set up like that

#### Mario Carneiro (Dec 09 2021 at 18:28):

The way to write recursive definitions that have provable properties is to use structural recursion or `termination_by`

#### Michael Burge (Dec 09 2021 at 18:29):

How do you specify a termination proof on the `let rec`

using `termination_by`

? I saw examples in the test suite for `def`

and `mutual`

declarations, but not for `let rec`

.

#### Michael Burge (Dec 09 2021 at 18:31):

It should be easy to prove termination since `next`

is strictly-decreasing.

#### Reid Barton (Dec 09 2021 at 18:35):

Michael Burge said:

How do you specify a termination proof on the

`let rec`

using`termination_by`

?

Don't know if there is a better way but one option is always to float out `loop`

to a top-level definition

#### Mario Carneiro (Dec 09 2021 at 18:42):

```
def evenq (n: Nat) : Bool := Nat.mod n 2 = 0
theorem half_lt (n : Nat) : n ≠ 0 → n / 2 < n := sorry
def pack (n: Nat) : List Nat :=
let next (n: Nat) := n / 2
have next_lt {n} : n ≠ 0 → next n < n := half_lt n
let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
if h : n = 0 then
List.cons acc accs
else
match evenq n with
| true => have := next_lt h; loop (next n) 0 (List.cons acc accs)
| false => have := next_lt h; loop (next n) (acc+1) accs
loop n 0 []
termination_by measure (·.2.2.1)
decreasing_by assumption
```

#### Mario Carneiro (Dec 09 2021 at 18:43):

it looks like it's not necessary to float out the definition, `termination_by`

syntax seems to be pretty flexible to allow choosing nested functions to work on

#### Mario Carneiro (Dec 09 2021 at 18:52):

As far as I can tell, this generates exactly the same IR too, except that it has an additional dummy argument for the use of the closure argument `next_lt`

in `loop`

#### Michael Burge (Dec 09 2021 at 19:05):

I would've expected `if h : n = 0`

to fail because `n = 0`

is `Prop`

not `Bool`

, and I don't see it in the Language Manual or defined in the Term parser. I also see ` if k == ``Lean.Parser.Term.letPatDecl then`

when searching the `lean4`

repository and `==`

evaluates to a `Bool`

, so it seems reusable for both `Prop`

and `Bool`

.

Is there a better reference for Lean syntax than the unit tests in the `lean4`

repo, that would include the semantics for things like `if`

?

#### Yakov Pechersky (Dec 09 2021 at 19:07):

Since your condition in the if statement is about equality of naturals, that is decidable equality, so it can compute. Decidability is the ability of "computing" a bool from a proof.

#### Michael Burge (Dec 09 2021 at 19:47):

So there's probably a library typeclass or something for types that are decidable, and `if`

desugars to it(maybe it's a macro?). And decidable in Lean wouldn't mean computable(because `BusyBeaver(n)`

for sufficiently large n would be `Nat`

but uncomputable even in principle), but something like "allows case analysis in classic logic".

It looks like if is a macro defined in terms of `ite`

which I see references to in C++ code, so it's built-in to the core language. There are also tactics that generate a reference to `of_decide_eq_true`

in the `Decidable`

typeclass.

So `if`

eventually compiles down to a reference to `of_decide_eq_true`

, which is proven for any type implementing `Decidable`

.

#### Michael Burge (Dec 09 2021 at 19:49):

Correction: That C++ code looks like it is generated from the .lean code to allow bootstrapping, so is a red herring. `if`

is only a macro that generates a typeclass constraint in pure lean

#### Reid Barton (Dec 09 2021 at 19:50):

`if h : p then x else y`

is syntax for `dite`

which is just a bit further down in that file.

#### Michael Burge (Dec 09 2021 at 20:02):

So the macro for `if h : C`

generates a pair of functions that receives `C`

or `Not C`

in the context, while `if C`

generates a pair of values unconditionally. In the proof that Mario wrote for me, `half_lt`

uses `n ≠ 0`

which is the `else`

condition of the `if h: n = 0`

, so this is why the `h : C`

syntax was used(because the else case consumes `Not C`

).

And now I notice `h`

is passed explicitly to `next_lt`

.

#### Michael Burge (Dec 09 2021 at 20:09):

`terminates_by`

takes a function that maps the type to `Nat`

(so it's probably theoretically impossible to do transfinite induction proofs with Lean). The centerdot is probably the "current context", and `.2.2.1`

are unwrapping pairs to get to the `n`

that is proven to be decreasing.

Why can't it refer to `n`

directly, since it's attached to `pack`

that has `n`

in scope?

#### Reid Barton (Dec 09 2021 at 20:33):

Michael Burge said:

(so it's probably theoretically impossible to do transfinite induction proofs with Lean)

It's definitely possible, maybe not using the `terminates_by`

syntax though.

#### Sebastien Gouezel (Dec 09 2021 at 20:41):

See for instance docs#besicovitch.tau_package.index for an example of a construction by transfinite induction.

#### Sebastian Ullrich (Dec 09 2021 at 20:59):

`termination_by`

takes any `WellFoundedRelation`

; it's `measure`

that reduces it to finite measures

#### Mario Carneiro (Dec 09 2021 at 21:38):

Michael Burge said:

`terminates_by`

takes a function that maps the type to`Nat`

(so it's probably theoretically impossible to do transfinite induction proofs with Lean). The centerdot is probably the "current context", and`.2.2.1`

are unwrapping pairs to get to the`n`

that is proven to be decreasing.Why can't it refer to

`n`

directly, since it's attached to`pack`

that has`n`

in scope?

(As Sebastian says, you can prove more complex recursions if you don't use `measure`

, but in this case we just want a nat so it's fine to use it here.) `measure`

takes a function from the original domain (which is an autogenerated sigma type over all the arguments) to nat, and `(·.2.2.1)`

is notation for a lambda that picks out the right argument here. (`n`

is the third argument, because `next`

and `next_lt`

are captured variables which come first.)

It can't refer to `n`

directly because `termination_by`

isn't in scope of anything - it is elaborated in the empty context, although one could imagine a variation on the syntax that automatically untuples the sigma type and gives all the variables the original names so that they appear to still be in scope. But fundamentally, the proof of termination has to be separate from the lambda that gives the term's definition, because it's talking about all the definition's values, not just the "current" one for the in-scope values of the inputs.

#### Mario Carneiro (Dec 09 2021 at 21:45):

Michael Burge said:

And decidable in Lean wouldn't mean computable(because

`BusyBeaver(n)`

for sufficiently large n would be`Nat`

but uncomputable even in principle), but something like "allows case analysis in classic logic".

While this is true, in practice usually `Decidable p`

means that `p`

has an actual decision procedure. In the case of uncomputable decision procedures, this is indicated by an instance of `Decidable p`

that is marked `noncomputable`

. This does come up in one important case: in classical logic, when computation is not important, one can use (the lean 4 equivalent of) docs#classical.dec to nonconstructively prove that every proposition has a decision procedure (namely, one of the two functions `return true`

and `return false`

); this allows you to put anything in an `if`

statement, but the resulting definitions will themselves be marked `noncomputable`

, reflecting that the definition has no code generation associated to it and `#eval`

will not work.

Last updated: Dec 20 2023 at 11:08 UTC