of_as_true proofs

Stream: general

[Joe Hendrix]

I'm trying to build up a mental model of the efficiency of using decidable predicates to construct proofs in tactics..
Let's say I have a decidable predicate P : nat -> Prop with an instance h : decidable_pred P, and a concrete value x : nat in a tactic.
I can match on h x within the tactic monad (which I think is using the VM), and see if the prop is true or false.
However, I'd also like to have an expression for the proof of P x. I seem to be able to do that via an expression like @of_as_true _ (h x) trivial, but I think this results in the elaborator needing to reduce h x to whnf. I think of this as slower than the VM, since among other things nat will have a unary representation.
Is the above correct, and is so is there some way like reflection to have the VM (or the compiler in Lean 4) run h x and efficiently construct the needed proof?

[Mario Carneiro]

No, you can't directly produce a "fast" kernel proof from a "fast" VM function. For many common operations on nat, norm_num will produce efficient kernel proofs using VM evaluation to guide the construction, but the method is generally completely different than what the decidable instance does

[Joe Hendrix]

Good to know I'm not missing something. I think it would be useful to have some way to write a verified decision procedure in logic mode, and then be able to use it to discharge proof obligations in tactic mode.
For similar reasons, I started down the path of building up has_reflect instances for datatypes in proofs (e.g., has_reflect (and P Q)), but it's (1) a lot of work, and (2) still unclear how to support for some properties. Specifically, I have decidable (\forall (x : fin n), P x), but I'm struck on has_reflect (\forall (x : fin n), P x).

[Mario Carneiro]

hm, that's an interesting use of has_reflect. Usually we don't use has_reflect for propositions, what's the goal here?

[Mario Carneiro]

I think what you want is actually decidable, or at least semidecidable (where semidecidable p is basically option p)

[Mario Carneiro]

but you are limited by the same things as decidable proofs

[Joe Hendrix]

The idea for that use was to get the VM to produce the proof object using the decidable instance, then call has_reflect.reflect to construct the appropriate expression.

[Mario Carneiro]

decidable instances don't have proof objects

[Mario Carneiro]

they put all the computation in the kernel

[Joe Hendrix]

I'm referring to the proof object p that is the argument to decidable.is_true p

[Mario Carneiro]

You could infer decidable p, normalize it to is_true h and return h, but this is going to be almost as slow as kernel computing it

[Mario Carneiro]

you are "elaborator computing" it in this case

[Joe Hendrix]

I think I haven't been clear. I use the tactic decidable_tac below that uses uses the elaborator fairly often. As a work around to get more use of the VM, I was hoping to be able to use both decidable and has_reflect instances to get something a bit more efficient in the decidable_reflected tactic below:

