cool paper on reification

Stream: general

[Andrew Ashworth]

just in case anybody else is interested in proofs by reflection: https://people.csail.mit.edu/jgross/personal-website/papers/2018-reification-by-parametricity-itp-draft.pdf

[Andrew Ashworth]

it's my favorite topic right now since i'm trying to teach myself how to write reflective tactics in lean

[Andrew Ashworth]

i wish i was in oxford so i could attend the workshops at ITP :|

[Andrew Ashworth]

does lean have a vm_compute equivalent?

[Mario Carneiro]

No. @Jeremy Avigad This paper relates to our discussion about proof by #eval

[Simon Hudon]

I had a conversation with @Mario Carneiro a while back on proofs by reflection. He was pointing out to me that they are not as beneficial in Lean as they are in Coq because of some details of computation in the kernel

[Simon Hudon]

I don't remember which detail that was

[Mario Carneiro]

It's possible to do proof by reflection using the kernel for computation, but it's not very fast

[Mario Carneiro]

doing proof by reflection using the VM is not supported (directly)

[Mario Carneiro]

but you can use tactics, computing in the VM, to craft appropriate theorems as certificates for the kernel

[Andrew Ashworth]

is there an example of that in lean? I think the idea of verified decision procedures is very appealing theoretically

[Mario Carneiro]

norm_num and ring use this latter strategy

[Mario Carneiro]

cooper uses kernel reflection, and vm_cooper uses "tactic reflection"

[Andrew Ashworth]

and in lean 4, i think we will be able to extract tactics and use them?

[Mario Carneiro]

sure, that's one thing compilation should allow

[Andrew Ashworth]

not tactics, i mean regular function defs

[Andrew Ashworth]

so we could extract the check_is_even program as described in the paper and have it run in C++

[Mario Carneiro]

You can #eval check_is_even currently

[Mario Carneiro]

to run in the VM

[Mario Carneiro]

or you can #reduce check_is_even to run in the kernel

[Andrew Ashworth]

but, in a sense, we can't reason about vm evaluation, it's outside lean, is my current understanding

[Andrew Ashworth]

if there was a #eval that produced exprs we could though

[Mario Carneiro]

no but we can trust the results

[Mario Carneiro]

like if we evaluate a bool expr and get tt we believe the same should hold true of reduce

[Mario Carneiro]

The reasoning would go into the definition of the function being evaluated itself

[Andrew Ashworth]

reasoning would go into the definition? do you have a concrete example? I don't quite follow. As I understand it the kernel is quite strict. If we use nat, it will reduce everything strictly using the zero / succ nat representation. However, vm evaluation might use a bignum library for speed. How can we say their behavior is equivalent?
(maybe I should just be reading more about reflection / I don't understand how Lean uses GMP)

[Mario Carneiro]

The assumption, the trust, goes into assuming that the VM respects the lean model. You verify the lean model

[Andrew Ashworth]

ah, gotcha

[Mario Carneiro]

But that's not much different from assuming the kernel is correctly implemented in C++. You expand your trust level a bit and get fast evaluation

[Andrew Ashworth]

it's interesting to me that reflection is slow because generating the reified syntax and reducing the output of the interpretation function are such huge constant overheads. I would've guessed that the manipulations you might do on the AST you create would've been a bigger deal in practice for most problems

[Andrew Ashworth]

well, you weren't kidding about kernel computation

inductive is_even : ℕ → Prop
| zero : is_even 0
| ssuc : ∀ n, is_even n → is_even (nat.succ (nat.succ n))

meta def prove_even : tactic unit := `[repeat {constructor}]

example : is_even 2000 := by do timetac "" prove_even

def check_is_even : ℕ → bool
| nat.zero := tt
| (nat.succ nat.zero) := ff
| (nat.succ (nat.succ n')) := check_is_even n'

local attribute [elab_as_eliminator] nat.case_strong_induction_on
theorem cie_sound : ∀ n, check_is_even n = tt → is_even n :=
λ n, nat.case_strong_induction_on n
  (λ h, is_even.zero)
  (λ n', nat.rec_on n'
    (λ h₁ h₂, have h₃ : check_is_even 1 = ff, from rfl, by contradiction)
    (λ m h₁ h₂ h₃, is_even.ssuc _ ((h₂ m) (nat.le_succ m) h₃)))

example : is_even 2000 := by do timetac "" `[exact cie_sound 2000 rfl]