# Zulip Chat Archive

## Stream: general

### Topic: of_as_true proofs

#### Joe Hendrix (Dec 28 2018 at 02:40):

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 (Dec 28 2018 at 04:12):

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 (Dec 28 2018 at 06:06):

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 (Dec 28 2018 at 06:10):

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 (Dec 28 2018 at 06:11):

I think what you want is actually `decidable`

, or at least `semidecidable`

(where `semidecidable p`

is basically `option p`

)

#### Mario Carneiro (Dec 28 2018 at 06:11):

but you are limited by the same things as `decidable`

proofs

#### Joe Hendrix (Dec 28 2018 at 06:11):

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 (Dec 28 2018 at 06:12):

decidable instances don't have proof objects

#### Mario Carneiro (Dec 28 2018 at 06:12):

they put all the computation in the kernel

#### Joe Hendrix (Dec 28 2018 at 06:13):

I'm referring to the proof object `p`

that is the argument to `decidable.is_true p`

#### Mario Carneiro (Dec 28 2018 at 06:14):

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 (Dec 28 2018 at 06:14):

you are "elaborator computing" it in this case

#### Joe Hendrix (Dec 28 2018 at 06:32):

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 (Dec 28 2018 at 06:43):

You can't write `has_reflect`

instances for many propositions

#### Mario Carneiro (Dec 28 2018 at 06:43):

like `or`

#### Mario Carneiro (Dec 28 2018 at 06:46):

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 (Dec 28 2018 at 06:47):

So `decidable p`

implies `has_reflect p`

because you can evaluate the decidable instance and take the proof out

#### Joe Hendrix (Dec 28 2018 at 06:48):

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 (Dec 28 2018 at 06:49):

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

#### Mario Carneiro (Dec 28 2018 at 06:49):

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

#### Joe Hendrix (Dec 28 2018 at 06:51):

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 (Dec 28 2018 at 06:51):

exactly

#### Mario Carneiro (Dec 28 2018 at 06:51):

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 (Dec 28 2018 at 06:51):

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 (Dec 28 2018 at 06:51):

`and`

has large elimination because it only has one constructor

#### Joe Hendrix (Dec 28 2018 at 06:52):

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

#### Mario Carneiro (Dec 28 2018 at 06:53):

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 (Dec 28 2018 at 06:54):

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 (Dec 28 2018 at 06:56):

How are you supposed to use `decidable_reflected`

?

#### Mario Carneiro (Dec 28 2018 at 06:56):

nothing says what `P`

is

#### Mario Carneiro (Dec 28 2018 at 06:57):

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

#### Mario Carneiro (Dec 28 2018 at 06:57):

`decidable_tac`

is the same as `exact_dec_trivial`

afaict

#### Joe Hendrix (Dec 28 2018 at 06:58):

Let me work on an example. Is `exact_dec_trivial`

in Lean standard library or mathlib?

#### Mario Carneiro (Dec 28 2018 at 06:59):

It's in mathlib, but it's literally `exact dec_trivial`

which is core only

#### Joe Hendrix (Dec 28 2018 at 07:00):

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 (Dec 28 2018 at 07:02):

note that `dec_trivial`

is notation for `of_as_true (by trivial)`

; the tactic is there I think to stage the elaboration

#### Mario Carneiro (Dec 28 2018 at 07:06):

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 (Dec 28 2018 at 07:08):

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 (Dec 28 2018 at 07:34):

@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 (Dec 28 2018 at 09:04):

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 (Dec 28 2018 at 09:32):

it has to be meta, because it's creating `expr`

s

#### Mario Carneiro (Dec 28 2018 at 09:33):

this is a limitation of lean 3 tactic framework

#### Mario Carneiro (Dec 28 2018 at 09:34):

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

Last updated: Aug 03 2023 at 10:10 UTC