max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: IndPredBelow should not add auxiliary declarations containing sorry (#4563)

Browse source 
Issue #4535 is being affected by a bug in the structural inductive
predicate termination checker (`IndPred.lean`). This module did not
exist in Lean 3, and it is buggy in Lean 4. In the given example, it
introduces an auxiliary declaration containing a `sorry`, and the fails.
This PR ensures this kind of declaration is not added to the
environment.

Closes #4535

TODO: we need a new maintainer for the `IndPred.lean`.
This commit is contained in:
Leonardo de Moura 2024-06-25 22:57:32 +02:00 • committed by GitHub
parent 4964ce3ce8
commit fb6d29e260
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/IndPredBelow.lean
View file

@ -434,7 +434,7 @@ partial def mkBelowMatcher
withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
for lhs in lhss do
trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
res.addMatcher
-- if a wrong index is picked, the resulting matcher can be type-incorrect.
-- we check here, so that errors can propagate higher up the call stack.

14
src/Lean/Meta/Match/Match.lean
View file

@ -830,8 +830,12 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
The number of patterns must be the same in each `AltLHS`.
The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
`(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
-/
def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
let numDiscrs := discrInfos.size
let numEqs := getNumEqsFromDiscrInfos discrInfos
@ -844,6 +848,11 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
let uElim ← getLevel matchTypeBody
let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
let val ← instantiateMVars val
let type ← instantiateMVars type
if exceptionIfContainsSorry then
if type.hasSorry || val.hasSorry then
throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
/- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@ -857,7 +866,6 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
| negSucc n => succ n
```
which is defined **before** `Int.decLt` -/
let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen