From f1707117f0e4381027fe5e37cbbe695e66b8bac8 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 31 Oct 2024 19:12:14 -0700 Subject: [PATCH] feat: conv `arg` now can access more arguments (#5894) Specializes the congr lemma generated for the `arg` conv tactic to only rewrite the chosen argument. This makes it much more likely that the chosen argument is able to be accessed. Lets `arg` access the domain and codomain of pi types via `arg 1` and `arg 2` in more situations. Upstreams `pi_congr` for this from mathlib. Adds a negative indexing option, where `arg -2` accesses the second-to-last argument for example, making the behavior of `lhs` available to `arg`. This works for `enter` as well. Other improvement: when there is an error in the `enter [...]` tactic, individual locations get underlined with the error. The tactic info now also is like `rw`, so you can see the intermediate conv states. Closes #5871 --- src/Init/Conv.lean | 31 ++-- src/Init/SimpLemmas.lean | 7 + src/Lean/Elab/Tactic/Conv/Congr.lean | 216 ++++++++++++++++++++------- src/Lean/Meta/CongrTheorems.lean | 23 +++ tests/lean/conv1.lean.expected.out | 8 +- tests/lean/run/2942.lean | 32 ++++ tests/lean/run/conv_arg.lean | 81 ++++++++++ tests/lean/run/issue4394.lean | 2 +- 8 files changed, 325 insertions(+), 75 deletions(-) create mode 100644 tests/lean/run/conv_arg.lean diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 5365b63ea8..323abdf177 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -47,12 +47,20 @@ scoped syntax (name := withAnnotateState) /-- `skip` does nothing. -/ syntax (name := skip) "skip" : conv -/-- Traverses into the left subterm of a binary operator. -(In general, for an `n`-ary operator, it traverses into the second to last argument.) -/ +/-- +Traverses into the left subterm of a binary operator. + +In general, for an `n`-ary operator, it traverses into the second to last argument. +It is a synonym for `arg -2`. +-/ syntax (name := lhs) "lhs" : conv -/-- Traverses into the right subterm of a binary operator. -(In general, for an `n`-ary operator, it traverses into the last argument.) -/ +/-- +Traverses into the right subterm of a binary operator. + +In general, for an `n`-ary operator, it traverses into the last argument. +It is a synonym for `arg -1`. +-/ syntax (name := rhs) "rhs" : conv /-- Traverses into the function of a (unary) function application. @@ -75,13 +83,17 @@ subgoals for all the function arguments. For example, if the target is `f x y` t `congr` produces two subgoals, one for `x` and one for `y`. -/ syntax (name := congr) "congr" : conv +syntax argArg := "@"? "-"? num + /-- * `arg i` traverses into the `i`'th argument of the target. For example if the target is `f a b c d` then `arg 1` traverses to `a` and `arg 3` traverses to `c`. + The index may be negative; `arg -1` traverses into the last argument, + `arg -2` into the second-to-last argument, and so on. * `arg @i` is the same as `arg i` but it counts all arguments instead of just the explicit arguments. * `arg 0` traverses into the function. If the target is `f a b c d`, `arg 0` traverses into `f`. -/ -syntax (name := arg) "arg " "@"? num : conv +syntax (name := arg) "arg " argArg : conv /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression) to target `e`, introducing name `x` in the process. -/ @@ -264,7 +276,7 @@ macro "right" : conv => `(conv| rhs) /-- `intro` traverses into binders. Synonym for `ext`. -/ macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*) -syntax enterArg := ident <|> ("@"? num) +syntax enterArg := ident <|> argArg /-- `enter [arg, ...]` is a compact way to describe a path to a subterm. It is a shorthand for other conv tactics as follows: @@ -273,12 +285,7 @@ It is a shorthand for other conv tactics as follows: * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`. For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]` will traverse to the subterm `b`. -/ -syntax "enter" " [" withoutPosition(enterArg,+) "]" : conv -macro_rules - | `(conv| enter [$i:num]) => `(conv| arg $i) - | `(conv| enter [@$i]) => `(conv| arg @$i) - | `(conv| enter [$id:ident]) => `(conv| ext $id) - | `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*])) +syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv /-- The `apply thm` conv tactic is the same as `apply thm` the tactic. There are no restrictions on `thm`, but strange results may occur if `thm` diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 37dc57f73e..d75a4a6bc7 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -54,6 +54,13 @@ theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by subst h₁; simp [← h₂] +theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → Prop) : + (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a)) := + h ▸ rfl + +theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a := + (funext h : β = β') ▸ rfl + theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β} (h₁ : a = a') (h₂ : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) := h₁ ▸ (funext h₂ : b = b') ▸ rfl diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index f20a29f67c..ab68579c7f 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -11,6 +11,8 @@ import Lean.Elab.Tactic.Conv.Basic namespace Lean.Elab.Tactic.Conv open Meta +@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure () + private def congrImplies (mvarId : MVarId) : MetaM (List MVarId) := do let [mvarId₁, mvarId₂, _, _] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr) | throwError "'apply implies_congr' unexpected result" let mvarId₁ ← markAsConvGoal mvarId₁ @@ -72,6 +74,14 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) ( mvarIdsNewInsts := mvarIdsNewInsts ++ mvarIdsNewInsts' return (proof, mvarIdsNew, mvarIdsNewInsts) +private def resolveRhs (tacticName : String) (rhs rhs' : Expr) : MetaM Unit := do + unless (← isDefEqGuarded rhs rhs') do + throwError "invalid '{tacticName}' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" + +private def resolveRhsFromProof (tacticName : String) (rhs proof : Expr) : MetaM Unit := do + let some (_, _, rhs') := (← whnf (← inferType proof)).eq? | throwError "'{tacticName}' conv tactic failed, equality expected" + resolveRhs tacticName rhs rhs' + def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) : MetaM (List (Option MVarId)) := mvarId.withContext do let origTag ← mvarId.getTag @@ -82,9 +92,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) : else if lhs.isApp then let (proof, mvarIdsNew, mvarIdsNewInsts) ← mkCongrThm origTag lhs.getAppFn lhs.getAppArgs addImplicitArgs nameSubgoals - let some (_, _, rhs') := (← whnf (← inferType proof)).eq? | throwError "'congr' conv tactic failed, equality expected" - unless (← isDefEqGuarded rhs rhs') do - throwError "invalid 'congr' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" + resolveRhsFromProof "congr" rhs proof mvarId.assign proof return mvarIdsNew.toList ++ mvarIdsNewInsts.toList else @@ -93,42 +101,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) : @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do replaceMainGoal <| List.filterMap id (← congr (← getMainGoal)) --- mvarIds is the list of goals produced by congr. We only want to change the one at position `i` --- so this closes all other equality goals with `rfl.`. There are non-equality goals produced --- by `congr` (e.g. dependent instances), these are kept as goals. -private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) : - TacticM Unit := do - if i >= 0 then - let i := i.toNat - if h : i < mvarIds.length then - let mut otherGoals := #[] - for mvarId? in mvarIds, j in [:mvarIds.length] do - match mvarId? with - | none => pure () - | some mvarId => - if i != j then - if (← mvarId.getType').isEq then - mvarId.refl - else - -- If its not an equality, it's likely a class constraint, to be left open - otherGoals := otherGoals.push mvarId - match mvarIds[i] with - | none => throwError "cannot select argument" - | some mvarId => replaceMainGoal (mvarId :: otherGoals.toList) - return () - throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)" - -@[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure () - -@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do - let mvarIds ← congr (← getMainGoal) (nameSubgoals := false) - selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2) - -@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do - let mvarIds ← congr (← getMainGoal) (nameSubgoals := false) - selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1) - -/-- Implementation of `arg 0` -/ +/-- Implementation of `arg 0`. -/ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let (lhs, rhs) ← getLhsRhsCore mvarId let lhs := (← instantiateMVars lhs).cleanupAnnotations @@ -136,24 +109,137 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do throwError "invalid 'arg 0' conv tactic, application expected{indentExpr lhs}" lhs.withApp fun f xs => do let (g, mvarNew) ← mkConvGoalFor f - mvarId.assign (← xs.foldlM (fun mvar a => Meta.mkCongrFun mvar a) mvarNew) - let rhs' := mkAppN g xs - unless ← isDefEqGuarded rhs rhs' do - throwError "invalid 'arg 0' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" + mvarId.assign (← xs.foldlM (init := mvarNew) Meta.mkCongrFun) + resolveRhs "arg 0" rhs (mkAppN g xs) return mvarNew.mvarId! -@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do - match stx with - | `(conv| arg $[@%$tk?]? $i:num) => - let i := i.getNat - if i == 0 then - replaceMainGoal [← congrFunN (← getMainGoal)] +private partial def mkCongrArgZeroThm (tacticName : String) (origTag : Name) (f : Expr) (args : Array Expr) : + MetaM (Expr × MVarId × Array MVarId) := do + let funInfo ← getFunInfoNArgs f args.size + let some congrThm ← mkCongrSimpCore? f funInfo (← getCongrSimpKindsForArgZero funInfo) (subsingletonInstImplicitRhs := false) + | throwError "'{tacticName}' conv tactic failed to create congruence theorem" + unless congrThm.argKinds[0]! matches .eq do + throwError "'{tacticName}' conv tactic failed, cannot select argument" + let mut eNew := f + let mut proof := congrThm.proof + let mut mvarIdNew? := none + let mut mvarIdsNewInsts := #[] + for h : i in [:congrThm.argKinds.size] do + let arg := args[i]! + let argInfo := funInfo.paramInfo[i]! + match congrThm.argKinds[i] with + | .fixed | .cast => + eNew := mkApp eNew arg + proof := mkApp proof arg + | .eq => + let (rhs, mvarNew) ← mkConvGoalFor arg origTag + eNew := mkApp eNew rhs + proof := mkApp3 proof arg rhs mvarNew + if mvarIdNew?.isSome then throwError "'{tacticName}' conv tactic failed, cannot select argument" + mvarIdNew? := some mvarNew.mvarId! + | .subsingletonInst => + proof := mkApp proof arg + let rhs ← mkFreshExprMVar (← whnf (← inferType proof)).bindingDomain! + eNew := mkApp eNew rhs + proof := mkApp proof rhs + mvarIdsNewInsts := mvarIdsNewInsts.push rhs.mvarId! + | .heq | .fixedNoParam => unreachable! + let proof' ← args[congrThm.argKinds.size:].foldlM (init := proof) mkCongrFun + return (proof', mvarIdNew?.get!, mvarIdsNewInsts) + +/-- +Implements `arg` for foralls. If `domain` is true, accesses the domain, otherwise accesses the codomain. +-/ +def congrArgForall (tacticName : String) (domain : Bool) (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List MVarId) := do + let .forallE n t b bi := lhs | unreachable! + if domain then + if !b.hasLooseBVars then + let (t', g) ← mkConvGoalFor t (← mvarId.getTag) + mvarId.assign <| ← mkAppM ``implies_congr #[g, ← mkEqRefl b] + resolveRhs tacticName rhs (.forallE n t' b bi) + return [g.mvarId!] + else if ← isProp b <&&> isProp lhs then + let (_rhs, g) ← mkConvGoalFor t (← mvarId.getTag) + let proof ← mkAppM ``forall_prop_congr_dom #[g, .lam n t b .default] + resolveRhsFromProof tacticName rhs proof + mvarId.assign proof + return [g.mvarId!] else - let i := i - 1 - let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false) - selectIdx "arg" mvarIds i + throwError m!"'{tacticName}' conv tactic failed, cannot select domain" + else + withLocalDeclD (← mkFreshUserName n) t fun arg => do + let u ← getLevel t + let q := b.instantiate1 arg + let (q', g) ← mkConvGoalFor q (← mvarId.getTag) + let v ← getLevel q + let proof := mkAppN (.const ``pi_congr [u, v]) + #[t, .lam n t b .default, ← mkLambdaFVars #[arg] q', ← mkLambdaFVars #[arg] g] + resolveRhsFromProof tacticName rhs proof + mvarId.assign proof + return [g.mvarId!] + +/-- Implementation of `arg i`. -/ +def congrArgN (tacticName : String) (mvarId : MVarId) (i : Int) (explicit : Bool) : MetaM (List MVarId) := mvarId.withContext do + let (lhs, rhs) ← getLhsRhsCore mvarId + let lhs := (← instantiateMVars lhs).cleanupAnnotations + if lhs.isForall then + if i < -2 || i == 0 || i > 2 then throwError "invalid '{tacticName}' conv tactic, index is out of bounds for pi type" + let domain := i == 1 || i == -2 + return ← congrArgForall tacticName domain mvarId lhs rhs + else if lhs.isApp then + lhs.withApp fun f xs => do + let (f, xs) ← applyArgs f xs i + let (proof, mvarIdNew, mvarIdsNewInsts) ← mkCongrArgZeroThm tacticName (← mvarId.getTag) f xs + resolveRhsFromProof tacticName rhs proof + mvarId.assign proof + return mvarIdNew :: mvarIdsNewInsts.toList + else + throwError "invalid '{tacticName}' conv tactic, application or implication expected{indentExpr lhs}" +where + applyArgs (f : Expr) (xs : Array Expr) (i : Int) : MetaM (Expr × Array Expr) := do + if explicit then + let i := if i > 0 then i - 1 else i + xs.size + if i < 0 || i ≥ xs.size then + throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds" + let idx := i.natAbs + return (mkAppN f xs[0:idx], xs[idx:]) + else + let mut fType ← inferType f + let mut j := 0 + let mut explicitIdxs := #[] + for k in [0:xs.size] do + unless fType.isForall do + fType ← withTransparency .all <| whnf (fType.instantiateRevRange j k xs) + j := k + let .forallE _ _ b bi := fType | failure + fType := b + if bi.isExplicit then + explicitIdxs := explicitIdxs.push k + let i := if i > 0 then i - 1 else i + explicitIdxs.size + if i < 0 || i ≥ explicitIdxs.size then + throwError "invalid '{tacticName}' tactic, application has {xs.size} explicit argument(s) but the index is out of bounds" + let idx := explicitIdxs[i.natAbs]! + return (mkAppN f xs[0:idx], xs[idx:]) + +def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := do + if i == 0 then + replaceMainGoal [← congrFunN (← getMainGoal)] + else + replaceMainGoal (← congrArgN tacticName (← getMainGoal) i explicit) + +@[builtin_tactic Lean.Parser.Tactic.Conv.arg] def elabArg : Tactic := fun stx => do + match stx with + | `(conv| arg $[@%$tk?]? $[-%$neg?]? $i:num) => + let i : Int := if neg?.isSome then -i.getNat else i.getNat + evalArg "arg" i (explicit := tk?.isSome) | _ => throwUnsupportedSyntax +@[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do + evalArg "lhs" (-2) false + +@[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do + evalArg "rhs" (-1) false + @[builtin_tactic Lean.Parser.Tactic.Conv.«fun»] def evalFun : Tactic := fun _ => do let mvarId ← getMainGoal mvarId.withContext do @@ -163,9 +249,7 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do | throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}" let (g, mvarNew) ← mkConvGoalFor f mvarId.assign (← Meta.mkCongrFun mvarNew a) - let rhs' := .app g a - unless ← isDefEqGuarded rhs rhs' do - throwError "invalid 'fun' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" + resolveRhs "fun" rhs (.app g a) replaceMainGoal [mvarNew.mvarId!] def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do @@ -209,9 +293,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : let (qa, mvarNew) ← mkConvGoalFor pa let q ← mkLambdaFVars #[a] qa let h ← mkLambdaFVars #[a] mvarNew - let rhs' ← mkForallFVars #[a] qa - unless (← isDefEqGuarded rhs rhs') do - throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}" + resolveRhs "ext" rhs (← mkForallFVars #[a] qa) return (q, h, mvarNew) let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h mvarId.assign proof @@ -238,4 +320,22 @@ private def ext (userName? : Option Name) : TacticM Unit := do for id in ids do withRef id <| ext id.getId +-- syntax (name := enter) "enter" " [" enterArg,+ "]" : conv +@[builtin_tactic Lean.Parser.Tactic.Conv.enter] def evalEnter : Tactic := fun stx => do + let token := stx[0] + let lbrak := stx[1] + let enterArgsAndSeps := stx[2].getArgs + -- show initial state up to (incl.) `[` + withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ()) + let numEnterArgs := (enterArgsAndSeps.size + 1) / 2 + for i in [:numEnterArgs] do + let enterArg := enterArgsAndSeps[2 * i]! + let sep := enterArgsAndSeps.getD (2 * i + 1) .missing + -- show state up to (incl.) next `,` and show errors on `enterArg` + withTacticInfoContext (mkNullNode #[enterArg, sep]) <| withRef enterArg do + match enterArg with + | `(Parser.Tactic.Conv.enterArg| $arg:argArg) => evalTactic (← `(conv| arg $arg)) + | `(Parser.Tactic.Conv.enterArg| $id:ident) => evalTactic (← `(conv| ext $id)) + | _ => pure () + end Lean.Elab.Tactic.Conv diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 2bd1484ce1..f5818f1dfd 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -231,6 +231,29 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) : result := result.push .eq return fixKindsForDependencies info result +/-- +Variant of `getCongrSimpKinds` for rewriting just argument 0. +If it is possible to rewrite, the 0th `CongrArgKind` is `CongrArgKind.eq`, +and otherwise it is `CongrArgKind.fixed`. This is used for the `arg` conv tactic. +-/ +def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) := do + let mut result := #[] + for h : i in [:info.paramInfo.size] do + if info.resultDeps.contains i then + result := result.push .fixed + else if i == 0 then + result := result.push .eq + else if info.paramInfo[i].isProp then + result := result.push .cast + else if info.paramInfo[i].isInstImplicit then + if shouldUseSubsingletonInst info result i then + result := result.push .subsingletonInst + else + result := result.push .fixed + else + result := result.push .fixed + return fixKindsForDependencies info result + /-- Create a congruence theorem that is useful for the simplifier and `congr` tactic. -/ diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out index 21bcb4c821..8da1c2c899 100644 --- a/tests/lean/conv1.lean.expected.out +++ b/tests/lean/conv1.lean.expected.out @@ -125,11 +125,11 @@ x y : Nat h1 : y = 0 h2 : p x | y -conv1.lean:221:10-221:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s) -conv1.lean:224:10-224:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s) -conv1.lean:227:10-227:13: error: invalid 'congr' conv tactic, application or implication expected +conv1.lean:221:10-221:13: error: invalid 'lhs' tactic, application has 1 explicit argument(s) but the index is out of bounds +conv1.lean:224:10-224:15: error: invalid 'arg' tactic, application has 1 explicit argument(s) but the index is out of bounds +conv1.lean:227:10-227:13: error: invalid 'rhs' conv tactic, application or implication expected p -conv1.lean:230:10-230:15: error: cannot select argument +conv1.lean:230:10-230:15: error: 'arg' conv tactic failed, cannot select argument a✝ : Nat := 0 b✝ : Nat := a✝ | 0 = 0 diff --git a/tests/lean/run/2942.lean b/tests/lean/run/2942.lean index e971ae7005..8643f0e704 100644 --- a/tests/lean/run/2942.lean +++ b/tests/lean/run/2942.lean @@ -34,3 +34,35 @@ example (a b : Nat) (g : {α : Type} → α → α) (f : Nat → Nat) (h : a = b lhs arg 2 rw [h] + +/-! +While we are here, test `arg` too via `enter`. +-/ + +/-- +info: a b : Nat +g : {α : Type} → α → α +f : Nat → Nat +h : a = b +| a +--- +info: a b : Nat +g : {α : Type} → α → α +f : Nat → Nat +h : a = b +| f +--- +info: a b : Nat +g : {α : Type} → α → α +f : Nat → Nat +h : a = b +| a +-/ +#guard_msgs in +example (a b : Nat) (g : {α : Type} → α → α) (f : Nat → Nat) (h : a = b) : g f a = g f b := by + conv => + conv => enter [1,2]; trace_state + conv => enter [1,1]; trace_state + conv => enter [1,@3]; trace_state + conv => fail_if_success enter [1,@1] -- cannot select the `Type` argument due to dependence. + rw [h] diff --git a/tests/lean/run/conv_arg.lean b/tests/lean/run/conv_arg.lean new file mode 100644 index 0000000000..bd1642346e --- /dev/null +++ b/tests/lean/run/conv_arg.lean @@ -0,0 +1,81 @@ +/-! +# Tests for `conv` mode `arg` tactic +-/ + +/-! +Basic `arg` usage +-/ +example (a b : Nat) (h : b = a) : a + b = a + a := by + conv => + enter [1, 2] + rw [h] + +example (a b : Nat) (h : b = a) : a + b = a + a := by + conv => + enter [-2, -1] + rw [h] + +-- Implications +example (p₁ p₂ q : Prop) (h : p₁ ↔ p₂) : (p₁ → q) ↔ (p₂ → q) := by + conv => enter [1, 1] + conv => + enter [1, 1] + rw [h] + +example (p q₁ q₂ : Prop) (h : q₁ ↔ q₂) : (p → q₁) ↔ (p → q₂) := by + conv => enter [1, 2] + conv => + enter [1, 2] + rw [h] + +-- Dependent implications +/-- +info: i✝ : Nat +| i✝ < 10 +--- +info: a✝¹ : Nat +a✝ : a✝¹ < 10 +| ↑⟨a✝¹, ⋯⟩ = a✝¹ +-/ +#guard_msgs in +example : ∀ (i : Nat) (h : i < 10), (⟨i, h⟩ : Fin 10).val = i := by + conv => + enter [2,1] + trace_state + conv => + enter [2,2] + trace_state + simp + simp + +/-! +Explicit mode +-/ +example (f : {_ : Nat} → Nat → Nat) (h : n = n') : @f n m = @f n' m := by + conv => + enter [1, @1] + rw [h] + +example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by + conv => + enter [1, @2] + rw [h] + +/-! +Issue https://github.com/leanprover/lean4/issues/5871 +The `arg` tactic was `congr` theorems, which was too restrictive. +-/ +class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where + /-- The coercion from `F` to a function. -/ + coe : F → ∀ a : α, β a + +structure MyFun (α β : Type) where + toFun : α → β + +instance : DFunLike (MyFun α β) α (fun _ => β) where + coe f := f.toFun + +example (a b : Nat) (h : a = b) (f : MyFun Nat Int) : DFunLike.coe f a = DFunLike.coe f b := by + conv => + enter [1, 2] -- the `arg 2` used to fail + rw [h] diff --git a/tests/lean/run/issue4394.lean b/tests/lean/run/issue4394.lean index b666a40205..b4684a4598 100644 --- a/tests/lean/run/issue4394.lean +++ b/tests/lean/run/issue4394.lean @@ -55,7 +55,7 @@ example [PropClass n] (h : P1 n) : P1 n := by conv => arg 1; rw [id.eq_def n] exact h -/-- error: cannot select argument -/ +/-- error: 'arg' conv tactic failed, cannot select argument -/ #guard_msgs in example [TypeClass n] [TypeClass (id n)] (h : P2 n) : P2 (id n) := by conv => arg 1