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

fix: FunInd: rewrite matches more reliably in .induct_unfolding (#8277)

Browse source 
This PR improves the generation of `.induct_unfolding` by rewriting
`match` statements more reliably, using the new “congruence equations”
introduced in #8284. Fixes #8195.
This commit is contained in:
Joachim Breitner 2025-05-11 17:26:28 +02:00 • committed by GitHub
parent dc1a70fa43
commit 33aaabaed7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 302 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Meta/Match/MatcherApp/Transform.lean
View file

@ -222,7 +222,7 @@ def transform
(addEqualities : Bool := false)
(onParams : Expr → n Expr := pure)
(onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
(onAlt : Expr → Expr → n Expr := fun _ e => pure e)
(onAlt : Nat → Expr → Expr → n Expr := fun _ _ e => pure e)
(onRemaining : Array Expr → n (Array Expr) := pure) :
n MatcherApp := do
@ -294,12 +294,13 @@ def transform
let aux2 := mkApp aux2 motive'
let aux2 := mkAppN aux2 discrs'
unless (← isTypeCorrect aux2) do
logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
check aux2
mapError (f := (m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\n{indentD ·}")) do
check aux2
let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2
let mut alts' := #[]
for alt in matcherApp.alts,
for altIdx in [:matcherApp.alts.size],
alt in matcherApp.alts,
numParams in matcherApp.altNumParams,
splitterNumParams in matchEqns.splitterAltNumParams,
origAltType in origAltTypes,
@ -313,7 +314,7 @@ def transform
forallBoundedTelescope altType extraEqualities fun ys4 altType => do
let alt ← try instantiateLambda alt (args ++ ys3)
catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
let alt' ← onAlt altType alt
let alt' ← onAlt altIdx altType alt
mkLambdaFVars (ys ++ ys2 ++ ys3 ++ ys4) alt'
alts' := alts'.push alt'
@ -339,7 +340,8 @@ def transform
let altTypes ← inferArgumentTypesN matcherApp.alts.size aux
let mut alts' := #[]
for alt in matcherApp.alts,
for altIdx in [:matcherApp.alts.size],
alt in matcherApp.alts,
numParams in matcherApp.altNumParams,
altType in altTypes do
let alt' ← forallBoundedTelescope altType numParams fun xs altType => do
@ -348,7 +350,7 @@ def transform
let names ← lambdaTelescope alt fun xs _ => xs.mapM (·.fvarId!.getUserName)
withUserNames xs names do
let alt ← instantiateLambda alt xs
let alt' ← onAlt altType alt
let alt' ← onAlt altIdx altType alt
mkLambdaFVars (xs ++ ys4) alt'
alts' := alts'.push alt'
@ -422,7 +424,7 @@ def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do
}
mkArrowN extraParams typeMatcherApp.toExpr
)
(onAlt := fun expAltType alt => do
(onAlt := fun _altIdx expAltType alt => do
let altType ← inferType alt
let eq ← mkEq expAltType altType
let proof ← mkFreshExprSyntheticOpaqueMVar eq

77
src/Lean/Meta/Tactic/FunInd.lean
View file

@ -203,8 +203,6 @@ something goes wrong, one still gets a useful induction principle, just maybe wi
not fully simplified.
-/
set_option autoImplicit false
namespace Lean.Tactic.FunInd
open Lean Elab Meta
@ -327,7 +325,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
-- statement and the inferred alt types
let dummyGoal := mkConst ``True []
mkArrow eTypeAbst dummyGoal)
(onAlt := fun altType alt => do
(onAlt := fun _altIdx altType alt => do
lambdaTelescope1 alt fun oldIH' alt => do
forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
let #[newIH'] := newIH' | unreachable!
@ -345,7 +343,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
(onMotive := fun _motiveArgs motiveBody => do
let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
M.eval (foldAndCollect oldIH newIH isRecCall body))
(onAlt := fun altType alt => do
(onAlt := fun _altIdx altType alt => do
lambdaTelescope1 alt fun oldIH' alt => do
-- We don't have suitable newIH around here, but we don't care since
-- we just want to fold calls. So lets create a fake one.
@ -650,7 +648,7 @@ def rwFun (names : Array Name) (e : Expr) : MetaM Simp.Result := do
else
return { expr := e }
def rwMatcher (e : Expr) : MetaM Simp.Result := do
def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
let mut e := e
while true do
@ -664,10 +662,67 @@ def rwMatcher (e : Expr) : MetaM Simp.Result := do
break
return { expr := e }
else
Split.simpMatch e
unless (← isMatcherApp e) do
return { expr := e }
let matcherDeclName := e.getAppFn.constName!
let eqns ← Match.genMatchCongrEqns matcherDeclName
unless altIdx < eqns.size do
trace[Tactic.FunInd] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
return { expr := e }
let eqnThm := eqns[altIdx]!
try
withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
let eqProof := mkAppN (mkConst eqnThm e.getAppFn.constLevels!) e.getAppArgs
let (hyps, _, eqType) ← forallMetaTelescope (← inferType eqProof)
trace[Meta.FunInd] "eqProof has type{indentExpr eqType}"
let proof := mkAppN eqProof hyps
let hyps := hyps.map (·.mvarId!)
let (isHeq, lhs, rhs) ← do
if let some (_, lhs, _, rhs) := eqType.heq? then pure (true, lhs, rhs) else
if let some (_, lhs, rhs) := eqType.eq? then pure (false, lhs, rhs) else
throwError m!"Type of {.ofConstName eqnThm} is not an equality"
if !(← isDefEq e lhs) then
throwError m!"Left-hand side {lhs} of {.ofConstName eqnThm} does not apply to {e}"
/-
Here we instantiate the hypotheses of the congruence equation theorem
There are two sets of hypotheses to instantiate:
- `Eq` or `HEq` that relate the discriminants to the patterns
Solving these should instantiate the pattern variables.
- Overlap hypotheses (`isEqnThmHypothesis`)
With more book keeping we could maybe do this very precisely, knowing exactly
which facts provided by the splitter should go where, but it's tedious.
So for now let's use heuristics and try `assumption` and `rfl`.
-/
for h in hyps do
unless (← h.isAssigned) do
let hType ← h.getType
if Simp.isEqnThmHypothesis hType then
-- Using unrestricted h.substVars here does not work well; it could
-- even introduce a dependency on the `oldIH` we want to eliminate
h.assumption <|> throwError "Failed to discharge {h}"
else if hType.isEq then
h.assumption <|> h.refl <|> throwError m!"Failed to resolve {h}"
else if hType.isHEq then
h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve {h}"
let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned)
unless unassignedHyps.isEmpty do
throwError m!"Not all hypotheses of {.ofConstName eqnThm} could be discharged: {unassignedHyps}"
let rhs ← instantiateMVars rhs
let proof ← instantiateMVars proof
let proof ← if isHeq then
try mkEqOfHEq proof
catch e => throwError m!"Could not un-HEq {proof}:{indentD e.toMessageData} "
else
pure proof
return {
expr := rhs
proof? := proof
}
catch ex =>
trace[Meta.FunInd] "Failed to apply {.ofConstName eqnThm}:{indentD ex.toMessageData}"
return { expr := e }
/--
Builds an expression of type `goal` by replicating the expression `e` into its tail-call-positions,
where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
as `MVars` as it goes.
@ -767,13 +822,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
(addEqualities := true)
(onParams := (foldAndCollect oldIH newIH isRecCall ·))
(onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
(onAlt := fun expAltType alt => M2.branch do
(onAlt := fun altIdx expAltType alt => M2.branch do
lambdaTelescope1 alt fun oldIH' alt => do
forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
let #[newIH'] := newIH' | unreachable!
let toErase' := toErase ++ #[oldIH', newIH'.fvarId!]
let toClear' := toClear ++ matcherApp.discrs.filterMap (·.fvarId?)
let alt' ← withRewrittenMotiveArg goal' rwMatcher fun goal'' => do
let alt' ← withRewrittenMotiveArg goal' (rwMatcher altIdx) fun goal'' => do
-- logInfo m!"rwMatcher after {matcherApp.matcherName} on{indentExpr goal'}\nyields{indentExpr goal''}"
buildInductionBody toErase' toClear' goal'' oldIH' newIH'.fvarId! isRecCall alt
mkLambdaFVars #[newIH'] alt')
@ -790,8 +845,8 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
(addEqualities := true)
(onParams := (foldAndCollect oldIH newIH isRecCall ·))
(onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
(onAlt := fun expAltType alt => M2.branch do
withRewrittenMotiveArg expAltType Split.simpMatch fun expAltType' =>
(onAlt := fun altIdx expAltType alt => M2.branch do
withRewrittenMotiveArg expAltType (rwMatcher altIdx) fun expAltType' =>
buildInductionBody toErase toClear expAltType' oldIH newIH isRecCall alt)
return matcherApp'.toExpr

102
tests/lean/run/funind_unfolding.lean
View file

@ -10,9 +10,10 @@ termination_by x => x
info: fib.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
(case3 : ∀ (n : Nat), motive n.succ.succ (fib n + fib (n + 1))) (x✝ : Nat) : motive x✝ (fib x✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check fib.fun_cases_unfolding
-- set_option trace.Meta.FunInd true in
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
@ -25,7 +26,7 @@ info: ackermann.fun_cases_unfolding (motive : Nat → Nat → Nat → Prop) (cas
(case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m))) (x✝ x✝¹ : Nat) :
motive x✝ x✝¹ (ackermann x✝ x✝¹)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check ackermann.fun_cases_unfolding
def fib' : Nat → Nat
@ -39,7 +40,7 @@ info: fib'.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0
(case3 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → motive n (fib' (n - 1) + fib' (n - 2))) (x✝ : Nat) :
motive x✝ (fib' x✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check fib'.fun_cases_unfolding
def fib'' (n : Nat) : Nat :=
@ -66,7 +67,7 @@ info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n
¬foo < 100 → motive n 0)
(n : Nat) : motive n (fib'' n)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check fib''.fun_cases_unfolding
-- set_option trace.Meta.FunInd true in
@ -80,7 +81,7 @@ info: filter.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 :
(case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs)) (p : Nat → Bool)
(x✝ : List Nat) : motive p x✝
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check filter.fun_cases
/--
@ -90,7 +91,7 @@ info: filter.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List
(case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs) (filter p xs))
(p : Nat → Bool) (x✝ : List Nat) : motive p x✝ (filter p x✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check filter.fun_cases_unfolding
/--
@ -98,7 +99,7 @@ info: filter.induct (p : Nat → Bool) (motive : List Nat → Prop) (case1 : mot
(case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs → motive (x :: xs))
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check filter.induct
/--
@ -107,7 +108,7 @@ info: filter.induct_unfolding (p : Nat → Bool) (motive : List Nat → List Nat
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs (filter p xs) → motive (x :: xs) (filter p xs))
(a✝ : List Nat) : motive a✝ (filter p a✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check filter.induct_unfolding
theorem filter_const_false_is_nil :
@ -141,7 +142,7 @@ info: map.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀
(case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs)) (f : Nat → Bool) (x✝ : List Nat) :
motive f x✝
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map.fun_cases
/--
@ -150,14 +151,14 @@ info: map.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Boo
(case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs) (f x :: map f xs)) (f : Nat → Bool)
(x✝ : List Nat) : motive f x✝ (map f x✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map.fun_cases_unfolding
/--
info: map.induct (motive : List Nat → Prop) (case1 : motive [])
(case2 : ∀ (x : Nat) (xs : List Nat), motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map.induct
/--
@ -165,11 +166,12 @@ info: map.induct_unfolding (f : Nat → Bool) (motive : List Nat → List Bool
(case2 : ∀ (x : Nat) (xs : List Nat), motive xs (map f xs) → motive (x :: xs) (f x :: map f xs)) (a✝ : List Nat) :
motive a✝ (map f a✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map.induct_unfolding
namespace BinaryWF
-- set_option trace.Meta.FunInd true in
def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2 f xs ys
| _, _ => []
@ -187,7 +189,7 @@ info: BinaryWF.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List N
motive x x_1 [])
(a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2.induct_unfolding
end BinaryWF
@ -209,7 +211,7 @@ info: BinaryStructural.map2.induct_unfolding (f : Nat → Nat → Bool) (motive
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive t x [])
(a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2.induct_unfolding
end BinaryStructural
@ -245,7 +247,7 @@ info: MutualWF.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool) (motive1
motive2 x x_1 []) :
(∀ (a a_1 : List Nat), motive1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive2 a a_1 (map2b f a a_1)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2a.mutual_induct_unfolding
/--
@ -266,7 +268,7 @@ info: MutualWF.map2a.induct_unfolding (f : Nat → Nat → Bool) (motive1 motive
motive2 x x_1 [])
(a✝ a✝¹ : List Nat) : motive1 a✝ a✝¹ (map2a f a✝ a✝¹)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2a.induct_unfolding
end MutualWF
@ -297,7 +299,7 @@ info: MutualStructural.map2a.induct (motive_1 motive_2 : List Nat → List Nat
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_2 t x)
(a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2a.induct
@ -320,7 +322,7 @@ info: MutualStructural.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool)
motive_2 t x (map2b f t x)) :
(∀ (a a_1 : List Nat), motive_1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive_2 a a_1 (map2b f a a_1)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2a.mutual_induct_unfolding
@ -343,7 +345,7 @@ info: MutualStructural.map2a.induct_unfolding (f : Nat → Nat → Bool)
motive_2 t x (map2b f t x))
(a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹ (map2a f a✝ a✝¹)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check map2a.induct_unfolding
end MutualStructural
@ -391,7 +393,7 @@ info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat →
(case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int)
(root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check siftDown.induct_unfolding
/--
@ -413,7 +415,7 @@ info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.si
(case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int)
(root : Nat) (h : e ≤ a.size) : motive a root h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check siftDown.induct
-- Now something with have
@ -429,14 +431,14 @@ info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42
(case2 : ∀ (x : Nat), 0 < x → ¬x = 42 → motive (x - 1) (withHave (x - 1)) → motive x (withHave (x - 1))) (n : Nat) :
motive n (withHave n)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check withHave.induct_unfolding
/--
info: withHave.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
(case2 : ∀ (n : Nat), 0 < n → ¬n = 42 → motive n (withHave (n - 1))) (n : Nat) : motive n (withHave n)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check withHave.fun_cases_unfolding
-- Structural Mutual recursion
@ -466,7 +468,7 @@ info: Tree.size.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → N
motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
(a✝ : Tree α) : motive_1 a✝ a✝.size
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check Tree.size.induct_unfolding
/--
@ -483,5 +485,55 @@ info: Tree.size_aux.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α
motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
(a✝ : List (Tree α)) : motive_2 a✝ (Tree.size_aux a✝)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check Tree.size_aux.induct_unfolding
-- When the discriminants are duplicated, it is very easy for `FunInd` to be confused
-- about how to instantiate the equality theorem. Maybe not relevant in practice for now?
-- Maybe even impossible to solve.
-- set_option trace.Meta.FunInd true in
set_option linter.unusedVariables false in
def duplicatedDiscriminant (n : Nat) : Bool :=
match h1 : n, h2 : n with
| 0, 0 => true
| a+1, 0 => false -- by simp_all
| 0, b+1 => false -- by simp_all
| a, b => true
/--
info: duplicatedDiscriminant.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 = 0 → motive 0 true)
(case2 :
∀ (a : Nat),
a.succ = 0 →
motive 0
(match h1 : 0, h2 : 0 with
| 0, 0 => true
| a.succ, 0 => false
| 0, b.succ => false
| a, b => true))
(case3 :
∀ (b : Nat),
0 = b.succ →
motive b.succ
(match h1 : b.succ, h2 : b.succ with
| 0, 0 => true
| a.succ, 0 => false
| 0, b_1.succ => false
| a, b_1 => true))
(case4 :
∀ (b : Nat),
(b = 0 → b = 0 → False) →
(∀ (a : Nat), b = a.succ → b = 0 → False) →
(∀ (b_1 : Nat), b = 0 → b = b_1.succ → False) →
motive b
(match h1 : b, h2 : b with
| 0, 0 => true
| a.succ, 0 => false
| 0, b_1.succ => false
| a, b_1 => true))
(n : Nat) : motive n (duplicatedDiscriminant n)
-/
#guard_msgs(pass trace, all) in
#check duplicatedDiscriminant.fun_cases_unfolding

21
tests/lean/run/issue8103.lean
View file

@ -1,3 +1,4 @@
-- set_option trace.Meta.FunInd true in
def foo (n m : Nat) (h : n < m) : Nat :=
match m with
| 0 => by contradiction -- This case should not show up in the principles below
@ -10,7 +11,7 @@ info: foo.induct (motive : (n m : Nat) → n < m → Prop) (case1 : ∀ (m : Nat
(case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
(h : n < m) : motive n m h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check foo.induct
/--
@ -20,7 +21,7 @@ info: foo.induct_unfolding (motive : (n m : Nat) → n < m → Nat → Prop)
∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ (foo n m ⋯) → motive n.succ m.succ h (foo n m ⋯))
(n m : Nat) (h : n < m) : motive n m h (foo n m h)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check foo.induct_unfolding
@ -30,7 +31,7 @@ info: foo.fun_cases (motive : (n m : Nat) → n < m → Prop)
(case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m + 1 → n.succ < m.succ → motive n.succ m.succ h) (n m : Nat)
(h : n < m) : motive n m h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check foo.fun_cases
def bar (n m : Nat) (h : n = m) : Nat :=
@ -45,7 +46,7 @@ info: bar.induct (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h : 0 =
(case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
(h : n = m) : motive n m h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check bar.induct
/--
@ -54,7 +55,7 @@ info: bar.induct_unfolding (motive : (n m : Nat) → n = m → Nat → Prop) (ca
∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ (bar n m ⋯) → motive n.succ m.succ h (bar n m ⋯))
(n m : Nat) (h : n = m) : motive n m h (bar n m h)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check bar.induct_unfolding
/--
@ -62,7 +63,7 @@ info: bar.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h :
(case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
(h : n = m) : motive n m h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check bar.fun_cases
def baz (n : Nat) (h : n ≠ 0) : Nat :=
@ -76,7 +77,7 @@ info: baz.induct (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 +
(case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 → motive k.succ h) (n : Nat) (h : n ≠ 0) :
motive n h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check baz.induct
/--
@ -84,14 +85,14 @@ info: baz.induct_unfolding (motive : (n : Nat) → n ≠ 0 → Nat → Prop) (ca
(case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 (baz k h_1) → motive k.succ h (baz k h_1)) (n : Nat)
(h : n ≠ 0) : motive n h (baz n h)
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check baz.induct_unfolding
/--
info: baz.fun_cases (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 + 1 ≠ 0), Nat.succ 0 ≠ 0 → motive (Nat.succ 0) h)
(case2 : ∀ (k : Nat) (h : k + 1 ≠ 0), ¬k = 0 → k.succ ≠ 0 → motive k.succ h) (n : Nat) (h : n ≠ 0) : motive n h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check baz.fun_cases
@ -107,5 +108,5 @@ info: mean.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h :
(case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
(h : n = m) : motive n m h
-/
#guard_msgs in
#guard_msgs(pass trace, all) in
#check mean.fun_cases

106
tests/lean/run/issue8195.lean Normal file
View file

@ -0,0 +1,106 @@
import Lean
-- set_option trace.Meta.FunInd true
axiom testSorry : α
def test (l : List Nat) : Nat :=
match l with
| [] => 0
| x :: l =>
match x == 3 with
| false => test l
| true => test l
/--
info: test.induct_unfolding (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
(case2 : ∀ (x : Nat) (l : List Nat), (x == 3) = false → motive l (test l) → motive (x :: l) (test l))
(case3 : ∀ (x : Nat) (l : List Nat), (x == 3) = true → motive l (test l) → motive (x :: l) (test l)) (l : List Nat) :
motive l (test l)
-/
#guard_msgs in
#check test.induct_unfolding
opaque someFunction (x : Nat) (h : (x == 3) = false) : Nat
opaque someOtherFunction (x : Nat) (h : (x == 3) = true) : Nat
def deptest (l : List Nat) : Nat :=
match l with
| [] => 0
| x :: l =>
match h : x == 3 with
| false => deptest l + someFunction x h
| true => deptest l + someOtherFunction x h
/--
info: deptest.induct_unfolding (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
(case2 :
∀ (x : Nat) (l : List Nat) (h : (x == 3) = false),
motive l (deptest l) → motive (x :: l) (deptest l + someFunction x h))
(case3 :
∀ (x : Nat) (l : List Nat) (h : (x == 3) = true),
motive l (deptest l) → motive (x :: l) (deptest l + someOtherFunction x h))
(l : List Nat) : motive l (deptest l)
-/
#guard_msgs in
#check deptest.induct_unfolding
-- This one doesn't work, the result type varies in the branches
-- But we fail gracefully
def depTestOddType (l : List Nat) :
match l with
| [] => Unit
| x :: _ =>
if x == 3 then
Unit
else
Nat
:=
match l with
| [] => ()
| x :: _ =>
(match h : x == 3 with
| false => someFunction x h
| true => () : if x == 3 then Unit else Nat)
/--
info: depTestOddType.fun_cases_unfolding
(motive :
(l : List Nat) →
(match l with
| [] => Unit
| x :: tail => if (x == 3) = true then Unit else Nat) →
Prop)
(case1 : motive [] ())
(case2 :
∀ (x : Nat) (l : List Nat),
(x == 3) = false →
motive (x :: l)
(match h : x == 3 with
| false => someFunction x h
| true => ()))
(case3 :
∀ (x : Nat) (l : List Nat),
(x == 3) = true →
motive (x :: l)
(match h : x == 3 with
| false => someFunction x h
| true => ()))
(l : List Nat) : motive l (depTestOddType l)
-/
#guard_msgs in
#check depTestOddType.fun_cases_unfolding
-- set_option trace.Meta.FunInd true in
set_option linter.unusedVariables false in
def testMe (n : Nat) : Bool :=
match _ : n - 2 with
| 0 => true
| m => false
/--
info: testMe.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : ∀ (n : Nat), n - 2 = 0 → motive n true)
(case2 : ∀ (n : Nat), (n - 2 = 0 → False) → motive n false) (n : Nat) : motive n (testMe n)
-/
#guard_msgs in
#check testMe.fun_cases_unfolding

32
tests/lean/run/issue8213.lean Normal file
View file

@ -0,0 +1,32 @@
-- set_option trace.Meta.FunInd true
def myTest {α}
(mmotive : (x : List α) → Sort v)
(x : List α)
(h_1 : (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc))
(h_2 : (x' : List α) → x = x' → mmotive x') : mmotive x :=
match (generalizing := false) h : x with
| a :: dc => h_1 a dc h
| x' => h_2 x' h
/--
error: Failed to realize constant myTest.fun_cases:
Cannot derive functional cases principle (please report this issue)
⏎
failed to transform matcher, type error when constructing new pre-splitter motive:
@myTest.match_1 _fvar.28 (fun x => @_fvar.27 _fvar.28 _fvar.29 x _fvar.31 _fvar.32) _fvar.30
⏎
Application type mismatch: In the appplication
motive mmotive x✝ h_1
the final argument
h_1
has type
(a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
but is expected to have type
(a : α) → (dc : List α) → x✝ = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
---
error: unknown identifier 'myTest.fun_cases'
-/
#guard_msgs in
def foo := @myTest.fun_cases