From 8f899bf5bd04cc854e30fc29e75390f32e95883a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 10 Sep 2024 08:36:38 +0200 Subject: [PATCH] doc: code comments about reflection support (#5235) I found that the kernel has special support for `e =?= true`, and will in this case aggressively whnf `e`. This explains the following behavior (for a `sqrt` function with fuel): ```lean theorem foo : sqrt 100000000000000000002 == 10000000000 := rfl -- fast theorem foo : sqrt 100000000000000000002 = 10000000000 := rfl -- slow theorem foo : sqrt 100000000000000000002 = 10000000000 := by decide -- fast ``` The special support in the kernel only applies for closed `e` and `true` on the RHS. It could be generlized (also open terms, also `false`, other data type's constructors, different orientation). But maybe I should wait for evidence that this generaziation really matters, or whether all applications (proof by reflection) can be made to have this form. --- src/Lean/Elab/Tactic/ElabTerm.lean | 3 ++- src/kernel/type_checker.cpp | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index ca9eae6138..0134dbfd16 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -405,7 +405,8 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do if r.isAppOf ``isTrue then -- Success! -- While we have a proof from reduction, we do not embed it in the proof term, - -- and instead we let the kernel recompute it during type checking from the following more efficient term. + -- and instead we let the kernel recompute it during type checking from the following more + -- efficient term. The kernel handles the unification `e =?= true` specially. let rflPrf ← mkEqRefl (toExpr true) return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf else diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 0a07d45880..54b7192dcc 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -1072,7 +1072,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) { // Very basic support for proofs by reflection. If `t` has no free variables and `s` is `Bool.true`, // we fully reduce `t` and check whether result is `s`. - // TODO: add metadata to control whether this optimization is used or not. + // This code path is taken in particular when using the `decide` tactic, which produces + // proof terms of the form `Eq.refl true : decide p = true`. if (!has_fvar(t) && is_constant(s, *g_bool_true)) { if (is_constant(whnf(t), *g_bool_true)) { return true;