From 69c71f6476f4204c5e83bee74f8d51725e836d14 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 29 Jul 2024 12:18:47 -0700 Subject: [PATCH] fix: make `elabAsElim` aware of explicit motive arguments (#4817) Some eliminators (such as `False.rec`) have an explicit motive argument. The `elabAsElim` elaborator assumed that all motives are implicit. If the explicit motive argument is `_`, then it uses the elab-as-elim procedure, and otherwise it falls back to the standard app elaborator. Furthermore, if an explicit elaborator is not provided, it falls back to treating the elaborator as being implicit, which is convenient for writing `h.rec` rather than `h.rec _`. Rationale: for `False.rec`, this simulates it having an implicit motive, and also motives are generally not going to be available in the expected type. Closes #4347 --- src/Lean/Elab/App.lean | 44 ++++++++++++++++++++++++++------ tests/lean/276.lean | 2 +- tests/lean/276.lean.expected.out | 5 ++-- tests/lean/run/1697.lean | 2 +- tests/lean/run/elabAsElim.lean | 11 ++++++++ tests/lean/run/emptyLcnf.lean | 2 +- 6 files changed, 52 insertions(+), 14 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index dfd836c73c..4c49d4c792 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -743,7 +743,7 @@ structure State where abbrev M := ReaderT Context $ StateRefT State TermElabM /-- Infer the `motive` using the expected type by `kabstract`ing the discriminants. -/ -def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do +def mkMotive (discrs : Array Expr) (expectedType : Expr) : MetaM Expr := do discrs.foldrM (init := expectedType) fun discr motive => do let discr ← instantiateMVars discr let motiveBody ← kabstract motive discr @@ -878,7 +878,16 @@ partial def main : M Expr := do main let idx := (← get).idx if (← read).elimInfo.motivePos == idx then - let motive ← mkImplicitArg binderType binderInfo + let motive ← + match (← getNextArg? binderName binderInfo) with + | .some arg => + /- Due to `Lean.Elab.Term.elabAppArgs.elabAsElim?`, this must be a positional argument that is the syntax `_`. -/ + elabArg arg binderType + | .none | .undef => + /- Note: undef occurs when the motive is explicit but missing. + In this case, we treat it as if it were an implicit argument + to support writing `h.rec` when `h : False`, rather than requiring `h.rec _`. -/ + mkImplicitArg binderType binderInfo setMotive motive addArgAndContinue motive else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then @@ -970,15 +979,34 @@ where unless (← shouldElabAsElim declName) do return none let elimInfo ← getElimInfo declName forallTelescopeReducing (← inferType f) fun xs _ => do - if h : elimInfo.motivePos < xs.size then - let x := xs[elimInfo.motivePos] + /- Process arguments similar to `Lean.Elab.Term.ElabElim.main` to see if the motive has been + provided, in which case we use the standard app elaborator. + If the motive is explicit (like for `False.rec`), then a positional `_` counts as "not provided". -/ + let mut args := args.toList + let mut namedArgs := namedArgs.toList + for x in xs[0:elimInfo.motivePos] do let localDecl ← x.fvarId!.getDecl - if findBinderName? namedArgs.toList localDecl.userName matches some _ then + match findBinderName? namedArgs localDecl.userName with + | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName + | none => if localDecl.binderInfo.isExplicit then args := args.tailD [] + -- Invariant: `elimInfo.motivePos < xs.size` due to construction of `elimInfo`. + let some x := xs[elimInfo.motivePos]? | unreachable! + let localDecl ← x.fvarId!.getDecl + if findBinderName? namedArgs localDecl.userName matches some _ then + -- motive has been explicitly provided, so we should use standard app elaborator + return none + else + match localDecl.binderInfo.isExplicit, args with + | true, .expr _ :: _ => -- motive has been explicitly provided, so we should use standard app elaborator return none - return some elimInfo - else - return none + | true, .stx arg :: _ => + if arg.isOfKind ``Lean.Parser.Term.hole then + return some elimInfo + else + -- positional motive is not `_`, so we should use standard app elaborator + return none + | _, _ => return some elimInfo /-- Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`. diff --git a/tests/lean/276.lean b/tests/lean/276.lean index bae43741a8..aeae650d0e 100644 --- a/tests/lean/276.lean +++ b/tests/lean/276.lean @@ -5,5 +5,5 @@ set_option pp.all true in #check fun {α : Sort v} => PEmpty.rec (fun _ => α) -- but `def` doesn't work --- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec' +-- error: code generator does not support recursor 'PEmpty.rec' yet def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α) diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out index 35e51a5f70..cea833efcd 100644 --- a/tests/lean/276.lean.expected.out +++ b/tests/lean/276.lean.expected.out @@ -1,3 +1,2 @@ -276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available -fun {α : Sort v} => @?m α : {α : Sort v} → @?m α -276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available +fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α +276.lean:9:4-9:16: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index 23534e4551..bb8d15715c 100644 --- a/tests/lean/run/1697.lean +++ b/tests/lean/run/1697.lean @@ -8,7 +8,7 @@ error: cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash). -/ #guard_msgs in -#eval show Nat from False.rec (by decide) +#eval show Nat from False.elim (by decide) /-- warning: declaration uses 'sorry' diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean index b76607fcf5..d3585e3750 100644 --- a/tests/lean/run/elabAsElim.lean +++ b/tests/lean/run/elabAsElim.lean @@ -175,3 +175,14 @@ def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k 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 + +/-! +Issue https://github.com/leanprover/lean4/issues/4347 + +`False.rec` has `motive` as an explicit argument. +-/ + +example (h : False) : Nat := False.rec (fun _ => Nat) h +example (h : False) : Nat := False.rec _ h +example (h : False) : Nat := h.rec +example (h : False) : Nat := h.rec _ diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean index e3fd9967eb..01d5f5ebd8 100644 --- a/tests/lean/run/emptyLcnf.lean +++ b/tests/lean/run/emptyLcnf.lean @@ -3,7 +3,7 @@ import Lean inductive MyEmpty def f (x : MyEmpty) : Nat := - MyEmpty.casesOn x + MyEmpty.casesOn _ x set_option trace.Compiler.result true /--