How to simplify inner let?

Stream: general

[Michael Burge]

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]

You can't prove anything about a partial def

[Michael Burge]

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

[Michael Burge]

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]

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]

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]

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

[Mario Carneiro]

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

[Michael Burge]

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]

It should be easy to prove termination since next is strictly-decreasing.

[Reid Barton]

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]

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]

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]

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]

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]

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]

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]

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]

if h : p then x else y is syntax for dite which is just a bit further down in that file.

[Michael Burge]

So the macro for if h : C generates a pair of functions that receives C or Not C in the context, while if Cgenerates 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]

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]

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]

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

[Sebastian Ullrich]

termination_by takes any WellFoundedRelation; it's measure that reduces it to finite measures

[Mario Carneiro]

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]

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.