diff --git a/src/Init.lean b/src/Init.lean index 9d0ca6d7ad16..7d3cbcd006ac 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -33,3 +33,4 @@ import Init.SizeOfLemmas import Init.BinderPredicates import Init.Ext import Init.Omega +import Init.Congr! diff --git a/src/Init/Congr!.lean b/src/Init/Congr!.lean new file mode 100644 index 000000000000..113f4568da84 --- /dev/null +++ b/src/Init/Congr!.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2023 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Init.RCases + +open Lean + +/-- +Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by +recursively applying congruence lemmas. For example, with `⊢ f as = g bs` we could get +two goals `⊢ f = g` and `⊢ as = bs`. + +Syntax: +``` +congr! +congr! n +congr! with x y z +congr! n with x y z +``` +Here, `n` is a natural number and `x`, `y`, `z` are `rintro` patterns (like `h`, `rfl`, `⟨x, y⟩`, +`_`, `-`, `(h | h)`, etc.). + +The `congr!` tactic is similar to `congr` but is more insistent in trying to equate left-hand sides +to right-hand sides of goals. Here is a list of things it can try: + +- If `R` in `⊢ R x y` is a reflexive relation, it will convert the goal to `⊢ x = y` if possible. + The list of reflexive relations is maintained using the `@[refl]` attribute. + As a special case, `⊢ p ↔ q` is converted to `⊢ p = q` during congruence processing and then + returned to `⊢ p ↔ q` form at the end. + +- If there is a user congruence lemma associated to the goal (for instance, a `@[congr]`-tagged + lemma applying to `⊢ List.map f xs = List.map g ys`), then it will use that. + +- It uses a congruence lemma generator at least as capable as the one used by `congr` and `simp`. + If there is a subexpression that can be rewritten by `simp`, then `congr!` should be able + to generate an equality for it. + +- It can do congruences of pi types using lemmas like `implies_congr` and `pi_congr`. + +- Before applying congruences, it will run the `intros` tactic automatically. + The introduced variables can be given names using a `with` clause. + This helps when congruence lemmas provide additional assumptions in hypotheses. + +- When there is an equality between functions, so long as at least one is obviously a lambda, we + apply `funext` or `hfunext`, which allows for congruence of lambda bodies. + +- It can try to close goals using a few strategies, including checking + definitional equality, trying to apply `Subsingleton.elim` or `proof_irrel_heq`, and using the + `assumption` tactic. + +The optional parameter is the depth of the recursive applications. +This is useful when `congr!` is too aggressive in breaking down the goal. +For example, given `⊢ f (g (x + y)) = f (g (y + x))`, +`congr!` produces the goals `⊢ x = y` and `⊢ y = x`, +while `congr! 2` produces the intended `⊢ x + y = y + x`. + +The `congr!` tactic also takes a configuration option, for example +```lean +congr! (config := {transparency := .default}) 2 +``` +This overrides the default, which is to apply congruence lemmas at reducible transparency. + +The `congr!` tactic is aggressive with equating two sides of everything. There is a predefined +configuration that uses a different strategy: +Try +```lean +congr! (config := .unfoldSameFun) +``` +This only allows congruences between functions applications of definitionally equal functions, +and it applies congruence lemmas at default transparency (rather than just reducible). +This is somewhat like `congr`. + +See `Congr!.Config` for all options. +-/ +syntax (name := congr!) "congr!" (Parser.Tactic.config)? (ppSpace num)? + (" with" (ppSpace colGt rintroPat)*)? : tactic diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 010795552732..8eafe467e667 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -26,6 +26,20 @@ set_option linter.missingDocs true -- keep it documented theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by cases propext (iff_of_true hp hq); rfl +theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by + cases propext (iff_of_true hp hq); rfl + +theorem hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : ∀a, β a} {f' : ∀a, β' a} + (hα : α = α') (h : ∀a a', HEq a a' → HEq (f a) (f' a')) : HEq f f' := by + subst hα + have : ∀a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a) + have : β = β' := by funext a + exact type_eq_of_heq (this a) + subst this + apply heq_of_eq + funext a + exact eq_of_heq (this a) + /-! ## not -/ theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl)) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 852bfb7a0911..9987eb70d16c 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -45,7 +45,7 @@ theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) := implies_dep_congr_ctx h₁ h₂ -theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) := +theorem forall_congr {α : Sort u} {p q : α → Sort v} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) := (funext h : p = q) ▸ rfl theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index ee564806aeb1..6bd50d62b7b6 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -958,7 +958,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`. -/ syntax (name := congr) "congr" (ppSpace num)? : tactic - /-- In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for: ``` diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 493b2e46bd44..86469442fe13 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -39,3 +39,4 @@ import Lean.Elab.Tactic.SolveByElim import Lean.Elab.Tactic.LibrarySearch import Lean.Elab.Tactic.ShowTerm import Lean.Elab.Tactic.Rfl +import Lean.Elab.Tactic.Congr! diff --git a/src/Lean/Elab/Tactic/Congr!.lean b/src/Lean/Elab/Tactic/Congr!.lean new file mode 100644 index 000000000000..96ed50a7e64b --- /dev/null +++ b/src/Lean/Elab/Tactic/Congr!.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2023 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Init.Congr! +import Lean.Meta.Tactic.Congr! + +/-! +# The `congr!` tactic + +This is a more powerful version of the `congr` tactic that knows about more congruence lemmas and +can apply to more situations. It is similar to the `congr'` tactic from Mathlib 3. + +The `congr!` tactic is used by the `convert` and `convert_to` tactics. + +See the syntax docstring for more details. +-/ + +open Lean Elab Tactic Meta.Tactic.Congr! + +namespace Lean.Elab.Tactic + +declare_config_elab elabConfig Config + +@[builtin_tactic «congr!»] def evalCongr! : Tactic := fun stx => + match stx with + | `(tactic| congr! $[$cfg:config]? $[$n]? $[with $ps?*]?) => do + let config ← elabConfig (mkOptionalNode cfg) + let patterns := (Lean.Elab.Tactic.RCases.expandRIntroPats (ps?.getD #[])).toList + liftMetaTactic fun g ↦ + let depth := n.map (·.getNat) + g.congrN! depth config patterns + | _ => throwUnsupportedSyntax + +end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/Congr.lean b/src/Lean/Elab/Tactic/Congr.lean index bbfab37d537b..02a2994ef303 100644 --- a/src/Lean/Elab/Tactic/Congr.lean +++ b/src/Lean/Elab/Tactic/Congr.lean @@ -9,7 +9,6 @@ import Lean.Elab.Tactic.Basic namespace Lean.Elab.Tactic -namespace Lean.Elab.Tactic @[builtin_tactic Parser.Tactic.congr] def evalCongr : Tactic := fun stx => match stx with | `(tactic| congr $[$n?]?) => @@ -19,5 +18,3 @@ namespace Lean.Elab.Tactic | _ => throwUnsupportedSyntax end Lean.Elab.Tactic - - diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 9060bd91d650..b20f3f5dbefd 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -176,6 +176,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : let lhs := (← instantiateMVars lhs).cleanupAnnotations if let .forallE n d b bi := lhs then let u ← getLevel d + let v ← getLevel b let p : Expr := .lam n d b bi let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do @@ -187,7 +188,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : unless (← isDefEqGuarded rhs rhs') do throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" return (q, h, mvarNew) - let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h + let proof := mkApp4 (mkConst ``forall_congr [u, v]) d p q h mvarId.assign proof return mvarNew.mvarId! else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then diff --git a/src/Lean/Elab/Tactic/Rfl.lean b/src/Lean/Elab/Tactic/Rfl.lean index 0ade703419e2..705f6a763f65 100644 --- a/src/Lean/Elab/Tactic/Rfl.lean +++ b/src/Lean/Elab/Tactic/Rfl.lean @@ -16,13 +16,6 @@ provided the reflexivity lemma has been marked as `@[refl]`. namespace Lean.Elab.Tactic.Rfl -/-- -This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive -relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]. --/ -elab_rules : tactic - | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl) - @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx => match stx with | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl) diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 498e2f9bf943..ab59111b2b2b 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -4,329 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Meta.AppBuilder -import Lean.Class - -namespace Lean.Meta - -inductive CongrArgKind where - /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/ - | fixed - /-- - It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. - This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ - | fixedNoParam - /-- - The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`. - `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/ - | eq - /-- - The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. - They correspond to arguments that are subsingletons/propositions. -/ - | cast - /-- - The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. - `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ - | heq - /-- - For congr-simp theorems only. Indicates a decidable instance argument. - The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ - | subsingletonInst - deriving Inhabited, Repr - -structure CongrTheorem where - type : Expr - proof : Expr - argKinds : Array CongrArgKind - -private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do - let mut lctx := lctx - for y in ys do - let decl := lctx.getFVar! y - lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'") - return lctx - -private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do - let mut lctx := lctx - for y in ys do - let decl := lctx.getFVar! y - lctx := lctx.setBinderInfo decl.fvarId BinderInfo.default - return lctx - -partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do - let fType ← inferType f - forallBoundedTelescope fType numArgs fun xs _ => - forallBoundedTelescope fType numArgs fun ys _ => do - if xs.size != numArgs then - throwError "failed to generate hcongr theorem, insufficient number of arguments" - else - let lctx := addPrimeToFVarUserNames ys (← getLCtx) |> setBinderInfosD ys |> setBinderInfosD xs - withLCtx lctx (← getLocalInstances) do - withNewEqs xs ys fun eqs argKinds => do - let mut hs := #[] - for x in xs, y in ys, eq in eqs do - hs := hs.push x |>.push y |>.push eq - let lhs := mkAppN f xs - let rhs := mkAppN f ys - let congrType ← mkForallFVars hs (← mkHEq lhs rhs) - return { - type := congrType - proof := (← mkProof congrType) - argKinds - } -where - withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α := - let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do - if i < xs.size then - let x := xs[i]! - let y := ys[i]! - let xType := (← inferType x).consumeTypeAnnotations - let yType := (← inferType y).consumeTypeAnnotations - if xType == yType then - withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h => - loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq) - else - withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkHEq x y) fun h => - loop (i+1) (eqs.push h) (kinds.push CongrArgKind.heq) - else - k eqs kinds - loop 0 #[] #[] - - mkProof (type : Expr) : MetaM Expr := do - if let some (_, lhs, _) := type.eq? then - mkEqRefl lhs - else if let some (_, lhs, _, _) := type.heq? then - mkHEqRefl lhs - else - forallBoundedTelescope type (some 1) fun a type => - let a := a[0]! - forallBoundedTelescope type (some 1) fun b motive => - let b := b[0]! - let type := type.bindingBody!.instantiate1 a - withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do - let type := type.bindingBody! - let motive := motive.bindingBody! - let minor ← mkProof type - let mut major := eqPr - if (← whnf (← inferType eqPr)).isHEq then - major ← mkEqOfHEq major - let motive ← mkLambdaFVars #[b] motive - mkLambdaFVars #[a, b, eqPr] (← mkEqNDRec motive minor major) - -def mkHCongr (f : Expr) : MetaM CongrTheorem := do - mkHCongrWithArity f (← getFunInfo f).getArity - -/-- - Ensure that all dependencies for `congr_arg_kind::Eq` are `congr_arg_kind::Fixed`. --/ -private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do - let mut kinds := kinds - for i in [:info.paramInfo.size] do - for j in [i+1:info.paramInfo.size] do - if info.paramInfo[j]!.backDeps.contains i then - if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then - -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed. - kinds := kinds.set! i CongrArgKind.fixed - break - return kinds - -/-- - (Try to) cast expression `e` to the given type using the equations `eqs`. - `deps` contains the indices of the relevant equalities. - Remark: deps is sorted. -/ -private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do - let rec go (i : Nat) (type : Expr) : MetaM Expr := do - if i < deps.size then - match eqs[deps[i]!]! with - | none => go (i+1) type - | some major => - let some (_, lhs, rhs) := (← inferType major).eq? | unreachable! - if (← dependsOn type major.fvarId!) then - let motive ← mkLambdaFVars #[rhs, major] type - let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs) - let minor ← go (i+1) typeNew - mkEqRec motive minor major - else - let motive ← mkLambdaFVars #[rhs] type - let typeNew := type.replaceFVar rhs lhs - let minor ← go (i+1) typeNew - mkEqNDRec motive minor major - else - return e - go 0 type - -private def hasCastLike (kinds : Array CongrArgKind) : Bool := - kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst - -private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do - forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type - -/-- - Test whether we should use `subsingletonInst` kind for instances which depend on `eq`. - (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/ -private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do - if info.paramInfo[i]!.isDecInst then - for j in info.paramInfo[i]!.backDeps do - if kinds[j]! matches CongrArgKind.eq then - return true - return false - -/-- -If `f` is a class constructor, return a bitmask `m` s.t. `m[i]` is true if the `i`-th parameter -corresponds to a subobject field. - -We use this function to implement the special support for class constructors at `getCongrSimpKinds`. -See issue #1808 --/ -private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := do - let .const declName _ := f | return none - let .ctorInfo val ← getConstInfo declName | return none - unless isClass (← getEnv) val.induct do return none - forallTelescopeReducing val.type fun xs _ => do - let env ← getEnv - let mut mask := #[] - for i in [:xs.size] do - if i < val.numParams then - mask := mask.push false - else - let localDecl ← xs[i]!.fvarId!.getDecl - mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome - return some mask - -/-- Compute `CongrArgKind`s for a simp congruence theorem. -/ -def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) := do - /- - The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this - argument. However, if there are references from `i` to `j`, we cannot - rewrite both `i` and `j`. So we must change the `CongrArgKind` at - either `i` or `j`. In principle, if there is a dependency with `i` - appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is - an optimization: if `i` is a subsingleton, we can fix it instead of - `j`, since all subsingletons are equal anyway. The fixing happens in - two loops: one for the special cases, and one for the general case. - - This method has special support for class constructors. - For this kind of function, we treat subobject fields as regular parameters instead of instance implicit ones. - We added this feature because of issue #1808 - -/ - let mut result := #[] - let mask? ← getClassSubobjectMask? f - for i in [:info.paramInfo.size] do - if info.resultDeps.contains i then - result := result.push .fixed - else if info.paramInfo[i]!.isProp then - result := result.push .cast - else if info.paramInfo[i]!.isInstImplicit then - if let some mask := mask? then - if h : i < mask.size then - if mask[i] then - -- Parameter is a subobect field of a class constructor. See comment above. - result := result.push .eq - continue - if shouldUseSubsingletonInst info result i then - result := result.push .subsingletonInst - else - result := result.push .fixed - else - result := result.push .eq - return fixKindsForDependencies info result - -/-- - Create a congruence theorem that is useful for the simplifier and `congr` tactic. --/ -partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do - if let some result ← mk? f info kinds then - return some result - else if hasCastLike kinds then - -- Simplify kinds and try again - let kinds := kinds.map fun kind => - if kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst then CongrArgKind.fixed else kind - mk? f info kinds - else - return none -where - /-- - Create a congruence theorem that is useful for the simplifier. - In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem - contains an input `a_i` representing the i-th argument in the left-hand-side, and - it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side. - The idea is that the right-hand-side of this theorem "tells" the simplifier - how the resulting term looks like. -/ - mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do - try - let fType ← inferType f - forallBoundedTelescope fType kinds.size fun lhss _ => do - if lhss.size != kinds.size then return none - let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do - if i == kinds.size then - let lhs := mkAppN f lhss - let rhs := mkAppN f rhss - let type ← mkForallFVars hyps (← mkEq lhs rhs) - let proof ← mkProof type kinds - return { type, proof, argKinds := kinds } - else - let hyps := hyps.push lhss[i]! - match kinds[i]! with - | .heq | .fixedNoParam => unreachable! - | .eq => - let localDecl ← lhss[i]!.fvarId!.getDecl - withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do - withLocalDeclD (localDecl.userName.appendBefore "e_") (← mkEq lhss[i]! rhs) fun eq => do - go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq) - | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps - | .cast => - let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss - let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs - go (i+1) (rhss.push rhs) (eqs.push none) hyps - | .subsingletonInst => - -- The `lhs` does not need to instance implicit since it can be inferred from the LHS - withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do - let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss - let rhsBi := if subsingletonInstImplicitRhs then .instImplicit else .implicit - withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs => - go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs) - return some (← go 0 #[] #[] #[]) - catch _ => - return none - - mkProof (type : Expr) (kinds : Array CongrArgKind) : MetaM Expr := do - let rec go (i : Nat) (type : Expr) : MetaM Expr := do - if i == kinds.size then - let some (_, lhs, _) := type.eq? | unreachable! - mkEqRefl lhs - else - withNext type fun lhs type => do - match kinds[i]! with - | .heq | .fixedNoParam => unreachable! - | .fixed => mkLambdaFVars #[lhs] (← go (i+1) type) - | .cast => mkLambdaFVars #[lhs] (← go (i+1) type) - | .eq => - let typeSub := type.bindingBody!.bindingBody!.instantiate #[(← mkEqRefl lhs), lhs] - withNext type fun rhs type => - withNext type fun heq type => do - let motive ← mkLambdaFVars #[rhs, heq] type - let proofSub ← go (i+1) typeSub - mkLambdaFVars #[lhs, rhs, heq] (← mkEqRec motive proofSub heq) - | .subsingletonInst => - let typeSub := type.bindingBody!.instantiate #[lhs] - withNext type fun rhs type => do - let motive ← mkLambdaFVars #[rhs] type - let proofSub ← go (i+1) typeSub - let heq ← mkAppM ``Subsingleton.elim #[lhs, rhs] - mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq) - go 0 type - -/-- -Create a congruence theorem for `f`. The theorem is used in the simplifier. - -If `subsingletonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters -is marked as instance implicit. It forces the simplifier to compute the new instance when applying -the congruence theorem. -For the `congr` tactic we set it to `false`. --/ -def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do - let f := (← instantiateMVars f).cleanupAnnotations - let info ← getFunInfo f - mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs) - -end Lean.Meta +import Lean.Meta.CongrTheorems.Basic +import Lean.Meta.CongrTheorems.Rich diff --git a/src/Lean/Meta/CongrTheorems/Basic.lean b/src/Lean/Meta/CongrTheorems/Basic.lean new file mode 100644 index 000000000000..498e2f9bf943 --- /dev/null +++ b/src/Lean/Meta/CongrTheorems/Basic.lean @@ -0,0 +1,332 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Meta.AppBuilder +import Lean.Class + +namespace Lean.Meta + +inductive CongrArgKind where + /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/ + | fixed + /-- + It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. + This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/ + | fixedNoParam + /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/ + | eq + /-- + The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. + They correspond to arguments that are subsingletons/propositions. -/ + | cast + /-- + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. + `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ + | heq + /-- + For congr-simp theorems only. Indicates a decidable instance argument. + The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ + | subsingletonInst + deriving Inhabited, Repr + +structure CongrTheorem where + type : Expr + proof : Expr + argKinds : Array CongrArgKind + +private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do + let mut lctx := lctx + for y in ys do + let decl := lctx.getFVar! y + lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'") + return lctx + +private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run do + let mut lctx := lctx + for y in ys do + let decl := lctx.getFVar! y + lctx := lctx.setBinderInfo decl.fvarId BinderInfo.default + return lctx + +partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do + let fType ← inferType f + forallBoundedTelescope fType numArgs fun xs _ => + forallBoundedTelescope fType numArgs fun ys _ => do + if xs.size != numArgs then + throwError "failed to generate hcongr theorem, insufficient number of arguments" + else + let lctx := addPrimeToFVarUserNames ys (← getLCtx) |> setBinderInfosD ys |> setBinderInfosD xs + withLCtx lctx (← getLocalInstances) do + withNewEqs xs ys fun eqs argKinds => do + let mut hs := #[] + for x in xs, y in ys, eq in eqs do + hs := hs.push x |>.push y |>.push eq + let lhs := mkAppN f xs + let rhs := mkAppN f ys + let congrType ← mkForallFVars hs (← mkHEq lhs rhs) + return { + type := congrType + proof := (← mkProof congrType) + argKinds + } +where + withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α := + let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do + if i < xs.size then + let x := xs[i]! + let y := ys[i]! + let xType := (← inferType x).consumeTypeAnnotations + let yType := (← inferType y).consumeTypeAnnotations + if xType == yType then + withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h => + loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq) + else + withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkHEq x y) fun h => + loop (i+1) (eqs.push h) (kinds.push CongrArgKind.heq) + else + k eqs kinds + loop 0 #[] #[] + + mkProof (type : Expr) : MetaM Expr := do + if let some (_, lhs, _) := type.eq? then + mkEqRefl lhs + else if let some (_, lhs, _, _) := type.heq? then + mkHEqRefl lhs + else + forallBoundedTelescope type (some 1) fun a type => + let a := a[0]! + forallBoundedTelescope type (some 1) fun b motive => + let b := b[0]! + let type := type.bindingBody!.instantiate1 a + withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do + let type := type.bindingBody! + let motive := motive.bindingBody! + let minor ← mkProof type + let mut major := eqPr + if (← whnf (← inferType eqPr)).isHEq then + major ← mkEqOfHEq major + let motive ← mkLambdaFVars #[b] motive + mkLambdaFVars #[a, b, eqPr] (← mkEqNDRec motive minor major) + +def mkHCongr (f : Expr) : MetaM CongrTheorem := do + mkHCongrWithArity f (← getFunInfo f).getArity + +/-- + Ensure that all dependencies for `congr_arg_kind::Eq` are `congr_arg_kind::Fixed`. +-/ +private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do + let mut kinds := kinds + for i in [:info.paramInfo.size] do + for j in [i+1:info.paramInfo.size] do + if info.paramInfo[j]!.backDeps.contains i then + if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then + -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed. + kinds := kinds.set! i CongrArgKind.fixed + break + return kinds + +/-- + (Try to) cast expression `e` to the given type using the equations `eqs`. + `deps` contains the indices of the relevant equalities. + Remark: deps is sorted. -/ +private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do + let rec go (i : Nat) (type : Expr) : MetaM Expr := do + if i < deps.size then + match eqs[deps[i]!]! with + | none => go (i+1) type + | some major => + let some (_, lhs, rhs) := (← inferType major).eq? | unreachable! + if (← dependsOn type major.fvarId!) then + let motive ← mkLambdaFVars #[rhs, major] type + let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs) + let minor ← go (i+1) typeNew + mkEqRec motive minor major + else + let motive ← mkLambdaFVars #[rhs] type + let typeNew := type.replaceFVar rhs lhs + let minor ← go (i+1) typeNew + mkEqNDRec motive minor major + else + return e + go 0 type + +private def hasCastLike (kinds : Array CongrArgKind) : Bool := + kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst + +private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do + forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type + +/-- + Test whether we should use `subsingletonInst` kind for instances which depend on `eq`. + (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/ +private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do + if info.paramInfo[i]!.isDecInst then + for j in info.paramInfo[i]!.backDeps do + if kinds[j]! matches CongrArgKind.eq then + return true + return false + +/-- +If `f` is a class constructor, return a bitmask `m` s.t. `m[i]` is true if the `i`-th parameter +corresponds to a subobject field. + +We use this function to implement the special support for class constructors at `getCongrSimpKinds`. +See issue #1808 +-/ +private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := do + let .const declName _ := f | return none + let .ctorInfo val ← getConstInfo declName | return none + unless isClass (← getEnv) val.induct do return none + forallTelescopeReducing val.type fun xs _ => do + let env ← getEnv + let mut mask := #[] + for i in [:xs.size] do + if i < val.numParams then + mask := mask.push false + else + let localDecl ← xs[i]!.fvarId!.getDecl + mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome + return some mask + +/-- Compute `CongrArgKind`s for a simp congruence theorem. -/ +def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) := do + /- + The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this + argument. However, if there are references from `i` to `j`, we cannot + rewrite both `i` and `j`. So we must change the `CongrArgKind` at + either `i` or `j`. In principle, if there is a dependency with `i` + appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is + an optimization: if `i` is a subsingleton, we can fix it instead of + `j`, since all subsingletons are equal anyway. The fixing happens in + two loops: one for the special cases, and one for the general case. + + This method has special support for class constructors. + For this kind of function, we treat subobject fields as regular parameters instead of instance implicit ones. + We added this feature because of issue #1808 + -/ + let mut result := #[] + let mask? ← getClassSubobjectMask? f + for i in [:info.paramInfo.size] do + if info.resultDeps.contains i then + result := result.push .fixed + else if info.paramInfo[i]!.isProp then + result := result.push .cast + else if info.paramInfo[i]!.isInstImplicit then + if let some mask := mask? then + if h : i < mask.size then + if mask[i] then + -- Parameter is a subobect field of a class constructor. See comment above. + result := result.push .eq + continue + if shouldUseSubsingletonInst info result i then + result := result.push .subsingletonInst + else + result := result.push .fixed + else + result := result.push .eq + return fixKindsForDependencies info result + +/-- + Create a congruence theorem that is useful for the simplifier and `congr` tactic. +-/ +partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do + if let some result ← mk? f info kinds then + return some result + else if hasCastLike kinds then + -- Simplify kinds and try again + let kinds := kinds.map fun kind => + if kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst then CongrArgKind.fixed else kind + mk? f info kinds + else + return none +where + /-- + Create a congruence theorem that is useful for the simplifier. + In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem + contains an input `a_i` representing the i-th argument in the left-hand-side, and + it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side. + The idea is that the right-hand-side of this theorem "tells" the simplifier + how the resulting term looks like. -/ + mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do + try + let fType ← inferType f + forallBoundedTelescope fType kinds.size fun lhss _ => do + if lhss.size != kinds.size then return none + let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do + if i == kinds.size then + let lhs := mkAppN f lhss + let rhs := mkAppN f rhss + let type ← mkForallFVars hyps (← mkEq lhs rhs) + let proof ← mkProof type kinds + return { type, proof, argKinds := kinds } + else + let hyps := hyps.push lhss[i]! + match kinds[i]! with + | .heq | .fixedNoParam => unreachable! + | .eq => + let localDecl ← lhss[i]!.fvarId!.getDecl + withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do + withLocalDeclD (localDecl.userName.appendBefore "e_") (← mkEq lhss[i]! rhs) fun eq => do + go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq) + | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps + | .cast => + let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss + let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs + go (i+1) (rhss.push rhs) (eqs.push none) hyps + | .subsingletonInst => + -- The `lhs` does not need to instance implicit since it can be inferred from the LHS + withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do + let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss + let rhsBi := if subsingletonInstImplicitRhs then .instImplicit else .implicit + withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs => + go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs) + return some (← go 0 #[] #[] #[]) + catch _ => + return none + + mkProof (type : Expr) (kinds : Array CongrArgKind) : MetaM Expr := do + let rec go (i : Nat) (type : Expr) : MetaM Expr := do + if i == kinds.size then + let some (_, lhs, _) := type.eq? | unreachable! + mkEqRefl lhs + else + withNext type fun lhs type => do + match kinds[i]! with + | .heq | .fixedNoParam => unreachable! + | .fixed => mkLambdaFVars #[lhs] (← go (i+1) type) + | .cast => mkLambdaFVars #[lhs] (← go (i+1) type) + | .eq => + let typeSub := type.bindingBody!.bindingBody!.instantiate #[(← mkEqRefl lhs), lhs] + withNext type fun rhs type => + withNext type fun heq type => do + let motive ← mkLambdaFVars #[rhs, heq] type + let proofSub ← go (i+1) typeSub + mkLambdaFVars #[lhs, rhs, heq] (← mkEqRec motive proofSub heq) + | .subsingletonInst => + let typeSub := type.bindingBody!.instantiate #[lhs] + withNext type fun rhs type => do + let motive ← mkLambdaFVars #[rhs] type + let proofSub ← go (i+1) typeSub + let heq ← mkAppM ``Subsingleton.elim #[lhs, rhs] + mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq) + go 0 type + +/-- +Create a congruence theorem for `f`. The theorem is used in the simplifier. + +If `subsingletonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters +is marked as instance implicit. It forces the simplifier to compute the new instance when applying +the congruence theorem. +For the `congr` tactic we set it to `false`. +-/ +def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do + let f := (← instantiateMVars f).cleanupAnnotations + let info ← getFunInfo f + mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs) + +end Lean.Meta diff --git a/src/Lean/Meta/CongrTheorems/Rich.lean b/src/Lean/Meta/CongrTheorems/Rich.lean new file mode 100644 index 000000000000..1fd6a3945042 --- /dev/null +++ b/src/Lean/Meta/CongrTheorems/Rich.lean @@ -0,0 +1,266 @@ +/- +Copyright (c) 2023 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Lean.Meta.CongrTheorems.Basic +import Lean.Meta.Tactic.Apply +import Lean.Meta.Tactic.Cleanup +import Lean.Meta.Tactic.Cases +import Lean.Meta.Tactic.Refl +import Lean.Class + +namespace Lean.Meta + +initialize registerTraceClass `Meta.CongrTheorems + +/-- 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`. -/ + process (cthm : CongrTheorem) (type : Expr) (argKinds : List CongrArgKind) + (argKinds' : Array CongrArgKind) (params args : Array Expr) : MetaM CongrTheorem := do + match argKinds with + | [] => + if params.size == args.size then + return cthm + else + let pf' ← mkLambdaFVars params (mkAppN cthm.proof args) + 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 params).isSome then + process cthm type' argKinds (argKinds'.push .subsingletonInst) + (params := params ++ #[x, y]) (args := args ++ #[x, y, .mvar g]) + else + process cthm type' argKinds (argKinds'.push argKind) + (params := params ++ params') (args := args ++ params') + | _ => 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 + -- Substitute equalities that come from only this congruence lemma. + 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 + +/-- +`mkRichHCongr fType funInfo fixedFun fixedParams forceHEq` +create a congruence lemma to prove that `Eq/HEq (f a₁ ... aₙ) (f' a₁' ... aₙ')`. +The functions have type `fType` and the number of arguments is governed by the `funInfo` data. +Each argument produces an `Eq/HEq aᵢ aᵢ'` hypothesis, but we also provide these hypotheses +the additional facts that the preceding equalities have been proved (unlike in `mkHCongrWithArity`). +The first two arguments of the resulting theorem are for `f` and `f'`, followed by a proof +of `f = f'`, unless `fixedFun` is `true` (see below). + +When including hypotheses about previous hypotheses, we make use of dependency information +and only include relevant equalities. + +The argument `fty` denotes the type of `f`. The arity of the resulting congruence lemma is +controlled by the size of the `info` array. + +For the purpose of generating nicer lemmas (to help `to_additive` for example), +this function supports generating lemmas where certain parameters +are meant to be fixed: + +* If `fixedFun` is `false` (the default) then the lemma starts with three arguments for `f`, `f'`, +and `h : f = f'`. Otherwise, if `fixedFun` is `true` then the lemma starts with just `f`. + +* If the `fixedParams` argument has `true` for a particular argument index, then this is a hint +that the congruence lemma may use the same parameter for both sides of the equality. There is +no guarantee -- it respects it if the types are equal for that parameter (i.e., if the parameter +does not depend on non-fixed parameters). + +If `forceHEq` is `true` then the conclusion of the generated theorem is a `HEq`. +Otherwise it might be an `Eq` if the equality is homogeneous. + +This is the interpretation of the `CongrArgKind`s in the generated congruence theorem: +* `.eq` corresponds to having three arguments `(x : α) (x' : α) (h : x = x')`. + Note that `h` might have additional hypotheses. +* `.heq` corresponds to having three arguments `(x : α) (x' : α') (h : HEq x x')` + Note that `h` might have additional hypotheses. +* `.fixed` corresponds to having a single argument `(x : α)` that is fixed between the LHS and RHS +* `.subsingletonInst` corresponds to having two arguments `(x : α) (x' : α')` for which the + congruence generator was able to prove that `HEq x x'` already. This is a slight abuse of + this `CongrArgKind` since this is used even for types that are not subsingleton typeclasses. + +Note that the first entry in this array is for the function itself. +-/ +partial def mkRichHCongr (fType : Expr) (info : FunInfo) + (fixedFun : Bool := false) (fixedParams : Array Bool := #[]) + (forceHEq : Bool := false) : + MetaM CongrTheorem := do + trace[Meta.CongrTheorems] "ftype: {fType}" + trace[Meta.CongrTheorems] "deps: {info.paramInfo.map (fun p => p.backDeps)}" + trace[Meta.CongrTheorems] "fixedFun={fixedFun}, fixedParams={fixedParams}" + doubleTelescope fType info.getArity fixedParams fun xs ys fixedParams => do + trace[Meta.CongrTheorems] "xs = {xs}" + trace[Meta.CongrTheorems] "ys = {ys}" + trace[Meta.CongrTheorems] "computed fixedParams={fixedParams}" + let lctx := (← getLCtx) -- checkpoint for a local context that only has the parameters + withLocalDeclD `f fType fun ef => withLocalDeclD `f' fType fun pef' => do + let ef' := if fixedFun then ef else pef' + withLocalDeclD `e (← mkEq ef ef') fun ee => do + withNewEqs xs ys fixedParams fun kinds eqs => do + let fParams := if fixedFun then #[ef] else #[ef, ef', ee] + let mut hs := fParams -- parameters to the basic congruence lemma + let mut hs' := fParams -- parameters to the richer congruence lemma + let mut vals' := fParams -- how to calculate the basic parameters from the richer ones + for i in [0 : info.getArity] do + hs := hs.push xs[i]! + hs' := hs'.push xs[i]! + vals' := vals'.push xs[i]! + if let some (eq, eq', val) := eqs[i]! then + -- Not a fixed argument + hs := hs.push ys[i]! |>.push eq + hs' := hs'.push ys[i]! |>.push eq' + vals' := vals'.push ys[i]! |>.push val + -- Generate the theorem with respect to the simpler hypotheses + let mkConcl := if forceHEq then mkHEq else mkEqHEq + let congrType ← mkForallFVars hs (← mkConcl (mkAppN ef xs) (mkAppN ef' ys)) + trace[Meta.CongrTheorems] "simple congrType: {congrType}" + let some proof ← withLCtx lctx (← getLocalInstances) <| trySolve congrType + | throwError "Internal error when constructing congruence lemma proof" + -- At this point, `mkLambdaFVars hs' (mkAppN proof vals')` is the richer proof. + -- We try to precompute some of the arguments using `trySolve`. + let mut hs'' := #[] -- eq' parameters that are actually used beyond those in `fParams` + let mut pfVars := #[] -- eq' parameters that can be solved for already + let mut pfVals := #[] -- the values to use for these parameters + let mut kinds' : Array CongrArgKind := #[if fixedFun then .fixed else .eq] + for i in [0 : info.getArity] do + hs'' := hs''.push xs[i]! + if let some (_, eq', _) := eqs[i]! then + -- Not a fixed argument + hs'' := hs''.push ys[i]! + let pf? ← withLCtx lctx (← getLocalInstances) <| trySolve (← inferType eq') + if let some pf := pf? then + pfVars := pfVars.push eq' + pfVals := pfVals.push pf + kinds' := kinds'.push .subsingletonInst + else + hs'' := hs''.push eq' + kinds' := kinds'.push kinds[i]! + else + kinds' := kinds'.push .fixed + trace[Meta.CongrTheorems] "CongrArgKinds: {repr kinds'}" + -- Take `proof`, abstract the pfVars and provide the solved-for proofs (as an + -- optimization for proof term size) then abstract the remaining variables. + -- The `usedOnly` probably has no affect. + -- Note that since we are doing `proof.beta vals'` there is technically some quadratic + -- complexity, but it shouldn't be too bad since they're some applications of just variables. + let proof' ← mkLambdaFVars fParams (← mkLambdaFVars (usedOnly := true) hs'' + (mkAppN (← mkLambdaFVars pfVars (proof.beta vals')) pfVals)) + let congrType' ← inferType proof' + trace[Meta.CongrTheorems] "rich congrType: {congrType'}" + return {proof := proof', type := congrType', argKinds := kinds'} +where + /-- Similar to doing `forallBoundedTelescope` twice, but makes use of the `fixed` array, which + is used as a hint for whether both variables should be the same. This is only a hint though, + since we respect it only if the binding domains are equal. + We affix `'` to the second list of variables, and all the variables are introduced + with default binder info. Calls `k` with the xs, ys, and a revised `fixed` array -/ + doubleTelescope {α} (fty : Expr) (numVars : Nat) (fixed : Array Bool) + (k : Array Expr → Array Expr → Array Bool → MetaM α) : MetaM α := do + let rec loop (i : Nat) + (ftyx ftyy : Expr) (xs ys : Array Expr) (fixed' : Array Bool) : MetaM α := do + if i < numVars then + let ftyx ← whnf ftyx + let ftyy ← whnf ftyy + unless ftyx.isForall do + throwError "doubleTelescope: function doesn't have enough parameters" + withLocalDeclD ftyx.bindingName! ftyx.bindingDomain! fun fvarx => do + let ftyx' := ftyx.bindingBody!.instantiate1 fvarx + if fixed.getD i false && ftyx.bindingDomain! == ftyy.bindingDomain! then + -- Fixed: use the same variable for both + let ftyy' := ftyy.bindingBody!.instantiate1 fvarx + loop (i + 1) ftyx' ftyy' (xs.push fvarx) (ys.push fvarx) (fixed'.push true) + else + -- Not fixed: use different variables + let yname := ftyy.bindingName!.appendAfter "'" + withLocalDeclD yname ftyy.bindingDomain! fun fvary => do + let ftyy' := ftyy.bindingBody!.instantiate1 fvary + loop (i + 1) ftyx' ftyy' (xs.push fvarx) (ys.push fvary) (fixed'.push false) + else + k xs ys fixed' + loop 0 fty fty #[] #[] #[] + /-- Introduce variables for equalities between the arrays of variables. Uses `fixedParams` + to control whether to introduce an equality for each pair. The array of triples passed to `k` + consists of (1) the simple congr lemma HEq arg, (2) the richer HEq arg, and (3) how to + compute 1 in terms of 2. -/ + withNewEqs {α} (xs ys : Array Expr) (fixedParams : Array Bool) + (k : Array CongrArgKind → Array (Option (Expr × Expr × Expr)) → MetaM α) : MetaM α := + let rec loop (i : Nat) + (kinds : Array CongrArgKind) (eqs : Array (Option (Expr × Expr × Expr))) := do + if i < xs.size then + let x := xs[i]! + let y := ys[i]! + if fixedParams[i]! then + loop (i+1) (kinds.push .fixed) (eqs.push none) + else + let deps := info.paramInfo[i]!.backDeps.filterMap (fun j => eqs[j]!) + let eq' ← mkForallFVars (deps.map fun (eq, _, _) => eq) (← mkEqHEq x y) + withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEqHEq x y) fun h => + withLocalDeclD ((`e').appendIndexAfter (i+1)) eq' fun h' => do + let v := mkAppN h' (deps.map fun (_, _, val) => val) + let kind := if (← inferType h).eq?.isSome then .eq else .heq + loop (i+1) (kinds.push kind) (eqs.push (h, h', v)) + else + k kinds eqs + loop 0 #[] #[] + /-- Given a type that is a bunch of equalities implying a goal (for example, a basic + congruence lemma), prove it if possible. Basic congruence lemmas should be provable by this. + There are some extra tricks for handling arguments to richer congruence lemmas. -/ + trySolveCore (mvarId : MVarId) : MetaM Unit := do + -- First cleanup the context since we're going to do `substEqs` and we don't want to + -- accidentally use variables not actually used by the theorem. + let mvarId ← mvarId.cleanup + let (_, mvarId) ← mvarId.intros + let mvarId := (← mvarId.substEqs).getD mvarId + try mvarId.refl; return catch _ => pure () + try mvarId.hrefl; return catch _ => pure () + if ← mvarId.proofIrrelHeq then return + -- Make the goal be an eq and then try `Subsingleton.elim` + let mvarId ← mvarId.heqOfEq + if ← mvarId.subsingletonElim then return + -- We have no more tricks. + throwError "was not able to solve for proof" + /-- Driver for `trySolveCore`. -/ + trySolve (ty : Expr) : MetaM (Option Expr) := observing? do + let mvar ← mkFreshExprMVar ty + trace[Meta.CongrTheorems] "trySolve {mvar.mvarId!}" + -- The proofs we generate shouldn't require unfolding anything. + withReducible <| trySolveCore mvar.mvarId! + trace[Meta.CongrTheorems] "trySolve success!" + let pf ← instantiateMVars mvar + return pf + +end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Congr!.lean b/src/Lean/Meta/Tactic/Congr!.lean new file mode 100644 index 000000000000..0e0f2b5f609d --- /dev/null +++ b/src/Lean/Meta/Tactic/Congr!.lean @@ -0,0 +1,643 @@ +/- +Copyright (c) 2023 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Lean.Elab.Tactic.Config +import Lean.Elab.Tactic.RCases +import Lean.Meta.CongrTheorems.Rich +import Lean.Meta.Tactic.Assumption +import Lean.Elab.Tactic.Rfl + +/-! +# The `congr!` tactic + +This is a more powerful version of the `congr` tactic that knows about more congruence lemmas and +can apply to more situations. It is similar to the `congr'` tactic from Mathlib 3. + +The `congr!` tactic is used by the `convert` and `convert_to` tactics. + +See the syntax docstring for more details. +-/ + +namespace Lean.Meta.Tactic.Congr! + +open Lean Meta Elab Tactic + +initialize registerTraceClass `congr! +initialize registerTraceClass `congr!.synthesize + +/-- The configuration for the `congr!` tactic. -/ +structure Config where + /-- If `closePre := true`, then try to close goals before applying congruence lemmas + using tactics such as `rfl` and `assumption. These tactics are applied with the + transparency level specified by `preTransparency`, which is `.reducible` by default. -/ + closePre : Bool := true + /-- If `closePost := true`, then try to close goals that remain after no more congruence + lemmas can be applied, using the same tactics as `closePre`. These tactics are applied + with current tactic transparency level. -/ + closePost : Bool := true + /-- The transparency level to use when applying a congruence theorem. + By default this is `.reducible`, which prevents unfolding of most definitions. -/ + transparency : TransparencyMode := TransparencyMode.reducible + /-- The transparency level to use when trying to close goals before applying congruence lemmas. + This includes trying to prove the goal by `rfl` and using the `assumption` tactic. + By default this is `.reducible`, which prevents unfolding of most definitions. -/ + preTransparency : TransparencyMode := TransparencyMode.reducible + /-- For passes that synthesize a congruence lemma using one side of the equality, + we run the pass both for the left-hand side and the right-hand side. If `preferLHS` is `true` + then we start with the left-hand side. + + This can be used to control which side's definitions are expanded when applying the + congruence lemma (if `preferLHS = true` then the RHS can be expanded). -/ + preferLHS : Bool := true + /-- Allow both sides to be partial applications. + When false, given an equality `f a b = g x y z` this means we never consider + proving `f a = g x y`. + + In this case, we might still consider `f = g x` if a pass generates a congruence lemma using the + left-hand side. Use `sameFun := true` to ensure both sides are applications + of the same function (making it be similar to the `congr` tactic). -/ + partialApp : Bool := true + /-- Whether to require that both sides of an equality be applications of defeq functions. + That is, if true, `f a = g x` is only considered if `f` and `g` are defeq (making it be similar + to the `congr` tactic). -/ + sameFun : Bool := false + /-- The maximum number of arguments to consider when doing congruence of function applications. + For example, with `f a b c = g w x y z`, setting `maxArgs := some 2` means it will only consider + either `f a b = g w x y` and `c = z` or `f a = g w x`, `b = y`, and `c = z`. Setting + `maxArgs := none` (the default) means no limit. + + When the functions are dependent, `maxArgs` can prevent congruence from working at all. + In `Fintype.card α = Fintype.card β`, one needs to have `maxArgs` at `2` or higher since + there is a `Fintype` instance argument that depends on the first. + + When there aren't such dependency issues, setting `maxArgs := some 1` causes `congr!` to + do congruence on a single argument at a time. This can be used in conjunction with the + iteration limit to control exactly how many arguments are to be processed by congruence. -/ + maxArgs : Option Nat := none + /-- For type arguments that are implicit or have forward dependencies, whether or not `congr!` + should generate equalities even if the types do not look plausibly equal. + + We have a heuristic in the main congruence generator that types + `α` and `β` are *plausibly equal* according to the following algorithm: + + - If the types are both propositions, they are plausibly equal (`Iff`s are plausible). + - If the types are from different universes, they are not plausibly equal. + - Suppose in whnf we have `α = f a₁ ... aₘ` and `β = g b₁ ... bₘ`. If `f` is not definitionally + equal to `g` or `m ≠ n`, then `α` and `β` are not plausibly equal. + - If there is some `i` such that `aᵢ` and `bᵢ` are not plausibly equal, then `α` and `β` are + not plausibly equal. + - Otherwise, `α` and `β` are plausibly equal. + + The purpose of this is to prevent considering equalities like `ℕ = ℤ` while allowing equalities + such as `Fin n = Fin m` or `Subtype p = Subtype q` (so long as these are subtypes of the + same type). + + The way this is implemented is that when the congruence generator is comparing arguments when + looking at an equality of function applications, it marks a function parameter as "fixed" if the + provided arguments are types that are not plausibly equal. The effect of this is that congruence + succeeds only if those arguments are defeq at `transparency` transparency. -/ + typeEqs : Bool := false + /-- As a last pass, perform eta expansion of both sides of an equality. For example, + this transforms a bare `HAdd.hAdd` into `fun x y => x + y`. -/ + etaExpand : Bool := false + /-- Whether to use the congruence generator that is used by `simp` and `congr`. This generator + is more strict, and it does not respect all configuration settings. It does respect + `preferLHS`, `partialApp` and `maxArgs` and transparency settings. It acts as if `sameFun := true` + and it ignores `typeEqs`. -/ + useCongrSimp : Bool := false + +/-- A configuration option that makes `congr!` do the sorts of aggressive unfoldings that `congr` +does while also similarly preventing `congr!` from considering partial applications or congruences +between different functions being applied. -/ +def Config.unfoldSameFun : Congr!.Config where + partialApp := false + sameFun := true + transparency := .default + preTransparency := .default + +/-- Whether the given number of arguments is allowed to be considered. -/ +def Config.numArgsOk (config : Config) (numArgs : Nat) : Bool := + numArgs ≤ config.maxArgs.getD numArgs + +/-- According to the configuration, how many of the arguments in `numArgs` should be considered. -/ +def Config.maxArgsFor (config : Config) (numArgs : Nat) : Nat := + min numArgs (config.maxArgs.getD numArgs) + +/-- +Asserts the given congruence theorem as fresh hypothesis, and then applies it. +Return the `fvarId` for the new hypothesis and the new subgoals. + +We apply it with transparency settings specified by `Congr!.Config.transparency`. +-/ +private def applyCongrThm? + (config : Congr!.Config) (mvarId : MVarId) (congrThmType congrThmProof : Expr) : + MetaM (List MVarId) := do + trace[congr!] "trying to apply congr lemma {congrThmType}" + try + let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThmType congrThmProof + let (fvarId, mvarId) ← mvarId.intro1P + let mvarIds ← withTransparency config.transparency <| + mvarId.apply (mkFVar fvarId) { synthAssignedInstances := false } + mvarIds.mapM fun mvarId => mvarId.tryClear fvarId + catch e => + withTraceNode `congr! (fun _ => pure m!"failed to apply congr lemma") do + trace[congr!] "{e.toMessageData}" + throw e + +/-- Returns whether or not it's reasonable to consider an equality between types `ty1` and `ty2`. +The heuristic is the following: + +- If `ty1` and `ty2` are in `Prop`, then yes. +- If in whnf both `ty1` and `ty2` have the same head and if (recursively) it's reasonable to + consider an equality between corresponding type arguments, then yes. +- Otherwise, no. + +This helps keep congr from going too far and generating hypotheses like `ℝ = ℤ`. + +To keep things from going out of control, there is a `maxDepth`. Additionally, if we do the check +with `maxDepth = 0` then the heuristic answers "no". -/ +def Congr!.plausiblyEqualTypes (ty1 ty2 : Expr) (maxDepth : Nat := 5) : MetaM Bool := + match maxDepth with + | 0 => return false + | maxDepth + 1 => do + -- Props are plausibly equal + if (← isProp ty1) && (← isProp ty2) then + return true + -- Types from different type universes are not plausibly equal. + -- This is redundant, but it saves carrying out the remaining checks. + unless ← withNewMCtxDepth <| isDefEq (← inferType ty1) (← inferType ty2) do + return false + -- Now put the types into whnf, check they have the same head, and then recurse on arguments + let ty1 ← whnfD ty1 + let ty2 ← whnfD ty2 + unless ← withNewMCtxDepth <| isDefEq ty1.getAppFn ty2.getAppFn do + return false + for arg1 in ty1.getAppArgs, arg2 in ty2.getAppArgs do + if (← isType arg1) && (← isType arg2) then + unless ← plausiblyEqualTypes arg1 arg2 maxDepth do + return false + return true + +/-- +This is like `Lean.MVarId.hcongr?` but (1) looks at both sides when generating the congruence lemma +and (2) inserts additional hypotheses from equalities from previous arguments. + +It uses `Lean.Meta.mkRichHCongr` to generate the congruence lemmas. + +If the goal is an `Eq`, it uses `eq_of_heq` first. + +As a backup strategy, it uses the LHS/RHS method like in `Lean.MVarId.congrSimp?` +(where `Congr!.Config.preferLHS` determines which side to try first). This uses a particular side +of the target, generates the congruence lemma, then tries applying it. This can make progress +with higher transparency settings. To help the unifier, in this mode it assumes both sides have the +exact same function. +-/ +partial +def _root_.Lean.MVarId.smartHCongr? (config : Congr!.Config) (mvarId : MVarId) : + MetaM (Option (List MVarId)) := + mvarId.withContext do + mvarId.checkNotAssigned `congr! + commitWhenSome? do + let mvarId ← mvarId.eqOfHEq + let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? | return none + if let some mvars ← loop mvarId 0 lhs rhs [] [] then + return mvars + -- The "correct" behavior failed. However, it's often useful + -- to apply congruence lemmas while unfolding definitions, which is what the + -- basic `congr` tactic does due to limitations in how congruence lemmas are generated. + -- We simulate this behavior here by generating congruence lemmas for the LHS and RHS and + -- then applying them. + trace[congr!] "Default smartHCongr? failed, trying LHS/RHS method" + let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs) + if let some mvars ← forSide mvarId fst then + return mvars + else if let some mvars ← forSide mvarId snd then + return mvars + else + return none +where + loop (mvarId : MVarId) (numArgs : Nat) (lhs rhs : Expr) (lhsArgs rhsArgs : List Expr) : + MetaM (Option (List MVarId)) := + match lhs.cleanupAnnotations, rhs.cleanupAnnotations with + | .app f a, .app f' b => do + if not (config.numArgsOk (numArgs + 1)) then + return none + let lhsArgs' := a :: lhsArgs + let rhsArgs' := b :: rhsArgs + -- We try to generate a theorem for the maximal number of arguments + if let some mvars ← loop mvarId (numArgs + 1) f f' lhsArgs' rhsArgs' then + return mvars + -- That failing, we now try for the present number of arguments. + if not config.partialApp && f.isApp && f'.isApp then + -- It's a partial application on both sides though. + return none + -- The congruence generator only handles the case where both functions have + -- definitionally equal types. + unless ← withNewMCtxDepth <| isDefEq (← inferType f) (← inferType f') do + return none + let funDefEq ← withReducible <| withNewMCtxDepth <| isDefEq f f' + if config.sameFun && not funDefEq then + return none + let info ← getFunInfoNArgs f (numArgs + 1) + let mut fixed : Array Bool := #[] + for larg in lhsArgs', rarg in rhsArgs', pinfo in info.paramInfo do + if !config.typeEqs && (!pinfo.isExplicit || pinfo.hasFwdDeps) then + -- When `typeEqs = false` then for non-explicit arguments or + -- arguments with forward dependencies, we want type arguments + -- to be plausibly equal. + if ← isType larg then + -- ^ since `f` and `f'` have defeq types, this implies `isType rarg`. + unless ← Congr!.plausiblyEqualTypes larg rarg do + fixed := fixed.push true + continue + fixed := fixed.push (← withReducible <| withNewMCtxDepth <| isDefEq larg rarg) + let cthm ← mkRichHCongr (forceHEq := true) (← inferType f) info + (fixedFun := funDefEq) (fixedParams := fixed) + -- Now see if the congruence theorem actually applies in this situation by applying it! + let (congrThm', congrProof') := + if funDefEq then + (cthm.type.bindingBody!.instantiate1 f, cthm.proof.beta #[f]) + else + (cthm.type.bindingBody!.bindingBody!.instantiateRev #[f, f'], + cthm.proof.beta #[f, f']) + observing? <| applyCongrThm? config mvarId congrThm' congrProof' + | _, _ => return none + forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) := do + let side := side.cleanupAnnotations + if not side.isApp then return none + let numArgs := config.maxArgsFor side.getAppNumArgs + if not config.partialApp && numArgs < side.getAppNumArgs then + return none + let mut f := side + for _ in [:numArgs] do + f := f.appFn!' + let info ← getFunInfoNArgs f numArgs + let mut fixed : Array Bool := #[] + if !config.typeEqs then + -- We need some strategy for fixed parameters to keep `forSide` from applying + -- in cases where `Congr!.possiblyEqualTypes` suggested not to in the previous pass. + for pinfo in info.paramInfo, arg in side.getAppArgs do + if pinfo.isProp || !(← isType arg) then + fixed := fixed.push false + else if pinfo.isExplicit && !pinfo.hasFwdDeps then + -- It's fine generating equalities for explicit type arguments without forward + -- dependencies. Only allowing these is a little strict, because an argument + -- might be something like `Fin n`. We might consider being able to generate + -- congruence lemmas that only allow equalities where they can plausibly go, + -- but that would take looking at a whole application tree. + fixed := fixed.push false + else + fixed := fixed.push true + let cthm ← mkRichHCongr (forceHEq := true) (← inferType f) info + (fixedFun := true) (fixedParams := fixed) + let congrThm' := cthm.type.bindingBody!.instantiate1 f + let congrProof' := cthm.proof.beta #[f] + observing? <| applyCongrThm? config mvarId congrThm' congrProof' + +/-- +Like `Lean.MVarId.congr?` but instead of using only the congruence lemma associated to the LHS, +it tries the RHS too, in the order specified by `config.preferLHS`. + +It uses `Lean.Meta.mkCongrSimp?` to generate a congruence lemma, like in the `congr` tactic. + +Applies the congruence generated congruence lemmas according to `config`. +-/ +def _root_.Lean.MVarId.congrSimp? (config : Congr!.Config) (mvarId : MVarId) : + MetaM (Option (List MVarId)) := + mvarId.withContext do + unless config.useCongrSimp do return none + mvarId.checkNotAssigned `congrSimp? + let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? | return none + let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs) + if let some mvars ← forSide mvarId fst then + return mvars + else if let some mvars ← forSide mvarId snd then + return mvars + else + return none +where + forSide (mvarId : MVarId) (side : Expr) : MetaM (Option (List MVarId)) := + commitWhenSome? do + let side := side.cleanupAnnotations + if not side.isApp then return none + let numArgs := config.maxArgsFor side.getAppNumArgs + if not config.partialApp && numArgs < side.getAppNumArgs then + return none + let mut f := side + for _ in [:numArgs] do + f := f.appFn!' + let some congrThm ← mkCongrSimpNArgs f numArgs + | return none + observing? <| applyCongrThm? config mvarId congrThm.type congrThm.proof + /-- Like `mkCongrSimp?` but takes in a specific arity. -/ + mkCongrSimpNArgs (f : Expr) (nArgs : Nat) : MetaM (Option CongrTheorem) := do + let f := (← instantiateMVars f).cleanupAnnotations + let info ← getFunInfoNArgs f nArgs + mkCongrSimpCore? f info + (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := false) + +/-- +Try applying user-provided congruence lemmas. If any are applicable, +returns a list of new goals. + +Tries a congruence lemma associated to the LHS and then, if that failed, the RHS. +-/ +def _root_.Lean.MVarId.userCongr? (config : Congr!.Config) (mvarId : MVarId) : + MetaM (Option (List MVarId)) := + mvarId.withContext do + mvarId.checkNotAssigned `userCongr? + let some (lhs, rhs) := (← withReducible mvarId.getType').eqOrIff? | return none + let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs) + if let some mvars ← forSide fst then + return mvars + else if let some mvars ← forSide snd then + return mvars + else + return none +where + forSide (side : Expr) : MetaM (Option (List MVarId)) := do + let side := side.cleanupAnnotations + if not side.isApp then return none + let some name := side.getAppFn.constName? | return none + let congrTheorems := (← getSimpCongrTheorems).get name + -- Note: congruence theorems are provided in decreasing order of priority. + for congrTheorem in congrTheorems do + let res ← observing? do + let cinfo ← getConstInfo congrTheorem.theoremName + let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar + let proof := mkConst congrTheorem.theoremName us + let ptype ← instantiateTypeLevelParams cinfo us + applyCongrThm? config mvarId ptype proof + if let some mvars := res then + return mvars + return none + +/-- +Try to apply `forall_congr`. This is similar to `Lean.MVar.congrImplies?`. +-/ +def _root_.Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) := + observing? do withReducible <| mvarId.apply (← mkConstWithFreshMVarLevels ``forall_congr) + +/-- +Try to apply `funext`, but only if it is an equality of two functions where at least one is +a lambda expression. + +One thing this check prevents is accidentally applying `funext` to a set equality, but also when +doing congruence we don't want to apply `funext` unnecessarily. +-/ +def _root_.Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) := + mvarId.withContext <| observing? do + let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? | failure + if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then failure + mvarId.apply (← mkConstWithFreshMVarLevels ``funext) + +/-- +Try to apply `hfunext`, returning the new goals if it succeeds. +Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HEq` is a lambda. +This prevents unfolding of things like `Set`. + +Need to have `Mathlib.Logic.Function.Basic` imported for this to succeed. +-/ +def _root_.Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) := + mvarId.withContext <| observing? do + let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? | failure + if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then failure + mvarId.apply (← mkConstWithFreshMVarLevels ``hfunext) + +/-- Like `implies_congr` but provides an additional assumption to the second hypothesis. +This is a non-dependent version of `pi_congr` that allows the domains to be different. -/ +private theorem implies_congr' {α α' : Sort u} {β β' : Sort v} (h : α = α') (h' : α' → β = β') : + (α → β) = (α' → β') := by + cases h + show (∀ (x : α), (fun _ => β) x) = _ + rw [funext h'] + +/-- A version of `Lean.MVarId.congrImplies?` that uses `implies_congr'` +instead of `implies_congr`. -/ +def _root_.Lean.MVarId.congrImplies?' (mvarId : MVarId) : MetaM (Option (List MVarId)) := + observing? do + let [mvarId₁, mvarId₂] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr') + | throwError "unexpected number of goals" + return [mvarId₁, mvarId₂] + +/-- +Try to apply `Subsingleton.helim` if the goal is a `HEq`. Tries synthesizing a `Subsingleton` +instance for both the LHS and the RHS. + +If successful, this reduces proving `@HEq α x β y` to proving `α = β`. +-/ +def _root_.Lean.MVarId.subsingletonHelim? (mvarId : MVarId) : MetaM (Option (List MVarId)) := + mvarId.withContext <| observing? do + mvarId.checkNotAssigned `subsingletonHelim + let some (α, lhs, β, rhs) := (← withReducible mvarId.getType').heq? | failure + let eqmvar ← mkFreshExprSyntheticOpaqueMVar (← mkEq α β) (← mvarId.getTag) + -- First try synthesizing using the left-hand side for the Subsingleton instance + if let some pf ← observing? (mkAppM ``Subsingleton.helim #[eqmvar, lhs, rhs]) then + mvarId.assign pf + return [eqmvar.mvarId!] + let eqsymm ← mkAppM ``Eq.symm #[eqmvar] + -- Second try synthesizing using the right-hand side for the Subsingleton instance + if let some pf ← observing? (mkAppM ``Subsingleton.helim #[eqsymm, rhs, lhs]) then + mvarId.assign (← mkAppM ``HEq.symm #[pf]) + return [eqmvar.mvarId!] + failure + +open Lean.MVarId + +/-- +A list of all the congruence strategies used by `Lean.MVarId.congrCore!`. +-/ +def _root_.Lean.MVarId.congrPasses! : + List (String × (Congr!.Config → MVarId → MetaM (Option (List MVarId)))) := + [("user congr", userCongr?), + ("hcongr lemma", smartHCongr?), + ("congr simp lemma", congrSimp?), + ("Subsingleton.helim", fun _ => subsingletonHelim?), + ("obvious funext", fun _ => obviousFunext?), + ("obvious hfunext", fun _ => obviousHfunext?), + ("congr_implies", fun _ => congrImplies?'), + ("congr_pi", fun _ => congrPi?)] + +structure CongrState where + /-- Accumulated goals that `congr!` could not handle. -/ + goals : Array MVarId + /-- Patterns to use when doing intro. -/ + patterns : List (TSyntax `rcasesPat) + +abbrev CongrMetaM := StateRefT CongrState MetaM + +/-- Pop the next pattern from the current state. -/ +def CongrMetaM.nextPattern : CongrMetaM (Option (TSyntax `rcasesPat)) := do + modifyGet fun s => + if let p :: ps := s.patterns then + (p, {s with patterns := ps}) + else + (none, s) + +private theorem heq_imp_of_eq_imp {p : HEq x y → Prop} (h : (he : x = y) → p (heq_of_eq he)) + (he : HEq x y) : p he := by + cases he + exact h rfl + +private theorem eq_imp_of_iff_imp {p : x = y → Prop} (h : (he : x ↔ y) → p (propext he)) + (he : x = y) : p he := by + cases he + exact h Iff.rfl + +/-- +Does `Lean.MVarId.intros` but then cleans up the introduced hypotheses, removing anything +that is trivial. If there are any patterns in the current `CongrMetaM` state then instead +of `Lean.MVarId.intros` it does `Std.Tactic.RCases.rintro`. + +Cleaning up includes: +- deleting hypotheses of the form `HEq x x`, `x = x`, and `x ↔ x`. +- deleting Prop hypotheses that are already in the local context. +- converting `HEq x y` to `x = y` if possible. +- converting `x = y` to `x ↔ y` if possible. +-/ +partial +def _root_.Lean.MVarId.introsClean (mvarId : MVarId) : CongrMetaM (List MVarId) := + loop mvarId +where + heqImpOfEqImp (mvarId : MVarId) : MetaM (Option MVarId) := + observing? <| withReducible do + let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``heq_imp_of_eq_imp) | failure + return mvarId + eqImpOfIffImp (mvarId : MVarId) : MetaM (Option MVarId) := + observing? <| withReducible do + let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``eq_imp_of_iff_imp) | failure + return mvarId + loop (mvarId : MVarId) : CongrMetaM (List MVarId) := + mvarId.withContext do + let ty ← withReducible <| mvarId.getType' + if ty.isForall then + let mvarId := (← heqImpOfEqImp mvarId).getD mvarId + let mvarId := (← eqImpOfIffImp mvarId).getD mvarId + let ty ← withReducible <| mvarId.getType' + if ty.isArrow then + if ← (isTrivialType ty.bindingDomain! + <||> (← getLCtx).anyM (fun decl => do + return (← instantiateMVars decl.type) == ty.bindingDomain!)) then + -- Don't intro, clear it + let mvar ← mkFreshExprSyntheticOpaqueMVar ty.bindingBody! (← mvarId.getTag) + mvarId.assign <| .lam .anonymous ty.bindingDomain! mvar .default + return ← loop mvar.mvarId! + if let some patt ← CongrMetaM.nextPattern then + let gs ← Term.TermElabM.run' <| Lean.Elab.Tactic.RCases.rintro #[patt] none mvarId + List.join <$> gs.mapM loop + else + let (_, mvarId) ← mvarId.intro1 + loop mvarId + else + return [mvarId] + isTrivialType (ty : Expr) : MetaM Bool := do + unless ← Meta.isProp ty do + return false + let ty ← instantiateMVars ty + if let some (lhs, rhs) := ty.eqOrIff? then + if lhs.cleanupAnnotations == rhs.cleanupAnnotations then + return true + if let some (α, lhs, β, rhs) := ty.heq? then + if α.cleanupAnnotations == β.cleanupAnnotations + && lhs.cleanupAnnotations == rhs.cleanupAnnotations then + return true + return false + +/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those). +Also, if `tryClose := true`, then try to close the goal using an assumption, `Subsingleton.Elim`, +or definitional equality. -/ +def _root_.Lean.MVarId.preCongr! (mvarId : MVarId) (tryClose : Bool) : MetaM (Option MVarId) := do + -- Next, turn `HEq` and `Iff` into `Eq` + let mvarId ← mvarId.heqOfEq + if tryClose then + -- This is a good time to check whether we have a relevant hypothesis. + if ← mvarId.assumptionCore then return none + let mvarId ← mvarId.iffOfEq + if tryClose then + -- Now try definitional equality. No need to try `mvarId.hrefl` since we already did `heqOfEq`. + -- We allow synthetic opaque metavariables to be assigned to fill in `x = _` goals that might + -- appear (for example, due to using `convert` with placeholders). + try withAssignableSyntheticOpaque mvarId.refl; return none catch _ => pure () + -- Now we go for (heterogenous) equality via subsingleton considerations + if ← mvarId.subsingletonElim then return none + if ← mvarId.proofIrrelHeq then return none + return some mvarId + +def _root_.Lean.MVarId.congrCore! (config : Congr!.Config) (mvarId : MVarId) : + MetaM (Option (List MVarId)) := do + mvarId.checkNotAssigned `congr! + let s ← saveState + /- We do `liftReflToEq` here rather than in `preCongr!` since we don't want to commit to it + if there are no relevant congr lemmas. -/ + let mvarId ← mvarId.liftReflToEq + for (passName, pass) in congrPasses! do + try + if let some mvarIds ← pass config mvarId then + trace[congr!] "pass succeeded: {passName}" + return mvarIds + catch e => + throwTacticEx `congr! mvarId + m!"internal error in congruence pass {passName}, {e.toMessageData}" + if ← mvarId.isAssigned then + throwTacticEx `congr! mvarId + s!"congruence pass {passName} assigned metavariable but failed" + restoreState s + trace[congr!] "no passes succeeded" + return none + +/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/ +def _root_.Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) := do + let some mvarId ← mvarId.preCongr! config.closePost | return none + -- Convert `p = q` to `p ↔ q`, which is likely the more useful form: + let mvarId ← mvarId.propext + if config.closePost then + -- `preCongr` sees `p = q`, but now we've put it back into `p ↔ q` form. + if ← mvarId.assumptionCore then return none + if config.etaExpand then + if let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? then + let lhs' ← Meta.etaExpand lhs + let rhs' ← Meta.etaExpand rhs + return ← mvarId.change (← mkEq lhs' rhs') + return mvarId + +/-- A more insistent version of `Lean.MVarId.congrN`. +See the documentation on the `congr!` syntax. + +The `depth?` argument controls the depth of the recursion. If `none`, then it uses a reasonably +large bound that is linear in the expression depth. -/ +def _root_.Lean.MVarId.congrN! (mvarId : MVarId) + (depth? : Option Nat := none) (config : Congr!.Config := {}) + (patterns : List (TSyntax `rcasesPat) := []) : + MetaM (List MVarId) := do + let ty ← withReducible <| mvarId.getType' + -- A reasonably large yet practically bounded default recursion depth. + let defaultDepth := min 1000000 (8 * (1 + ty.approxDepth.toNat)) + let depth := depth?.getD defaultDepth + let (_, s) ← go depth depth mvarId |>.run {goals := #[], patterns := patterns} + return s.goals.toList +where + post (mvarId : MVarId) : CongrMetaM Unit := do + for mvarId in ← mvarId.introsClean do + if let some mvarId ← mvarId.postCongr! config then + modify (fun s => {s with goals := s.goals.push mvarId}) + else + trace[congr!] "Dispatched goal by post-processing step." + go (depth : Nat) (n : Nat) (mvarId : MVarId) : CongrMetaM Unit := do + for mvarId in ← mvarId.introsClean do + if let some mvarId ← withTransparency config.preTransparency <| + mvarId.preCongr! config.closePre then + match n with + | 0 => + trace[congr!] "At level {depth - n}, doing post-processing. {mvarId}" + post mvarId + | n + 1 => + trace[congr!] "At level {depth - n}, trying congrCore!. {mvarId}" + if let some mvarIds ← mvarId.congrCore! config then + mvarIds.forM (go depth n) + else + post mvarId + +end Lean.Meta.Tactic.Congr! diff --git a/src/Lean/Meta/Tactic/Congr.lean b/src/Lean/Meta/Tactic/Congr.lean index 518ffe646c0d..022e93207a51 100644 --- a/src/Lean/Meta/Tactic/Congr.lean +++ b/src/Lean/Meta/Tactic/Congr.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Meta.CongrTheorems +import Lean.Meta.CongrTheorems.Basic import Lean.Meta.Tactic.Assert import Lean.Meta.Tactic.Apply import Lean.Meta.Tactic.Clear diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean index d727d309c841..8d7d7925cf31 100644 --- a/src/Lean/Meta/Tactic/NormCast.lean +++ b/src/Lean/Meta/Tactic/NormCast.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner -/ prelude -import Lean.Meta.CongrTheorems +import Lean.Meta.CongrTheorems.Basic import Lean.Meta.Tactic.Simp.Attr import Lean.Meta.CoeAttr diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 6cf6cb72e5c6..c6fb43e6df7f 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -425,14 +425,14 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu return .continue e /-- -Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms. +Auxiliary `dsimproc` for not visiting `OfNat.ofNat` application subterms. This is the `dsimp` equivalent of the approach used at `visitApp`. Recall that we fold orphan raw Nat literals. -/ private def doNotVisitOfNat : DSimproc := doNotVisit isOfNatNatLit ``OfNat.ofNat /-- -Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms. +Auxiliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms. -/ private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 2540eb529f6b..4acbd17f025f 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Meta.AppBuilder -import Lean.Meta.CongrTheorems +import Lean.Meta.CongrTheorems.Basic import Lean.Meta.Eqns import Lean.Meta.Tactic.Replace import Lean.Meta.Tactic.Simp.SimpTheorems diff --git a/tests/lean/run/congr!.lean b/tests/lean/run/congr!.lean new file mode 100644 index 000000000000..286c9c4a5492 --- /dev/null +++ b/tests/lean/run/congr!.lean @@ -0,0 +1,261 @@ +-- Everything should be built-in, but we still need this import in order to use `config`. +-- Moving `Lean.Meta.Tactic.Congr!` to `Init/MetaTypes.lean` and an update-stage0 should hopefully fix this? +import Lean.Meta.Tactic.Congr! + +private axiom test_sorry : ∀ {α}, α +set_option autoImplicit true + +-- Useful for debugging the generated congruence theorems +set_option trace.Meta.CongrTheorems true + +theorem ex1 (a b c : Nat) (h : a = b) : a + c = b + c := by + congr! + +theorem ex2 (a b : Nat) (h : a = b) : ∀ c, a + c = b + c := by + congr! + +theorem ex3 (a b : Nat) (h : a = b) : (fun c => a + c) = (fun c => b + c) := by + congr! + +theorem ex4 (a b : Nat) : Fin (a + b) = Fin (b + a) := by + congr! 1 + guard_target = a + b = b + a + apply Nat.add_comm + +theorem ex5 : ((a : Nat) → Fin (a + 1)) = ((a : Nat) → Fin (1 + a)) := by + congr! 2 with a + guard_target = a + 1 = 1 + a + apply Nat.add_comm + +theorem ex6 : ((a : Nat) × Fin (a + 1)) = ((a : Nat) × Fin (1 + a)) := by + congr! 3 with a + guard_target = a + 1 = 1 + a + apply Nat.add_comm + +theorem ex7 (p : Prop) (h1 h2 : p) : h1 = h2 := by + congr! + +theorem ex8 (p q : Prop) (h1 : p) (h2 : q) : HEq h1 h2 := by + congr! + +attribute [local refl] Nat.le_refl in +theorem ex9 (a b : Nat) (h : a = b) : a + 1 ≤ b + 1 := by + congr! + +theorem ex10 (x y : Unit) : x = y := by + congr! + +theorem ex11 (p q r : Nat → Prop) (h : q = r) : (∀ n, p n → q n) ↔ (∀ n, p n → r n) := by + congr! + +theorem ex12 (p q : Prop) (h : p ↔ q) : p = q := by + congr! + +theorem ex13 (x y : α) (h : x = y) (f : α → Nat) : f x = f y := by + congr! + +theorem ex14 {α : Type} (f : Nat → Nat) (h : ∀ x, f x = 0) (z : α) (hz : HEq z 0) : + HEq f (fun (_ : α) => z) := by + congr! + · guard_target = Nat = α + exact type_eq_of_heq hz.symm + next n x _ => + guard_target = HEq (f n) z + rw [h] + exact hz.symm + +theorem ex15 (p q : Nat → Prop) : + (∀ ε > 0, p ε) ↔ ∀ ε > 0, q ε := by + congr! 2 with ε hε + guard_hyp hε : ε > 0 + guard_target = p ε ↔ q ε + exact test_sorry + +/- Congruence here is OK since `Fin m = Fin n` is plausible to prove. -/ +example (m n : Nat) (h : m = n) (x : Fin m) (y : Fin n) : HEq (x + x) (y + y) := by + congr! + guard_target = HEq x y + exact test_sorry + guard_target = HEq x y + exact test_sorry + +/- Props are types, but prop equalities are totally plausible. -/ +example (p q r : Prop) : p ∧ q ↔ p ∧ r := by + congr! + guard_target = q ↔ r + exact test_sorry + +/- Congruence here is not OK by default since `α = β` is not generally plausible. -/ +example (α β) [inst1 : Add α] [inst2 : Add β] (x : α) (y : β) : HEq (x + x) (y + y) := by + congr! + guard_target = HEq (x + x) (y + y) + -- But with typeEqs we can get it to generate the congruence anyway: + have : α = β := test_sorry + have : HEq inst1 inst2 := test_sorry + congr! (config := { typeEqs := true }) + guard_target = HEq x y + exact test_sorry + guard_target = HEq x y + exact test_sorry + +example (prime : Nat → Prop) (n : Nat) : + prime (2 * n + 1) = prime (n + n + 1) := by + congr! + · guard_target =ₛ (HMul.hMul : Nat → Nat → Nat) = HAdd.hAdd + exact test_sorry + · guard_target = 2 = n + exact test_sorry + +example (prime : Nat → Prop) (n : Nat) : + prime (2 * n + 1) = prime (n + n + 1) := by + congr! (config := {etaExpand := true}) + · guard_target =ₛ (fun (x y : Nat) => x * y) = (fun (x y : Nat) => x + y) + exact test_sorry + · guard_target = 2 = n + exact test_sorry + +example (prime : Nat → Prop) (n : Nat) : + prime (2 * n + 1) = prime (n + n + 1) := by + congr! 2 + guard_target = 2 * n = n + n + exact test_sorry + +example (prime : Nat → Prop) (n : Nat) : + prime (2 * n + 1) = prime (n + n + 1) := by + congr! (config := .unfoldSameFun) + guard_target = 2 * n = n + n + exact test_sorry + +opaque partiallyApplied (p : Prop) [Decidable p] : Nat → Nat + +-- Partially applied dependent functions +example : partiallyApplied (True ∧ True) = partiallyApplied True := by + congr! + decide + +inductive walk (α : Type) : α → α → Type + | nil (n : α) : walk α n n + +def walk.map (f : α → β) (w : walk α x y) : walk β (f x) (f y) := + match x, y, w with + | _, _, .nil n => .nil (f n) + +example (w : walk α x y) (w' : walk α x' y') (f : α → β) : HEq (w.map f) (w'.map f) := by + congr! + guard_target = x = x' + exact test_sorry + guard_target = y = y' + exact test_sorry + -- get x = y and y = y' in context for `HEq w w'` goal. + have : x = x' := by assumption + have : y = y' := by assumption + guard_target = HEq w w' + exact test_sorry + +example (w : walk α x y) (w' : walk α x' y') (f : α → β) : HEq (w.map f) (w'.map f) := by + congr! with rfl rfl + guard_target = x = x' + exact test_sorry + guard_target = y = y' + exact test_sorry + guard_target = w = w' + exact test_sorry + +def MySet (α : Type _) := α → Prop +def MySet.image (f : α → β) (s : MySet α) : MySet β := fun y => ∃ x, s x ∧ f x = y + +-- Testing for equality between what are technically partially applied functions +example (s t : MySet α) (f g : α → β) (h1 : s = t) (h2 : f = g) : + MySet.image f s = MySet.image g t := by + congr! + + +example (c : Prop → Prop → Prop → Prop) (x x' y z z' : Prop) + (h₀ : x ↔ x') (h₁ : z ↔ z') : c x y z ↔ c x' y z' := by + congr! + +example {α β γ δ} {F : ∀{α β}, (α → β) → γ → δ} {f g : α → β} {s : γ} (h : ∀ (x : α), f x = g x) : + F f s = F g s := by + congr! + funext + apply h + +example {α β : Type _} {f : _ → β} {x y : {x : {x : α // x = x} // x = x} } (h : x.1 = y.1) : + f x = f y := by + congr! 1 + ext1 + exact h + +example {α β : Type _} {F : _ → β} {f g : {f : α → β // f = f} } + (h : ∀ x : α, (f : α → β) x = (g : α → β) x) : + F f = F g := by + congr! + ext x + apply h + +example {ls : List Nat} {f g : Nat → Nat} {h : ∀ x, f x = g x} : + ls.map (fun x => f x + 3) = ls.map (fun x => g x + 3) := by + congr! 3 with x -- it's a little too powerful and will get to `f = g` + exact h x + +-- succeed when either `ext` or `congr` can close the goal +example : () = () := by congr! +example : 0 = 0 := by congr! + +example {α} (a : α) : a = a := by congr! + +example {α} (a b : α) (h : false) : a = b := by + fail_if_success { congr! } + cases h + +def g (x : Nat) : Nat := x + 1 + +example (x y z : Nat) (h : x = z) (hy : y = 2) : 1 + x + y = g z + 2 := by + congr! + guard_target = HAdd.hAdd 1 = g + funext + simp [g, Nat.add_comm] + +example (Fintype : Type → Type) + (α β : Type) (inst : Fintype α) (inst' : Fintype β) : HEq inst inst' := by + congr! + guard_target = HEq inst inst' + exact test_sorry + +/- Here, `Fintype` is a subsingleton class so the `HEq` reduces to `Fintype α = Fintype β`. +Since these are explicit type arguments with no forward dependencies, this reduces to `α = β`. +Generating a type equality seems like the right thing to do in this context. +Usually `HEq inst inst'` wouldn't be generated as a subgoal with the default `typeEqs := false`. -/ +example (Fintype : Type → Type) [∀ γ, Subsingleton (Fintype γ)] + (α β : Type) (inst : Fintype α) (inst' : Fintype β) : HEq inst inst' := by + congr! + guard_target = α = β + exact test_sorry + +example : n = m → 3 + n = m + 3 := by + congr! 0 with rfl + guard_target = 3 + n = n + 3 + apply Nat.add_comm + +example (x y x' y' : Nat) (hx : x = x') (hy : y = y') : x + y = x' + y' := by + congr! (config := { closePre := false, closePost := false }) + exact hx + exact hy + +example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by + congr! + +example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by + congr! (config := { closePost := false }) + exact hx + +example : { f : Nat → Nat // f = id } := + ⟨?_, by + -- prevents `rfl` from solving for `?m` in `?m = id`: + congr! (config := { closePre := false, closePost := false }) + ext x + exact Nat.zero_add x⟩ + +-- Regression test. From fixing a "declaration has metavariables" bug +example (h : z = y) : (x = y ∨ x = z) → x = y := by + congr! with (rfl|rfl)