[sgraf812]

This PR fixes fun_cases and fun_induction for a match whose discriminant appears in the type of another variable in the goal.

Example:

inductive W where | a | b

inductive Op : W → Type where
  | y : Fin w.ctorIdx → Op w

def Op.f {w} (i : Op w) : Nat :=
  match (generalizing := false) (motive := Op w → Nat) i with
  | .y _ =>
    match (generalizing := false) (motive := W → Nat) w with
    | .a => 1
    | _ => 2

#check Op.f.fun_cases_unfolding
-- failed to transform matcher, type error when constructing new pre-splitter motive

The functional cases construction splits the inner match with a motive that abstracts the discriminant w from the goal motive (Op.y x) (match w with ...). The variable x : Fin w.ctorIdx stays free, so fun w' => motive (Op.y x) ... is type-incorrect.

For the motive of a match, mkLambdaFVarsMasked now abstracts a discriminant only if the result is type-correct (checkTypeCorrect := true). It checks the abstraction over all discriminants once, and only if that check fails does it check each discriminant. An unabstracted discriminant still gets the equality w = pattern from MatcherApp.transform, and rwMatcher uses this equality to reduce the match in each alternative. The default match was not affected, because it generalizes x together with w.

Closes #8213

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 87980ca against 8853987 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +11.4G (+0.11%)

Medium changes (2🟥)

• 🟥 build/module/Std.Data.DTreeMap.Internal.Balancing//instructions: +4.5G (+8.22%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Model//instructions: +1.5G (+2.76%) (reduced significance based on absolute threshold)

Small changes (1✅, 36🟥)

• 🟥 build/module/Init.Data.Array.Sort.Lemmas//instructions: +307.5M (+10.51%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Dyadic.Basic//instructions: +38.6M (+0.30%)
• 🟥 build/module/Init.Data.Float.Model.Unpacked.Pack.Lemmas//instructions: +15.6M (+1.56%)
• 🟥 build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop//instructions: +429.5M (+4.03%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.List.ControlImpl//instructions: +41.9M (+5.14%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.List.MinMaxOn//instructions: +41.7M (+0.73%)
• 🟥 build/module/Init.Data.List.Monadic//instructions: +154.7M (+1.91%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.List.Nat.Basic//instructions: +14.1M (+0.24%)
• 🟥 build/module/Init.Data.List.SplitOn.Lemmas//instructions: +18.5M (+0.99%)
• 🟥 build/module/Init.Data.Nat.PowMod//instructions: +12.3M (+1.19%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Nat.Power2.Lemmas//instructions: +6.7M (+0.82%)
• 🟥 build/module/Init.Data.Ord.Array//instructions: +23.6M (+0.84%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Range.Polymorphic.RangeIterator//instructions: +977.8M (+5.55%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.String.Decode//instructions: +189.1M (+0.80%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.String.Defs//instructions: +14.4M (+0.60%)
• 🟥 build/module/Init.Data.String.Lemmas.FindPos//instructions: +19.0M (+0.53%)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Char//instructions: +44.3M (+1.14%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Memcmp//instructions: +46.1M (+3.43%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Pred//instructions: +44.0M (+0.86%)
• 🟥 build/module/Init.Data.String.Lemmas.Pattern.Split.Char//instructions: +145.6M (+9.10%) (reduced significance based on absolute threshold)
• and 17 more

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 0352305 against 8853987 are in. There are significant results. @sgraf812

• 🟥 build exited with code -1
• 🟥 other exited with code -1

No significant changes detected.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 44bed7e against 8853987 are in. There are significant results. @sgraf812

• 🟥 build exited with code -1
• 🟥 other exited with code -1

No significant changes detected.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for c45c172 against 8853987 are in. There are significant results. @sgraf812

• 🟥 build exited with code -1
• 🟥 other exited with code -1

No significant changes detected.

[sgraf812]

!bench

[leanprover-radar]

Failed to find a commit to compare against.

_{You can edit the original message until the command succeeds.}

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for a82fd40 against 8853987 are in. No significant results found. @sgraf812

• 🟥 build//instructions: +563.1M (+0.01%)

Small changes (1✅, 6🟥)

• 🟥 build/module/Init.Data.Array.Sort.Lemmas//instructions: +35.6M (+1.22%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Nat.PowMod//instructions: +2.1M (+0.21%)
• 🟥 build/module/Init.Data.Vector.OfFn//instructions: +10.1M (+0.29%)
• 🟥 build/module/Lean.Data.RArray//instructions: +13.6M (+0.34%)
• 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +105.8M (+0.32%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Balancing//instructions: +191.7M (+0.35%)
• ✅ compiled/server_startup//instructions: -2.0M (-0.57%)