Quoting proofs with `ToExpr`

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

If I have n : Nat, then I can write toExpr n : Expr to quote it into a kernel term. Suppose I also have a proof h : n = 2. Can I somehow quote it to obtain pf : Q($(toExpr n) = 2)?

[Aaron Liu]

The only way I know of doing this is to hard-code the proof.

[Aaron Liu]

since proofs are erased in the compiler

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I see what you're saying, maybe my question doesn't even make sense; it would be asking that toExpr produce an Expr from a runtime value that's effectively Unit.

[Aaron Liu]

What's your application?

[Aaron Liu]

For h : n = 2 the proof that $(toExpr n) = 2 is just rfl

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The actual use case is more complicated. I have some type, Foo, and a Foo-checking function partial def check (a : Foo) : Except String { _u : Unit // GoodFoo a }. Then I run it at the meta-level (in an elaborator), and if it succeeds, I wish to produce a proof in Q(GoodFoo $(toExpr a)). (Foo is the syntax of a type theory and check is a typechecker, but I think that doesn't matter here.)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

(Thinking about it further, being able to reflect proofs like this is some analogue of nativeDecide, since the original checking runs in the interpreter.)

[Aaron Liu]

This is just decide

[Aaron Liu]

Write a Decidable instance

[Aaron Liu]

Actually, is this decide? It might be partial.

[Aaron Liu]

hmmmmmmmm

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Aaron Liu said:

Actually, is this decide? It might be partial.

Sorry yeah, it's partial def check.

[Aaron Liu]

oh no

[Aaron Liu]

so you can't prove anything at all?

[Aaron Liu]

I have an idea! You can make check return the Expr instead of the useless proof.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Aaron Liu said:

I have an idea! You can make check return the Expr instead of the useless proof.

Indeed this would be the standard approach, I just really didn't want to do that (because it makes the code of check strictly less readable); but I may have to.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

So what such a reflection principle is really asserting is that all the ToExpr implementations are correct, at least on GoodFoos. In certain cases we can prove this directly - or more accurately, construct Q(GoodFoo $(toExpr a)) - without changing check itself. I think this can only work if the proof term is constructible by recursion on a only (so on data, not on a proof), which may need some inversion principles.

inductive GoodNat : Nat → Prop where
  | one : GoodNat 1
  | succ {n} : GoodNat n → GoodNat (n + 1)

theorem GoodNat.pred {n} : GoodNat (n + 2) → GoodNat (n + 1)
  | succ h => h

def GoodNat.toExpr {n} (h : GoodNat n) : let n : Q(Nat) := toExpr n; Q(GoodNat $n) :=
  match n with
  | 1 => q(.one)
  | _+2 =>
    let e := GoodNat.pred h |>.toExpr
    q(.succ $e)

[Kyle Miller]

(Something that's probably not useful for you, but I was reminded of this recently: sometimes having a runtime value is enough to synthesize a proof, though probably most cases are fairly trivial. The only one that comes to mind is docs#instToExprFin)