feat: congruence equations for matchers (#8284)
This PR adds a new variant of equations for matchers, namely “congruence equations” that generalize the normal matcher equations. They have unrestricted left-hand-sides, extra equality assumptions relating the discriminiants with the patterns and thus prove heterogenous equalities. In that sense they combine congruence with rewriting. They can be used to rewrite matcher applications where, due to dependencies, `simp` would fail to rewrite the discriminants, and will be used when producing the unfolding induction theorems.
This commit is contained in:
Joachim Breitner
GitHub
parent
ca73223d4c
commit
dc1a70fa43
3 changed files with 415 additions and 64 deletions
|
|
@ -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_<idx>` -/
|
||||
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
192
tests/lean/run/matchCongrEqns.lean
Normal file
192
tests/lean/run/matchCongrEqns.lean
Normal file
|
|
@ -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}"
|
||||
-/
|
||||
Loading…
Add table
Reference in a new issue