(lean 4) witness from (decide p && .. && decide n)

Stream: Is there code for X?

[Chris B]

Am I missing an easy way to extend this:
example (a..n : Prop) [Decidable p] .. [Decidable n] (h0 : (p && .. && n) = true) : p ∧ .. ∧ n := by

to arbitrarily long conjunctions or do I need to write a tactic?

[Mario Carneiro]

If p..n are decidable, then p ∧ .. ∧ n is also decidable, so why not use by decide! instead of a ... = true hypothesis (presumably closed by rfl)?

[Mario Carneiro]

Another alternative is to use the decide function (known as to_bool in lean 3) and of_decide_eq_true:

example [Decidable a] [Decidable b] [Decidable c]
  (h0 : decide (a ∧ b ∧ c) = true) : a ∧ b ∧ c := of_decide_eq_true h0

[Chris B]

I'm using (or at least experimenting with) what seems to be Lean 4's preference for Bool when it comes to reflection which I think is due to the kernel bool support. E.g. Nat defines Nat.ble, then the (Nat.ble a b = true <-> Nat.LE a b) lemma, then shows Decidable Nat.le using ble and the reflection lemma.

[Chris B]

I think of_decide_eq_true will do what I need in most cases, thanks for that lead.

[Chris B]

Actually I guess it depends on how the decidable instance for each prop is defined. It's interesting that Decidable (And p q) doesn't use reflection.

[Mario Carneiro]

If you really want to swap && for ∧, you can do it with a typeclass:

example [Decidable a] [Decidable b] [Decidable c]
  (h0 : decide (a ∧ b ∧ c) = true) : a ∧ b ∧ c := of_decide_eq_true h0

class ToConj (a : Prop) (b : outParam Bool) where
  eq : a ↔ b

instance ToConj.base [Decidable a] : ToConj a a := ⟨⟨decide_eq_true, of_decide_eq_true⟩⟩
instance ToConj.conj [ToConj a b] [ToConj c d] : ToConj (a ∧ c) (b && d) where
  eq := by
    rw [@ToConj.eq a, @ToConj.eq c]
    cases b <;> cases d <;> decide

theorem ToConj.out [ToConj a b] (h0 : b = true) : a := ToConj.eq.2 h0

example [Decidable a] [Decidable b] [Decidable c]
  (h0 : (a && (b && c)) = true) : a ∧ b ∧ c := ToConj.out h0

[Mario Carneiro]

Chris B said:

I'm using (or at least experimenting with) what seems to be Lean 4's preference for Bool when it comes to reflection which I think is due to the kernel bool support. E.g. Nat defines Nat.ble, then the (Nat.ble a b = true <-> Nat.LE a b) lemma, then shows Decidable Nat.le using ble and the reflection lemma.

I think Nat.ble has a special status since it is an extern function

[Mario Carneiro]

I think Nat.decLe should have approximately equivalent codegen

[Mario Carneiro]

Chris B said:

Actually I guess it depends on how the decidable instance for each prop is defined. It's interesting that Decidable (And p q) doesn't use reflection.

I don't think there would be any advantage to "using reflection" here. It's just an if statement

[Chris B]

I'll take the codegen thing and the special status of Nat.ble into account, thanks.

[Mario Carneiro]

One thing to watch out for though is that Decidable p is an actual inductive type and not a thunk for one, meaning that instDecidableAnd and friends have to be marked macroInline to avoid evaluating both sides of the && eagerly

[Chris B]

I guess the only other difference would be the size of the proof in the kernel.

[Chris B]

Ok that's also really good to know, thank you.

[Mario Carneiro]

I think that if you use decide p on some proposition p and evaluate decide p = true by rfl, the kernel proof will be short, essentially @Eq.rfl true

[Mario Carneiro]

And if you use the magic bool evaluator the kernel won't even see the intermediate proof terms

[Chris B]

This has answered a bunch of questions and probably saved me a lot of work. I've never actually inspected an exported decidable proof, but now that I think about it that makes sense since the components of the decision procedure are already in the environment.

[Mario Carneiro]

It might still be an optimistic fantasy, but ideally Decidable p decision procedures should generate code exactly like the corresponding bool functions. Once you forget the proofs the structure is exactly the same