From 5938dbbd14145c9b78f7645c4777f62a3fc8212c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 22 Jul 2024 16:23:28 -0700 Subject: [PATCH] fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `elab_as_elim` elaborator eagerly elaborates arguments that can help with elaborating the motive, however it does not include the transitive closure of parameters appearing in types of parameters appearing in ... types of targets. This leads to counter-intuitive behavior where arguments supplied to the eliminator may unexpectedly have postponed elaboration, causing motives to be type incorrect for under-applied eliminators such as the following: ```lean class IsEmpty (α : Sort u) : Prop where protected false : α → False @[elab_as_elim] def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := (IsEmpty.false a).elim example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α) ``` The issue is that when `isEmptyElim (α := α)` is computing its motive, the value of the postponed argument `α` is still an unassignable metavariable. With this PR, this argument is now among those that are eagerly elaborated since it appears as the type of the target `a`. This PR also contains some other fixes: * When underapplied, does unification when instantiating foralls in the expected type. * When overapplied, type checks the generalized-and-reverted expected type. * When collecting targets, collects them in the correct order. Adds trace class `trace.Elab.app.elab_as_elim`. This is a followup to #4722, which added motive type checking but exposed the eagerness issue. --- src/Lean/Elab/App.lean | 94 +++++++++---- tests/lean/elabAsElim.lean | 98 ------------- tests/lean/elabAsElim.lean.expected.out | 8 -- tests/lean/run/elabAsElim.lean | 177 ++++++++++++++++++++++++ 4 files changed, 243 insertions(+), 134 deletions(-) delete mode 100644 tests/lean/elabAsElim.lean delete mode 100644 tests/lean/elabAsElim.lean.expected.out create mode 100644 tests/lean/run/elabAsElim.lean diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 8be94e99ebc8..14c0ae70d636 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Util.FindMVar +import Lean.Util.CollectFVars import Lean.Parser.Term import Lean.Meta.KAbstract import Lean.Meta.Tactic.ElimInfo @@ -711,6 +712,12 @@ structure Context where ``` theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b ``` + For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs + argument `α` to be elaborated eagerly to create a type-correct motive. + ``` + def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ... + example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α) + ``` -/ extraArgsPos : Array Nat @@ -724,8 +731,8 @@ structure State where namedArgs : List NamedArg /-- User-provided arguments that still have to be processed. -/ args : List Arg - /-- Discriminants processed so far. -/ - discrs : Array Expr := #[] + /-- Discriminants (targets) processed so far. -/ + discrs : Array (Option Expr) /-- Instance implicit arguments collected so far. -/ instMVars : Array MVarId := #[] /-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant. -/ @@ -742,10 +749,7 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do let motiveBody ← kabstract motive discr /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/ let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr)) - let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody - unless (← isTypeCorrect motive) do - throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}" - return motive + return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody /-- If the eliminator is over-applied, we "revert" the extra arguments. -/ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) := @@ -761,7 +765,7 @@ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (E return (mkApp f val, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody) /-- -Construct the resulting application after all discriminants have bee elaborated, and we have +Construct the resulting application after all discriminants have been elaborated, and we have consumed as many given arguments as possible. -/ def finalize : M Expr := do @@ -769,29 +773,50 @@ def finalize : M Expr := do throwError "failed to elaborate eliminator, unused named arguments: {(← get).namedArgs.map (·.name)}" let some motive := (← get).motive? | throwError "failed to elaborate eliminator, insufficient number of arguments" + trace[Elab.app.elab_as_elim] "motive: {motive}" forallTelescope (← get).fType fun xs _ => do + trace[Elab.app.elab_as_elim] "xs: {xs}" let mut expectedType := (← read).expectedType + trace[Elab.app.elab_as_elim] "expectedType:{indentD expectedType}" + let throwInsufficient := do + throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}" let mut f := (← get).f if xs.size > 0 then + -- under-application, specialize the expected type using `xs` assert! (← get).args.isEmpty - try - expectedType ← instantiateForall expectedType xs - catch _ => - throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}" + for x in xs do + let .forallE _ t b _ ← whnf expectedType | throwInsufficient + unless ← fullApproxDefEq <| isDefEq t (← inferType x) do + -- We can't assume that these binding domains were supposed to line up, so report insufficient arguments + throwInsufficient + expectedType := b.instantiate1 x + trace[Elab.app.elab_as_elim] "xs after specialization of expected type: {xs}" else - -- over-application, simulate `revert` + -- over-application, simulate `revert` while generalizing the values of these arguments in the expected type (f, expectedType) ← revertArgs (← get).args f expectedType + unless ← isTypeCorrect expectedType do + throwError "failed to elaborate eliminator, after generalizing over-applied arguments, expected type is type incorrect:{indentExpr expectedType}" + trace[Elab.app.elab_as_elim] "expectedType after processing:{indentD expectedType}" let result := mkAppN f xs + trace[Elab.app.elab_as_elim] "result:{indentD result}" let mut discrs := (← get).discrs let idx := (← get).idx - if (← get).discrs.size < (← read).elimInfo.targetsPos.size then + if discrs.any Option.isNone then for i in [idx:idx + xs.size], x in xs do - if (← read).elimInfo.targetsPos.contains i then - discrs := discrs.push x - let motiveVal ← mkMotive discrs expectedType + if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then + discrs := discrs.set! tidx x + if let some idx := discrs.findIdx? Option.isNone then + -- This should not happen. + trace[Elab.app.elab_as_elim] "Internal error, missing target with index {idx}" + throwError "failed to elaborate eliminator, insufficient number of arguments" + trace[Elab.app.elab_as_elim] "discrs: {discrs.map Option.get!}" + let motiveVal ← mkMotive (discrs.map Option.get!) expectedType + unless (← isTypeCorrect motiveVal) do + throwError "failed to elaborate eliminator, motive is not type correct:{indentD motiveVal}" unless (← isDefEq motive motiveVal) do throwError "failed to elaborate eliminator, invalid motive{indentExpr motiveVal}" synthesizeAppInstMVars (← get).instMVars result + trace[Elab.app.elab_as_elim] "completed motive:{indentD motive}" let result ← mkLambdaFVars xs (← instantiateMVars result) return result @@ -819,9 +844,9 @@ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg) def setMotive (motive : Expr) : M Unit := modify fun s => { s with motive? := motive } -/-- Push the given expression into the `discrs` field in the state. -/ -def addDiscr (discr : Expr) : M Unit := - modify fun s => { s with discrs := s.discrs.push discr } +/-- Push the given expression into the `discrs` field in the state, where `i` is which target it is for. -/ +def addDiscr (i : Nat) (discr : Expr) : M Unit := + modify fun s => { s with discrs := s.discrs.set! i discr } /-- Elaborate the given argument with the given expected type. -/ private def elabArg (arg : Arg) (argExpectedType : Expr) : M Expr := do @@ -856,11 +881,11 @@ partial def main : M Expr := do let motive ← mkImplicitArg binderType binderInfo setMotive motive addArgAndContinue motive - else if (← read).elimInfo.targetsPos.contains idx then + else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then match (← getNextArg? binderName binderInfo) with - | .some arg => let discr ← elabArg arg binderType; addDiscr discr; addArgAndContinue discr + | .some arg => let discr ← elabArg arg binderType; addDiscr tidx discr; addArgAndContinue discr | .undef => finalize - | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr discr; addArgAndContinue discr + | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr tidx discr; addArgAndContinue discr else match (← getNextArg? binderName binderInfo) with | .some (.stx stx) => if (← read).extraArgsPos.contains idx then @@ -922,10 +947,12 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) let expectedType ← instantiateMVars expectedType if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available" let extraArgsPos ← getElabAsElimExtraArgsPos elimInfo + trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}" ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' { f, fType args := args.toList namedArgs := namedArgs.toList + discrs := mkArray elimInfo.targetsPos.size none } else ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' { @@ -955,19 +982,29 @@ where /-- Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`. - The idea is that the contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`. + The idea is that they contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`. -/ getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do forallTelescope elimInfo.elimType fun xs type => do - let resultArgs := type.getAppArgs + let targets := type.getAppArgs + /- Compute transitive closure of fvars appearing in the motive and the targets. -/ + let initMotiveFVars : CollectFVars.State := targets.foldl (init := {}) collectFVars + let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do + let x := xs[i]! + if elimInfo.motivePos == i || elimInfo.targetsPos.contains i || s.fvarSet.contains x.fvarId! then + return collectFVars s (← inferType x) + else + return s + /- Collect the extra argument positions -/ let mut extraArgsPos := #[] for i in [:xs.size] do let x := xs[i]! - unless elimInfo.targetsPos.contains i do - let xType ← inferType x + unless elimInfo.motivePos == i || elimInfo.targetsPos.contains i do + let xType ← x.fvarId!.getType /- We only consider "first-order" types because we can reliably "extract" information from them. -/ - if isFirstOrder xType - && Option.isSome (xType.find? fun e => e.isFVar && resultArgs.contains e) then + if motiveFVars.fvarSet.contains x.fvarId! + || (isFirstOrder xType + && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then extraArgsPos := extraArgsPos.push i return extraArgsPos @@ -1528,5 +1565,6 @@ builtin_initialize registerTraceClass `Elab.app.args (inherited := true) registerTraceClass `Elab.app.propagateExpectedType (inherited := true) registerTraceClass `Elab.app.finalize (inherited := true) + registerTraceClass `Elab.app.elab_as_elim (inherited := true) end Lean.Elab.Term diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean deleted file mode 100644 index da254e3a58ff..000000000000 --- a/tests/lean/elabAsElim.lean +++ /dev/null @@ -1,98 +0,0 @@ -inductive Vec (α : Type u) : Nat → Type u - | nil : Vec α 0 - | cons : α → Vec α n → Vec α (n+1) - -def f1 (xs : Vec α n) : Nat := - Vec.casesOn xs 0 fun _ _ => 1 - -def f2 (xs : Vec α n) : Nat := - xs.casesOn 0 -- Error insufficient number of arguments - -def f3 (x : Nat) : Nat → (Nat → Nat) → Nat := - x.casesOn - -def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 := - xs.casesOn (by intros; contradiction) (by intros; simp_arith) - -def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := - xs.casesOn (by intros; contradiction) (by intros; simp_arith) h - -def f6 (x : Nat) := - 2 * x.casesOn 0 id - -example : f6 (x+1) = 2*x := rfl - -def f7 (xs : Vec α n) : Nat := - xs.casesOn (a := 10) 0 -- Error unused named args - -def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 := - @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith) - -def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := - xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h - -example (h₁ : a = b) (h₂ : b = c) : a = c := - Eq.rec h₂ h₁.symm - -@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by - cases h₁ - assumption - -example (h₁ : a = b) (h₂ : b = c) : a = c := - subst h₁.symm h₂ - -theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => - h.rec (λ h1 => h1 hp) (λ h2 => h2 hq) - -structure Point where - x : Nat - -theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q := - Point.recOn p <| - fun z1 q => Point.recOn q $ - fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA - -inductive pos_num : Type - | one : pos_num - | bit1 : pos_num → pos_num - | bit0 : pos_num → pos_num - -inductive num : Type - | zero : num - | pos : pos_num → num - -inductive znum : Type - | zero : znum - | pos : pos_num → znum - | neg : pos_num → znum - -def pos_num.pred' : pos_num → num - | one => .zero - | bit0 n => num.pos (num.casesOn (pred' n) one bit1) - | bit1 n => num.pos (bit0 n) - -protected def znum.bit1 : znum → znum - | zero => pos .one - | pos n => pos (pos_num.bit1 n) - | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1) - -example (h : False) : a = c := - h.rec - -example (h : False) : a = c := - h.elim - -noncomputable def f : Nat → Nat := - Nat.rec 0 (fun x _ => x) - -example : ∀ x, x ≥ 0 := - Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih) - -@[elab_as_elim] -def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry - -example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct - -example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct - -example {n : Type} : {T : n} → T = T := @(Foo.induction n) diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out deleted file mode 100644 index 07450ee1193e..000000000000 --- a/tests/lean/elabAsElim.lean.expected.out +++ /dev/null @@ -1,8 +0,0 @@ -elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type: - Nat -elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a] -elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry' -elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct: - fun x => T = T -elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct: - fun x => T✝ = T✝ diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean new file mode 100644 index 000000000000..b76607fcf5d1 --- /dev/null +++ b/tests/lean/run/elabAsElim.lean @@ -0,0 +1,177 @@ +/-! +# Tests of elabAsElim elaborator and the `elab_as_elim` attribute +-/ + +-- For debugging: +-- set_option trace.Elab.app.elab_as_elim true + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → Vec α n → Vec α (n+1) + +def f1 (xs : Vec α n) : Nat := + Vec.casesOn xs 0 fun _ _ => 1 + +/-! Under-applied eliminator, and expected type isn't a pi type. -/ +/-- +error: failed to elaborate eliminator, insufficient number of arguments, expected type: + Nat +-/ +#guard_msgs in +def f2 (xs : Vec α n) : Nat := + xs.casesOn 0 + +def f3 (x : Nat) : Nat → (Nat → Nat) → Nat := + x.casesOn + +/-! Under-applied eliminator, expected type's binders do not unify with remaining arguments. -/ +/-- +error: failed to elaborate eliminator, insufficient number of arguments, expected type: + (Nat → Nat) → Nat → Nat +-/ +#guard_msgs in +def f3' (x : Nat) : (Nat → Nat) → Nat → Nat := + x.casesOn + +def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 := + xs.casesOn (by intros; contradiction) (by intros; simp_arith) + +def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := + xs.casesOn (by intros; contradiction) (by intros; simp_arith) h + +def f6 (x : Nat) := + 2 * x.casesOn 0 id + +example : f6 (x+1) = 2*x := rfl + +/-- error: failed to elaborate eliminator, unused named arguments: [a] -/ +#guard_msgs in +def f7 (xs : Vec α n) : Nat := + xs.casesOn (a := 10) 0 + +def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 := + @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith) + +def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := + xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h + +example (h₁ : a = b) (h₂ : b = c) : a = c := + Eq.rec h₂ h₁.symm + +@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by + cases h₁ + assumption + +example (h₁ : a = b) (h₂ : b = c) : a = c := + subst h₁.symm h₂ + +theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => + h.rec (λ h1 => h1 hp) (λ h2 => h2 hq) + +structure Point where + x : Nat + +theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q := + Point.recOn p <| + fun z1 q => Point.recOn q $ + fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA + +inductive pos_num : Type + | one : pos_num + | bit1 : pos_num → pos_num + | bit0 : pos_num → pos_num + +inductive num : Type + | zero : num + | pos : pos_num → num + +inductive znum : Type + | zero : znum + | pos : pos_num → znum + | neg : pos_num → znum + +def pos_num.pred' : pos_num → num + | one => .zero + | bit0 n => num.pos (num.casesOn (pred' n) one bit1) + | bit1 n => num.pos (bit0 n) + +protected def znum.bit1 : znum → znum + | zero => pos .one + | pos n => pos (pos_num.bit1 n) + | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1) + +example (h : False) : a = c := + h.rec + +example (h : False) : a = c := + h.elim + +noncomputable def f : Nat → Nat := + Nat.rec 0 (fun x _ => x) + +example : ∀ x, x ≥ 0 := + Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih) + +/-! +Tests of `@[elab_as_elim]` when the motive is not type correct. +-/ + +@[elab_as_elim] +def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry + +/-- +error: failed to elaborate eliminator, motive is not type correct: + fun x => T = T +-/ +#guard_msgs in +example {n : Type} {T : n} : T = T := Foo.induction n + +/-- +error: failed to elaborate eliminator, motive is not type correct: + fun x => T✝ = T✝ +-/ +#guard_msgs in +example {n : Type} : {T : n} → T = T := Foo.induction n + +example {n : Type} : (T : n) → T = T := Foo.induction n + +-- Disable implicit lambda +example {n : Type} : {T : n} → T = T := @(Foo.induction n) + +/-! +A "motive is not type correct" regression test. +The `isEmptyElim` was failing due to being under-applied and the named `(α := α)` argument +having postponed elaboration. This fix is that `α` now elaborates eagerly. +-/ + +class IsEmpty (α : Sort u) : Prop where + protected false : α → False + +@[elab_as_elim] +def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := + (IsEmpty.false a).elim + +def Set (α : Type u) := α → Prop +def Set.univ {α : Type _} : Set α := fun _ => True +instance : Membership α (Set α) := ⟨fun x s => s x⟩ +def Set.pi {α : ι → Type _} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := fun f => ∀ i ∈ s, f i ∈ t i + +example {α : Type u} [IsEmpty α] {β : α → Type v} (x : (a : α) → β a) (s : (i : α) → Set (β i)) : + x ∈ Set.univ.pi s := isEmptyElim (α := α) + +-- Simplified version: +example {α : Type _} [IsEmpty α] : + id (α → False) := isEmptyElim (α := α) + +/-! +From mathlib, regression test. Need to eagerly elaborate the `n ≤ m` argument to deduce `m` +before computing the motive. +-/ + +@[elab_as_elim] +def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m := + sorry + +theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : + (leRecOn n.le_refl next x : C n) = x := + sorry