Lean4
/-- Construct the `GCongrLemma` data from a given lemma. -/
def makeGCongrLemma (declName : Name) (declTy : Expr) (numHyps prio : Nat) : MetaM GCongrLemma := do
withReducible <|
forallBoundedTelescope declTy numHyps fun xs targetTy => do
let fail {α} (m : MessageData) : MetaM α :=
throwError "\
@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.\n \
{m } in the conclusion of {declTy}"
let some (relName, lhs, rhs) := getRel (← whnf targetTy) |
fail "No relation found"
let some (head, lhsArgs) := getCongrAppFnArgs lhs |
fail "LHS is not suitable for congruence"
let some (head', rhsArgs) := getCongrAppFnArgs rhs |
fail "RHS is not suitable for congruence"
unless head == head' && lhsArgs.size == rhsArgs.size do
fail "LHS and RHS do not have the same head function and arity"
let mut numVarying := 0
let mut pairs :=
#[]
-- iterate through each pair of corresponding (LHS/RHS) inputs to the head function `head` in
-- the conclusion of the lemma
for i in [:lhsArgs.size]do
let e1 := lhsArgs[i]!
let e2 :=
rhsArgs[i]!
-- we call such a pair a "varying argument" pair if the LHS/RHS inputs are not defeq
-- (and not proofs)
let isEq ← isDefEq e1 e2 <||> (isProof e1 <&&> isProof e2)
if !isEq then
-- verify that the "varying argument" pairs are free variables (after eta-reduction)
let .fvar e1 := e1.eta |
fail "Not all arguments are free variables"
let .fvar e2 := e2.eta |
fail
"Not all arguments are free variables"
-- add such a pair to the `pairs` array
pairs := pairs.push (i, e1, e2)
numVarying := numVarying + 1
if numVarying = 0 then
fail "LHS and RHS are the same"
let mut mainSubgoals := #[]
let mut i :=
0
-- iterate over antecedents `hyp` to the lemma
for hyp in xs do
mainSubgoals ←
forallTelescopeReducing (← inferType hyp) fun args hypTy => do
-- pull out the conclusion `hypTy` of the antecedent, and check whether it is of the form
-- `lhs₁ _ ... _ ≈ rhs₁ _ ... _` (for a possibly different relation `≈` than the relation
-- `rel` above)
let hypTy ← whnf hypTy
if let some (_, lhs₁, rhs₁) := getRel hypTy then
if let .fvar lhs₁ := lhs₁.getAppFn then
if let .fvar rhs₁ := rhs₁.getAppFn then
-- check whether `(lhs₁, rhs₁)` is in some order one of the "varying argument" pairs from
-- the conclusion to the lemma
if let some j :=
pairs.find? fun (_, e1, e2) => lhs₁ == e1 && rhs₁ == e2 || lhs₁ == e2 && rhs₁ == e1 then
-- if yes, record the index of this antecedent as a "main subgoal", together with the
-- index of the "varying argument" pair it corresponds to
return mainSubgoals.push (i, j.1, args.size)
else
-- now check whether `hypTy` is of the form `rhs₁ _ ... _`,
-- and whether the last hypothesis is of the form `lhs₁ _ ... _`.
if let .fvar rhs₁ := hypTy.getAppFn then
if let some lastFVar := args.back? then
if let .fvar lhs₁ := (← inferType lastFVar).getAppFn then
if let some j :=
pairs.find? fun (_, e1, e2) => lhs₁ == e1 && rhs₁ == e2 || lhs₁ == e2 && rhs₁ == e1 then
return mainSubgoals.push (i, j.1, args.size - 1)
return mainSubgoals
i :=
i +
1
-- store all the information from this parse of the lemma's structure in a `GCongrLemma`
let key := { relName, head, arity := lhsArgs.size }
return { key, declName, mainSubgoals, numHyps, prio, numVarying }