meta def decidable_tac : tactic unit := do
  tgt ← tactic.target,
  tactic.apply ((`(@of_as_true) : expr) tgt),
  tactic.exact `(trivial)

meta def decidable_reflected (P:Prop) [h:decidable P] [g:has_reflect P] : tactic unit := do
  match h with
  | decidable.is_true p := tactic.exact (g p)
  | decidable.is_false q := tactic.fail "Prop false"
  end

Unfortunately, I can't actually write the necessary has_reflect instances. It seems like I would need some more support within Lean (perhaps constants that auto generated reflect instances for propositions).

[Mario Carneiro]

You can't write has_reflect instances for many propositions

[Mario Carneiro]

like or

[Mario Carneiro]

A has_reflect instance is a function that produces an expression that is a proof of p, provided p is in fact true

[Mario Carneiro]

So decidable p implies has_reflect p because you can evaluate the decidable instance and take the proof out

[Joe Hendrix]

Yep, I got and and true and thought this would work, then got stuck with forall. I tried or while writing up the example, and got the error about only being able to return a value of type P.

[Mario Carneiro]

If you know one or the other of the propositions is decidable, you can reflect an or

[Mario Carneiro]

but really decidable is the one you want, it's closed under all the operations

[Joe Hendrix]

Here was my attempt at or, but I can't match on the or value due to proof irrelevance:

meta instance or.reflect (P Q : Prop) [reflected P] [reflected Q] [hp:has_reflect P] [hq:reflected Q]
: has_reflect (P ∨ Q)
| (or.inl p) := `(or.inl).subst (hp p)
| (or.inr q) := `(or.inr).subst (hq q)

[Mario Carneiro]

exactly

[Mario Carneiro]

In a tactic, a proof value isn't very useful. It's only going to help avoid some code paths that weren't going to be exercised anyway

[Joe Hendrix]

Interesting and did not complain even though it looks like it recurses:

meta instance and.reflect (P Q : Prop) [reflected P] [reflected Q] [hp:has_reflect P] [hq:has_reflect Q]
: has_reflect (P ∧ Q)
| ⟨p,q⟩ := (`(and.intro).subst (hp p)).subst (hq q)

[Mario Carneiro]

and has large elimination because it only has one constructor

[Joe Hendrix]

The proof value is needed just so I can discharge theorems I'm proving.

[Mario Carneiro]

so if you have a function p -> expr coming from your has reflect instance, you could just as well have a function producing option expr with no proof preconditions

[Mario Carneiro]

So when you are writing a has_reflect instance you are just constructing a proof from nothing. Sometimes that's easy, like and, sometimes that requires backtracking like or, and sometimes it's really hard

[Mario Carneiro]

How are you supposed to use decidable_reflected?

[Mario Carneiro]

nothing says what P is

[Mario Carneiro]

it seems like it's mixing meta levels, and that's why you need has_reflect

[Mario Carneiro]

decidable_tac is the same as exact_dec_trivial afaict

[Joe Hendrix]

Let me work on an example. Is exact_dec_trivial in Lean standard library or mathlib?

[Mario Carneiro]

It's in mathlib, but it's literally exact dec_trivial which is core only

[Joe Hendrix]

I forget why I didn't just use exact dec_trivial -- I may not have known about it, I've used that tactic for a while now.

[Mario Carneiro]

note that dec_trivial is notation for of_as_true (by trivial); the tactic is there I think to stage the elaboration

[Mario Carneiro]

Okay, so I think I understand now what you are trying to do. You need a combination of decidable and has_reflect that produces exprs rather than proof values. You can automatically construct one by reflecting a decidable instance, but you can also produce much smarter proofs for nats and such

[Joe Hendrix]

That's right. I want proof search to run within the VM (or compiler in Lean 4), then either I can reflect on the generated proof, or maybe just have some magic constant that pretends to do it for me (say a safe version of sorry).
(edit, apparently I can't spell)

[Mario Carneiro]

@Joe Hendrix Here's an example of what I mean. Unfortunately I had to fight lean somewhat to write the instance, possibly the ergonomics of instance writing needs work.

@[class] meta inductive reflect_decidable (p : Prop)
| is_true (h : p) : /-reflected h-/ expr → reflect_decidable
| is_false (h : ¬ p) : /-reflected h-/ expr → reflect_decidable
open reflect_decidable

meta instance {p q : Prop} [reflected p] [reflected q] :
  ∀ [reflect_decidable p] [reflect_decidable q],
  reflect_decidable (p ∨ q)
| (is_true h e) _ := is_true (or.inl h) (expr.app `(@or.inl p q) e)
| _ (is_true h e) := is_true (or.inr h) (expr.app `(@or.inr p q) e)
| (is_false h₁ e₁) (is_false h₂ e₂) :=
  is_false (not_or h₁ h₂) (expr.mk_app `(@not_or p q) [e₁, e₂])

meta instance : reflect_decidable true := is_true trivial `(trivial)

open tactic
meta def by_reflection : tactic unit :=
do tgt ← target,
  let ty := `(reflect_decidable %%tgt),
  inst ← mk_instance ty,
  is_true _ e ← @tactic.eval_expr (reflect_decidable true)
    (by delta reflected; exact ty) inst,
  exact e

def ex : true ∨ true := by by_reflection
#print ex -- or.inl trivial

[Joe Hendrix]

That would kind of work. One downside is that reflect_decidable is meta. I'm interested in trying to write provably correct decision procedures, not just proof producing. I'll try this approach in the short term though.

[Mario Carneiro]

it has to be meta, because it's creating exprs

[Mario Carneiro]

this is a limitation of lean 3 tactic framework

[Mario Carneiro]

You could create objects that are like expr but not meta, and then post process at the end, but that would add some extra overhead