diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 92a348423d..f845ac7876 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -98,9 +98,68 @@ def unfoldNamedPattern (e : Expr) : MetaM Expr := do 1. Eliminates arguments for named parameters and the associated equation proofs. - 2. Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs. - Recall that this kind of parameter always occurs after the parameters correspoting to pattern variables. - `numNonEqParams` is the size of the prefix. + 2. Instantiate the `Unit` parameter of an otherwise argumentless alternative. + + It does not handle the equality parameters associated with the `h : discr` notation. + + The continuation `k` takes four arguments `ys args mask type`. + - `ys` are variables for the hypotheses that have not been eliminated. + - `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size` + - `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`. + - `type` is the resulting type for `altType`. + + We use the `mask` to build the splitter proof. See `mkSplitterProof`. + + This can be used to use the alternative of a match expression in its splitter. +-/ +partial def forallAltVarsTelescope (altType : Expr) (altNumParams numDiscrEqs : Nat) + (k : (patVars : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) : MetaM α := do + go #[] #[] #[] 0 altType +where + go (ys : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do + let type ← whnfForall type + if i < altNumParams - numDiscrEqs then + let Expr.forallE n d b .. := type + | throwError "expecting {altNumParams} parameters, excluding {numDiscrEqs} equalities, but found type{indentExpr altType}" + + -- Handle the special case of `Unit` parameters. + if i = 0 && altNumParams - numDiscrEqs = 1 && d.isConstOf ``Unit && !b.hasLooseBVars then + return ← k #[] #[mkConst ``Unit.unit] #[false] b + + let d ← Match.unfoldNamedPattern d + withLocalDeclD n d fun y => do + let typeNew := b.instantiate1 y + if let some (_, lhs, rhs) ← matchEq? d then + if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then + let some j := ys.finIdxOf? lhs | unreachable! + let ys := ys.eraseIdx j + let some k := args.idxOf? lhs | unreachable! + let mask := mask.set! k false + let args := args.map fun arg => if arg == lhs then rhs else arg + let arg ← mkEqRefl rhs + let typeNew := typeNew.replaceFVar lhs rhs + return ← withReplaceFVarId lhs.fvarId! rhs do + withReplaceFVarId y.fvarId! arg do + go ys (args.push arg) (mask.push false) (i+1) typeNew + go (ys.push y) (args.push y) (mask.push true) (i+1) typeNew + else + let type ← Match.unfoldNamedPattern type + k ys args mask type + + isNamedPatternProof (type : Expr) (h : Expr) : Bool := + Option.isSome <| type.find? fun e => + if let some e := Match.isNamedPattern? e then + e.appArg! == h + else + false + + +/-- + Extension of `forallAltTelescope` that continues further: + + Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs. + Recall that this kind of parameter always occurs after the parameters corresponding to pattern + variables. The continuation `k` takes four arguments `ys args mask type`. - `ys` are variables for the hypotheses that have not been eliminated. @@ -116,57 +175,45 @@ def unfoldNamedPattern (e : Expr) : MetaM Expr := do partial def forallAltTelescope (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : (ys : Array Expr) → (eqs : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) : MetaM α := do - go #[] #[] #[] #[] 0 altType + forallAltVarsTelescope altType altNumParams numDiscrEqs fun ys args mask altType => do + go ys #[] args mask 0 altType where go (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do let type ← whnfForall type - if i < altNumParams then + if i < numDiscrEqs then let Expr.forallE n d b .. := type | throwError "expecting {altNumParams} parameters, including {numDiscrEqs} equalities, but found type{indentExpr altType}" - if i < altNumParams - numDiscrEqs then - let d ← unfoldNamedPattern d - withLocalDeclD n d fun y => do - let typeNew := b.instantiate1 y - if let some (_, lhs, rhs) ← matchEq? d then - if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then - let some j := ys.finIdxOf? lhs | unreachable! - let ys := ys.eraseIdx j - let some k := args.idxOf? lhs | unreachable! - let mask := mask.set! k false - let args := args.map fun arg => if arg == lhs then rhs else arg - let arg ← mkEqRefl rhs - let typeNew := typeNew.replaceFVar lhs rhs - return ← withReplaceFVarId lhs.fvarId! rhs do - withReplaceFVarId y.fvarId! arg do - go ys eqs (args.push arg) (mask.push false) (i+1) typeNew - go (ys.push y) eqs (args.push y) (mask.push true) (i+1) typeNew + let arg ← if let some (_, _, rhs) ← matchEq? d then + mkEqRefl rhs + else if let some (_, _, _, rhs) ← matchHEq? d then + mkHEqRefl rhs else - let arg ← if let some (_, _, rhs) ← matchEq? d then - mkEqRefl rhs - else if let some (_, _, _, rhs) ← matchHEq? d then - mkHEqRefl rhs - else - throwError "unexpected match alternative type{indentExpr altType}" - withLocalDeclD n d fun eq => do - let typeNew := b.instantiate1 eq - go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew + throwError "unexpected match alternative type{indentExpr altType}" + withLocalDeclD n d fun eq => do + let typeNew := b.instantiate1 eq + go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew else let type ← unfoldNamedPattern type - /- Recall that alternatives that do not have variables have a `Unit` parameter to ensure - they are not eagerly evaluated. -/ - if ys.size == 1 then - if (← inferType ys[0]!).isConstOf ``Unit && !(← dependsOn type ys[0]!.fvarId!) then - let rhs := mkConst ``Unit.unit - return ← withReplaceFVarId ys[0]!.fvarId! rhs do - return (← k #[] #[] #[rhs] #[false] type) k ys eqs args mask type - isNamedPatternProof (type : Expr) (h : Expr) : Bool := - Option.isSome <| type.find? fun e => - if let some e := isNamedPattern? e then - e.appArg! == h - else - false +/-- +Given an application of an matcher arm `alt` that is expecting the `numDiscrEqs`, and +an array of `discr = pattern` equalities (one for each discriminant), apply those that +are expected by the alternative. +-/ +partial def mkAppDiscrEqs (alt : Expr) (heqs : Array Expr) (numDiscrEqs : Nat) : MetaM Expr := do + go alt (← inferType alt) 0 +where + go e ty i := do + if i < numDiscrEqs then + let Expr.forallE n d b .. := ty + | throwError "expecting {numDiscrEqs} equalities, but found type{indentExpr alt}" + for heq in heqs do + if (← isDefEq (← inferType heq) d) then + return ← go (mkApp e heq) (b.instantiate1 heq) (i+1) + throwError "Could not find equation {n} : {d} among {heqs}" + else + return e namespace SimpH @@ -328,21 +375,33 @@ private def unfoldElimOffset (mvarId : MVarId) : MetaM MVarId := do mvarId.deltaTarget (· == ``Nat.elimOffset) /-- - Helper method for proving a conditional equational theorem associated with an alternative of - the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/ -partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr := withLCtx {} {} do +Helper method for proving a conditional equational theorem associated with an alternative of +the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. + +The `heqPos`/`heqNum` arguments indicate that these hypotheses are `Eq`/`HEq` hypotheses +to substitute first; this is used for the generalized match equations. +-/ +partial def proveCondEqThm (matchDeclName : Name) (type : Expr) + (heqPos : Nat := 0) (heqNum : Nat := 0) : MetaM Expr := withLCtx {} {} do let type ← instantiateMVars type - forallTelescope type fun ys target => do - let mvar0 ← mkFreshExprSyntheticOpaqueMVar target - trace[Meta.Match.matchEqs] "proveCondEqThm {mvar0.mvarId!}" - let mvarId ← mvar0.mvarId!.deltaTarget (· == matchDeclName) - withDefault <| go mvarId 0 - mkLambdaFVars ys (← instantiateMVars mvar0) + let mvar0 ← mkFreshExprSyntheticOpaqueMVar type + trace[Meta.Match.matchEqs] "proveCondEqThm {mvar0.mvarId!}" + let mut mvarId := mvar0.mvarId! + if heqNum > 0 then + mvarId := (← mvarId.introN heqPos).2 + for _ in [:heqNum] do + let (h, mvarId') ← mvarId.intro1 + mvarId ← subst mvarId' h + trace[Meta.Match.matchEqs] "proveCondEqThm after subst{mvarId}" + mvarId := (← mvarId.intros).2 + mvarId ← mvarId.deltaTarget (· == matchDeclName) + mvarId ← mvarId.heqOfEq + go mvarId 0 + instantiateMVars mvar0 where go (mvarId : MVarId) (depth : Nat) : MetaM Unit := withIncRecDepth do trace[Meta.Match.matchEqs] "proveCondEqThm.go {mvarId}" - let mvarId' ← mvarId.modifyTargetEqLHS whnfCore - let mvarId := mvarId' + let mvarId ← mvarId.modifyTargetEqLHS whnfCore let subgoals ← (do mvarId.refl; return #[]) <|> @@ -768,21 +827,121 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no let result := { eqnNames, splitterName, splitterAltNumParams } registerMatchEqns matchDeclName result +def congrEqnThmSuffixBase := "congr_eq" +def congrEqnThmSuffixBasePrefix := congrEqnThmSuffixBase ++ "_" +def congrEqn1ThmSuffix := congrEqnThmSuffixBasePrefix ++ "1" +example : congrEqn1ThmSuffix = "congr_eq_1" := rfl + +/-- Returns `true` if `s` is of the form `congr_eq_` -/ +def iscongrEqnReservedNameSuffix (s : String) : Bool := + congrEqnThmSuffixBasePrefix.isPrefixOf s && (s.drop congrEqnThmSuffixBasePrefix.length).isNat + +/- We generate the equations and splitter on demand, and do not save them on .olean files. -/ +builtin_initialize matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name)) ← + -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`. + -- The resulting state can still be accessed on the generated declarations using `findStateAsync`; + -- see below + registerEnvExtension (pure {}) (asyncMode := .local) + +def registerMatchcongrEqns (matchDeclName : Name) (eqnNames : Array Name) : CoreM Unit := do + modifyEnv fun env => matchCongrEqnsExt.modifyState env fun map => + map.insert matchDeclName eqnNames + +/-- +Generate the congruence equations for the given match auxiliary declaration. +The congruence equations have a completely unrestriced left-hand side (arbitrary discriminants), +and take propositional equations relating the discriminants to the patterns as arguments. In this +sense they combine a congruence lemma with the regular equation lemma. +Since the motive depends on the discriminants, they are `HEq` equations. + +The code duplicates a fair bit of the logic above, and has to repeat the calculation of the +`notAlts`. One could avoid that and generate the generalized equations eagerly above, but they are +not always needed, so for now we live with the code duplication. +-/ +def genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name) := do + let baseName := mkPrivateName (← getEnv) matchDeclName + let firstEqnName := .str baseName congrEqn1ThmSuffix + realizeConst matchDeclName firstEqnName (go baseName) + return matchCongrEqnsExt.findStateAsync (← getEnv) firstEqnName |>.find! matchDeclName +where go baseName := withConfig (fun c => { c with etaStruct := .none }) do + withConfig (fun c => { c with etaStruct := .none }) do + let constInfo ← getConstInfo matchDeclName + let us := constInfo.levelParams.map mkLevelParam + let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function" + let numDiscrEqs := matchInfo.getNumDiscrEqs + forallTelescopeReducing constInfo.type fun xs _matchResultType => do + let mut eqnNames := #[] + let params := xs[:matchInfo.numParams] + let motive := xs[matchInfo.getMotivePos]! + let alts := xs[xs.size - matchInfo.numAlts:] + let firstDiscrIdx := matchInfo.numParams + 1 + let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs] + let mut notAlts := #[] + let mut idx := 1 + for i in [:alts.size] do + let altNumParams := matchInfo.altNumParams[i]! + let thmName := (Name.str baseName congrEqnThmSuffixBase).appendIndexAfter idx + eqnNames := eqnNames.push thmName + let notAlt ← do + let alt := alts[i]! + Match.forallAltVarsTelescope (← inferType alt) altNumParams numDiscrEqs fun altVars args _mask altResultType => do + let patterns ← forallTelescope altResultType fun _ t => pure t.getAppArgs + let mut heqsTypes := #[] + assert! patterns.size == discrs.size + for discr in discrs, pattern in patterns do + let heqType ← mkEqHEq discr pattern + heqsTypes := heqsTypes.push ((`heq).appendIndexAfter (heqsTypes.size + 1), heqType) + withLocalDeclsDND heqsTypes fun heqs => do + let rhs ← Match.mkAppDiscrEqs (mkAppN alt args) heqs numDiscrEqs + let mut hs := #[] + for notAlt in notAlts do + let h ← instantiateForall notAlt patterns + if let some h ← Match.simpH? h patterns.size then + hs := hs.push h + trace[Meta.Match.matchEqs] "hs: {hs}" + let mut notAlt := mkConst ``False + for discr in discrs.toArray.reverse, pattern in patterns.reverse do + notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt + notAlt ← mkForallFVars (discrs ++ altVars) notAlt + let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts) + let thmType ← mkHEq lhs rhs + let thmType ← hs.foldrM (init := thmType) (mkArrow · ·) + let thmType ← mkForallFVars (params ++ #[motive] ++ discrs ++ alts ++ altVars ++ heqs) thmType + let thmType ← Match.unfoldNamedPattern thmType + -- Here we prove the theorem from scratch. One could likely also use the (non-generalized) + -- match equation theorem after subst'ing the `heqs`. + let thmVal ← Match.proveCondEqThm matchDeclName thmType + (heqPos := params.size + 1 + discrs.size + alts.size + altVars.size) (heqNum := heqs.size) + unless (← getEnv).contains thmName do + addDecl <| Declaration.thmDecl { + name := thmName + levelParams := constInfo.levelParams + type := thmType + value := thmVal + } + return notAlt + notAlts := notAlts.push notAlt + idx := idx + 1 + registerMatchcongrEqns matchDeclName eqnNames + builtin_initialize registerTraceClass `Meta.Match.matchEqs -private def isMatchEqName? (env : Environment) (n : Name) : Option Name := do +private def isMatchEqName? (env : Environment) (n : Name) : Option (Name × Bool) := do let .str p s := n | failure - guard <| isEqnReservedNameSuffix s || s == "splitter" + guard <| isEqnReservedNameSuffix s || s == "splitter" || iscongrEqnReservedNameSuffix s let p ← privateToUserName? p guard <| isMatcherCore env p - return p + return (p, iscongrEqnReservedNameSuffix s) builtin_initialize registerReservedNamePredicate (isMatchEqName? · · |>.isSome) builtin_initialize registerReservedNameAction fun name => do - let some p := isMatchEqName? (← getEnv) name | + let some (p, isGenEq) := isMatchEqName? (← getEnv) name | return false - let _ ← MetaM.run' <| getEquationsFor p + if isGenEq then + let _ ← MetaM.run' <| genMatchCongrEqns p + else + let _ ← MetaM.run' <| getEquationsFor p return true end Lean.Meta.Match diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index bcd8b1b9f7..93368b9abc 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -190,8 +190,8 @@ private def forallAltTelescope' {α} (origAltType : Expr) (numParams numDiscrEqs : Nat) (k : Array Expr → Array Expr → n α) : n α := do map2MetaM (fun k => - Match.forallAltTelescope origAltType (numParams - numDiscrEqs) 0 - fun ys _eqs args _mask _bodyType => k ys args + Match.forallAltVarsTelescope origAltType numParams numDiscrEqs + fun ys args _mask _bodyType => k ys args ) k /-- @@ -282,8 +282,8 @@ def transform let aux1 := mkApp aux1 motive' let aux1 := mkAppN aux1 discrs' unless (← isTypeCorrect aux1) do - logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}" - check aux1 + mapError (f := (m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\n{indentD ·}")) do + check aux1 let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1 -- We replace the matcher with the splitter diff --git a/tests/lean/run/matchCongrEqns.lean b/tests/lean/run/matchCongrEqns.lean new file mode 100644 index 0000000000..260ee08dac --- /dev/null +++ b/tests/lean/run/matchCongrEqns.lean @@ -0,0 +1,192 @@ +/-! +Tricky cases and regressions tests for generalized match equations. +-/ +-- set_option trace.Meta.Match.matchEqs 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 + +-- #check myTest.match_1 +/-- +info: myTest.match_1.splitter.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) + (h_1 : (a : α) → (dc : List α) → x✝ = a :: dc → motive (a :: dc)) + (h_2 : (x' : List α) → (∀ (a : α) (dc : List α), x' = a :: dc → False) → x✝ = x' → motive x') : motive x✝ +-/ +#guard_msgs(pass trace, all) in +#check myTest.match_1.splitter +/-- +info: myTest.match_1.congr_eq_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) + (h_1 : (a : α) → (dc : List α) → x✝ = a :: dc → motive (a :: dc)) (h_2 : (x' : List α) → x✝ = x' → motive x') (a : α) + (dc : List α) (heq_1 : x✝ = a :: dc) : + HEq + (match h : x✝ with + | a :: dc => h_1 a dc h + | x' => h_2 x' h) + (h_1 a dc heq_1) +-/ +#guard_msgs(pass trace, all) in +#check myTest.match_1.congr_eq_1 + +/-- +info: myTest.match_1.congr_eq_2.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) + (h_1 : (a : α) → (dc : List α) → x✝ = a :: dc → motive (a :: dc)) (h_2 : (x' : List α) → x✝ = x' → motive x') + (x' : List α) (heq_1 : x✝ = x') : + (∀ (a : α) (dc : List α), x' = a :: dc → False) → + HEq + (match h : x✝ with + | a :: dc => h_1 a dc h + | x' => h_2 x' h) + (h_2 x' heq_1) +-/ +#guard_msgs(pass trace, all) in +#check myTest.match_1.congr_eq_2 + + +def take (n : Nat) (xs : List α) : List α := match n, xs with + | 0, _ => [] + | _+1, [] => [] + | n+1, a::as => a :: take n as + +/-- +info: take.match_1.{u_1, u_2} {α : Type u_1} (motive : Nat → List α → Sort u_2) (n✝ : Nat) (xs✝ : List α) + (h_1 : (x : List α) → motive 0 x) (h_2 : (n : Nat) → motive n.succ []) + (h_3 : (n : Nat) → (a : α) → (as : List α) → motive n.succ (a :: as)) : motive n✝ xs✝ +-/ +#guard_msgs(pass trace, all) in +#check take.match_1 + +/-- +info: take.match_1.congr_eq_1.{u_1, u_2} {α : Type u_1} (motive : Nat → List α → Sort u_2) (n✝ : Nat) (xs✝ : List α) + (h_1 : (x : List α) → motive 0 x) (h_2 : (n : Nat) → motive n.succ []) + (h_3 : (n : Nat) → (a : α) → (as : List α) → motive n.succ (a :: as)) (x✝ : List α) (heq_1 : n✝ = 0) + (heq_2 : xs✝ = x✝) : + HEq + (match n✝, xs✝ with + | 0, x => h_1 x + | n.succ, [] => h_2 n + | n.succ, a :: as => h_3 n a as) + (h_1 x✝) +-/ +#guard_msgs(pass trace, all) in #check take.match_1.congr_eq_1 + +def matchOptionUnit (o? : Option Unit) : Bool := Id.run do + if let some _ := o? then + true + else + false + +/-- +info: matchOptionUnit.match_1.congr_eq_1.{u_1} (motive : Option Unit → Sort u_1) (o?✝ : Option Unit) + (h_1 : (val : Unit) → motive (some val)) (h_2 : (x : Option Unit) → motive x) (val✝ : Unit) + (heq_1 : o?✝ = some val✝) : + HEq + (match o?✝ with + | some val => h_1 () + | x => h_2 x) + (h_1 val✝) +-/ +#guard_msgs(pass trace, all) in +#check matchOptionUnit.match_1.congr_eq_1 + +set_option linter.unusedVariables false in +partial def utf16PosToCodepointPosFromAux (s : String) : Nat → String.Pos → Nat → Bool + | 0, _, cp => true + | utf16pos, utf8pos, cp => false + +/-- +info: utf16PosToCodepointPosFromAux.match_1.congr_eq_1.{u_1} (motive : Nat → String.Pos → Nat → Sort u_1) (x✝ : Nat) + (x✝¹ : String.Pos) (x✝² : Nat) (h_1 : (x : String.Pos) → (cp : Nat) → motive 0 x cp) + (h_2 : (utf16pos : Nat) → (utf8pos : String.Pos) → (cp : Nat) → motive utf16pos utf8pos cp) (x✝³ : String.Pos) + (cp : Nat) (heq_1 : x✝ = 0) (heq_2 : x✝¹ = x✝³) (heq_3 : x✝² = cp) : + HEq + (match x✝, x✝¹, x✝² with + | 0, x, cp => h_1 x cp + | utf16pos, utf8pos, cp => h_2 utf16pos utf8pos cp) + (h_1 x✝³ cp) +-/ +#guard_msgs(pass trace, all) in +#check utf16PosToCodepointPosFromAux.match_1.congr_eq_1 + +opaque some_expr : Option Nat +def wrongEq (m? : Option Nat) (h : some_expr = m?) + (w : 0 < m?.getD 0) : Bool := by + match m?, w with + | some m?, _ => exact true + +/-- +info: wrongEq.match_1.congr_eq_1.{u_1} (motive : (m? : Option Nat) → 0 < m?.getD 0 → some_expr = m? → Sort u_1) + (m?✝ : Option Nat) (w✝ : 0 < m?✝.getD 0) (h : some_expr = m?✝) + (h_1 : (m? : Nat) → (x : 0 < (some m?).getD 0) → (h : some_expr = some m?) → motive (some m?) x h) (m? : Nat) + (x✝ : 0 < (some m?).getD 0) (h✝ : some_expr = some m?) (heq_1 : m?✝ = some m?) (heq_2 : HEq w✝ x✝) + (heq_3 : HEq h h✝) : + HEq + (match m?✝, w✝, h with + | some m?, x, h => h_1 m? x h) + (h_1 m? x✝ h✝) +-/ +#guard_msgs(pass trace, all) in #check wrongEq.match_1.congr_eq_1 + +set_option linter.unusedVariables false in +noncomputable def myNamedPatternTest (x : List Bool) : Bool := + match hx : x with + | x'@hx':(x::xs) => false + | x' => true + +/-- +info: myNamedPatternTest.match_1.congr_eq_1.{u_1} (motive : List Bool → Sort u_1) (x✝ : List Bool) + (h_1 : (x' : List Bool) → (x : Bool) → (xs : List Bool) → x' = x :: xs → x✝ = x :: xs → motive (x :: xs)) + (h_2 : (x' : List Bool) → x✝ = x' → motive x') (x : Bool) (xs : List Bool) (heq_1 : x✝ = x :: xs) : + HEq + (match hx : x✝ with + | x'@hx':(x :: xs) => h_1 x' x xs hx' hx + | x' => h_2 x' hx) + (h_1 (x :: xs) x xs ⋯ heq_1) +-/ +#guard_msgs(pass trace, all) in +#check myNamedPatternTest.match_1.congr_eq_1 + +set_option linter.unusedVariables false in +def testMe (n : Nat) : Bool := + match _ : n - 2 with + | 0 => true + | m => false + +/-- +info: testMe.match_1.congr_eq_2.{u_1} (motive : Nat → Sort u_1) (x✝ : Nat) (h_1 : x✝ = 0 → motive 0) + (h_2 : (m : Nat) → x✝ = m → motive m) (m : Nat) (heq_1 : x✝ = m) : + (m = 0 → False) → + HEq + (match h : x✝ with + | 0 => h_1 h + | m => h_2 m h) + (h_2 m heq_1) +-/ +#guard_msgs(pass trace, all) in +#check testMe.match_1.congr_eq_2 + +-- JFR: Code to check if all matchers with equations also have congruence equations +/- +open Lean Meta in +run_meta do + -- if false do -- comment this line to run the test on all matchers in the environment + let s := Lean.Meta.Match.Extension.extension.getState (← getEnv) (asyncMode := .local) + for (k,_) in s.map do --, _ in [:600] do + unless (`Lean).isPrefixOf (privateToUserName k) do + let mut ok := false + try + let _ ← Match.getEquationsFor k + ok := true + catch _ => + pure () + if ok then + try + let _ ← Lean.Meta.Match.Match.gendMatchCongrEqns k + catch e => + logError m!"failed to generate equations for {k} in {.ofConstName k.getPrefix}\n{indentD e.toMessageData}" +-/