From 313e313818fbf44c3e9fb9f52e901b927cf361f2 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 13 Oct 2024 12:06:52 +0200
Subject: [PATCH] =?UTF-8?q?feat:=20DiscrTree:=20index=20the=20domain=20of?=
 =?UTF-8?q?=20`=E2=88=80`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It bothered me that inferring instances of the shape `Decidable (∀ (x : Fin _), _)`
will go linearly through all instances of that shape, even those that are
about `∀ (x : Nat), …`. And that  `Decidable (∃ (x : Fin _), _)` gets better
indexing than `Decidable (∀ (x : Fin _), _)`.

Judging from code comments, the discr tree used to index arrow types
with two arguments (domain and body), and that led to bugs due to the
dependency, so the arguments were removed. But it seems that indexing
the domain is completely simple and innocent.

So let’s see what happens…

Mostly only insignificant perf improvements, unfortunately (~Mathlib.Data.Matroid.IndepAxioms — instructions -11.4B, overall build instructions -0.097 %):
http://speed.lean-fro.org/mathlib4/compare/dd333cc1-fa26-42f2-96c6-b0e66047d0b6/to/6875ff8f-a17c-431d-8b8b-2f00799be794

This is just a small baby step compared to the more invasive improvements
done in the [`RefinedDiscrTree` by  J. W. Gerbscheid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp/RefinedDiscrTree.html) in mathlib.
---
 src/Lean/Meta/DiscrTree.lean | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 40a2a1897826..ad1ec8021260 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -76,7 +76,7 @@ def Key.format : Key → Format
   | .const k _       => Std.format k
   | .proj s i _      => Std.format s ++ "." ++ Std.format i
   | .fvar k _        => Std.format k.name
-  | .arrow           => "→"
+  | .arrow           => "∀"
 
 instance : ToFormat Key := ⟨Key.format⟩
 
@@ -113,7 +113,8 @@ where
       mkApp m!"{mkFVar fvarId}" (← goN nargs) parenIfNonAtomic
     | .proj _ i nargs =>
       mkApp m!"{← go}.{i+1}" (← goN nargs) parenIfNonAtomic
-    | .arrow => return "<arrow>"
+    | .arrow =>
+      mkApp m!"∀ " (← goN 1) parenIfNonAtomic
     | .star => return "_"
     | .other => return "<other>"
     | .lit (.natVal v) => return m!"{v}"
@@ -129,21 +130,15 @@ def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a
   /-
-  Remark: `.arrow` used to have arity 2, and was used to encode non-dependent arrows.
-  However, this feature was a recurrent source of bugs. For example, a theorem about
-  a dependent arrow can be applied to a non-dependent one. The reverse direction may
-  also happen. See issue #2835.
-  ```
-  -- A theorem about the non-dependent arrow `a → a`
-  theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
-
-  -- can be applied to the dependent one `(h : P a) → P (f h)`.
-  example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
-    simp only [imp_self']
-  ```
-  Thus, we now index dependent and non-dependent arrows using the key `.arrow` with arity 0.
+  Remark: `.arrow` used to have arity 2, and was used to encode only **non**-dependent
+  arrows. However, this feature was a recurrent source of bugs. For example, a
+  theorem about a dependent arrow can be applied to a non-dependent one. The
+  reverse direction may also happen. See issue #2835. Therefore, `.arrow` was made
+  to have arity 0. But this throws away easy to use information, and makes it so
+  that ∀ and ∃ behave quite differently. So now `.arrow` at least indexes the
+  domain of the forall (whether dependent or non-dependent).
   -/
-  | .arrow      => 0
+  | .arrow      => 1
   | .proj _ _ a => 1 + a
   | _           => 0
 
@@ -422,7 +417,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
         return (.other, todo)
       else
         return (.star, todo)
-    | .forallE .. => return (.arrow, todo)
+    | .forallE _n d _ _ =>
+      return (.arrow, todo.push d)
     | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
@@ -581,7 +577,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .proj s i a .. =>
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE .. => return (.arrow, #[])
+  | .forallE _ d _ _ => return (.arrow, #[d])
   | _ => return (.other, #[])
 
 private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=