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
This commit is contained in:
Kyle Miller
GitHub
parent
3b80d1eb1f
commit
f1707117f0
8 changed files with 325 additions and 75 deletions
|
|
@ -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`
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
81
tests/lean/run/conv_arg.lean
Normal file
81
tests/lean/run/conv_arg.lean
Normal file
|
|
@ -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]
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue