Lean4
/-- Generates a congruence lemma for a function `f` for `numArgs` of its arguments.
The only `Lean.Meta.CongrArgKind` kinds that appear in such a lemma
are `.eq`, `.heq`, and `.subsingletonInst`.
The resulting lemma proves either an `Eq` or a `HEq` depending on whether the types
of the LHS and RHS are equal or not.
This function is a wrapper around `Lean.Meta.mkHCongrWithArity`.
It transforms the resulting congruence lemma by trying to automatically prove hypotheses
using subsingleton lemmas, and if they are so provable they are recorded with `.subsingletonInst`.
Note that this is slightly abusing `.subsingletonInst` since
(1) the argument might not be for a `Decidable` instance and
(2) the argument might not even be an instance. -/
def mkHCongrWithArity' (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
let thm ← mkHCongrWithArity f numArgs
process thm thm.type thm.argKinds.toList #[] #[] #[] #[]
where
/-- Process the congruence theorem by trying to pre-prove arguments using `prove`.
- `cthm` is the original `CongrTheorem`, modified only after visiting every argument.
- `type` is type of the congruence theorem, after all the parameters so far have been applied.
- `argKinds` is the list of `CongrArgKind`s, which this function recurses on.
- `argKinds'` is the accumulated array of `CongrArgKind`s, which is the original array but
with some kinds replaced by `.subsingletonInst`.
- `params` is the *new* list of parameters, as fvars that need to be abstracted at the end.
- `args` is the list of arguments (fvars) to supply to `cthm.proof` before abstracting `params`.
- `letArgs` records `(fvar, expr)` assignments for each `fvar` that was solved for by `prove`.
-/
process (cthm : CongrTheorem) (type : Expr) (argKinds : List CongrArgKind) (argKinds' : Array CongrArgKind)
(params args : Array Expr) (letArgs : Array (Expr × Expr)) : MetaM CongrTheorem := do
match argKinds with
| [] =>
if letArgs.isEmpty then
-- Then we didn't prove anything, so we can use the CongrTheorem as-is.
return cthm
else
let proof :=
letArgs.foldr (init := mkAppN cthm.proof args)
(fun (fvar, val) proof => (proof.abstract #[fvar]).instantiate1 val)
let pf' ← mkLambdaFVars params proof
return { proof := pf', type := ← inferType pf', argKinds := argKinds' }
| argKind :: argKinds =>
match argKind with
| .eq | .heq =>
forallBoundedTelescope type (some 3) fun params' type' => do
let #[x, y, eq] := params' |
unreachable!
-- See if we can prove `Eq` from previous parameters.
let g := (← mkFreshExprMVar (← inferType eq)).mvarId!
let g ← g.clear eq.fvarId!
if (← observing? <| prove g args).isSome then
let eqPf ← instantiateMVars (.mvar g)
process cthm type' argKinds (argKinds'.push .subsingletonInst) (params := params ++ #[x, y]) (args :=
args ++ params') (letArgs := letArgs.push (eq, eqPf))
else
process cthm type' argKinds (argKinds'.push argKind) (params := params ++ params') (args :=
args ++ params') (letArgs := letArgs)
| _ =>
panic! "Unexpected CongrArgKind"
/-- Close the goal given only the fvars in `params`, or else fails. -/
prove (g : MVarId) (params : Array Expr) : MetaM Unit := do
-- Prune the local context.
let g ← g.cleanup
let [g] ←
g.casesRec fun localDecl => do
return (localDecl.type.isEq || localDecl.type.isHEq) && params.contains localDecl.toExpr |
failure
try
g.refl;
return
catch _ =>
pure ()
try
g.hrefl;
return
catch _ =>
pure ()
if ← g.proofIrrelHeq then
return
-- Make the goal be an eq and then try `Subsingleton.elim`
let g ← g.heqOfEq
if ← g.subsingletonElim then
return
-- We have no more tricks.
failure
