From 44e7033c2700a697d7464ef00df0e7a239e08c19 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Sep 2021 16:56:40 -0700 Subject: [PATCH] feat: add support for `forall_congr` at `conv` --- src/Init/Conv.lean | 6 ++-- src/Lean/Elab/Tactic/Conv/Congr.lean | 47 ++++++++++++++++------------ tests/lean/conv1.lean | 20 +++++++++++- tests/lean/conv1.lean.expected.out | 13 ++++++++ 4 files changed, 63 insertions(+), 23 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index f3bbebacb9..3831014c30 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -26,8 +26,9 @@ syntax (name := whnf) "whnf" : conv syntax (name := congr) "congr" : conv syntax (name := arg) "arg " num : conv syntax (name := traceState) "traceState" : conv -syntax (name := funext) "funext" (colGt ident)* : conv +syntax (name := ext) "ext " (colGt ident)* : conv syntax (name := change) "change " term : conv +syntax (name := pattern) "pattern " term : conv syntax (name := rewrite) "rewrite " rwRuleSeq : conv syntax (name := erewrite) "erewrite " rwRuleSeq : conv syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv @@ -42,12 +43,13 @@ macro "erw " s:rwRuleSeq : conv => `(erewrite $s:rwRuleSeq) macro "args" : conv => `(congr) macro "left" : conv => `(lhs) macro "right" : conv => `(rhs) +macro "intro " xs:(colGt ident)* : conv => `(ext $(xs.getArgs)*) syntax enterArg := ident <|> num syntax "enter " "[" (colGt enterArg),+ "]": conv macro_rules | `(conv| enter [$i:numLit]) => `(conv| arg $i) - | `(conv| enter [$id:ident]) => `(conv| funext $id) + | `(conv| enter [$id:ident]) => `(conv| ext $id) | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*])) end Lean.Parser.Tactic.Conv diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 49cc07abfc..996b02cb82 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -11,16 +11,17 @@ open Meta def congr (mvarId : MVarId) : MetaM (List MVarId) := withMVarContext mvarId do - let (lhs, rhs) ← getLhsRhsCore mvarId - unless lhs.isApp do - throwError "invalid 'congr' conv tactic, application expected{indentExpr lhs}" - lhs.withApp fun f args => do + let (lhs, rhs) ← getLhsRhsCore mvarId + let lhs ← instantiateMVars lhs + trace[Meta.debug] "{lhs} = {rhs}" + unless lhs.isApp do + throwError "invalid 'congr' conv tactic, application expected{indentExpr lhs}" + lhs.withApp fun f args => do let infos := (← getFunInfoNArgs f args.size).paramInfo let mut r := { expr := f : Simp.Result } let mut newGoals := #[] let mut i := 0 for arg in args do - trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}" let addGoal ← if i < infos.size && !infos[i].hasFwdDeps then pure true @@ -34,11 +35,11 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) := r ← Simp.mkCongrFun r arg i := i + 1 let proof ← r.getProof - assignExprMVar rhs.mvarId! r.expr + unless (← isDefEqGuarded rhs r.expr) do + throwError "invalid 'congr' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr r.expr}" assignExprMVar mvarId proof return newGoals.toList - @[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do replaceMainGoal (← congr (← getMainGoal)) @@ -69,26 +70,32 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) := throwError "invalid 'arg' conv tactic, application has only {mvarIds.length} (nondependent) arguments" | _ => throwUnsupportedSyntax -private def funextCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId := +private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId := withMVarContext mvarId do - let (lhs, rhs) ← getLhsRhsCore mvarId - let lhsType ← whnfD (← inferType lhs) - unless lhsType.isForall do - throwError "invalid 'funext' conv tactic, function expected{indentD m!"{lhs} : {lhsType}"}" - let [mvarIdNew] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result" let userNames := if let some userName := userName? then [userName] else [] - let (_, mvarId) ← introN mvarIdNew 1 userNames - markAsConvGoal mvarId + let (lhs, rhs) ← getLhsRhsCore mvarId + let lhs ← instantiateMVars lhs + if lhs.isForall then + let [mvarId, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result" + let (_, mvarId) ← introN mvarId 1 userNames + markAsConvGoal mvarId + else + let lhsType ← whnfD (← inferType lhs) + unless lhsType.isForall do + throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}" + let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result" + let (_, mvarId) ← introN mvarId 1 userNames + markAsConvGoal mvarId -private def funext (userName? : Option Name) : TacticM Unit := do - replaceMainGoal [← funextCore (← getMainGoal) userName?] +private def ext (userName? : Option Name) : TacticM Unit := do + replaceMainGoal [← extCore (← getMainGoal) userName?] -@[builtinTactic Lean.Parser.Tactic.Conv.funext] def evalFunext : Tactic := fun stx => do +@[builtinTactic Lean.Parser.Tactic.Conv.ext] def evalExt : Tactic := fun stx => do let ids := stx[1].getArgs if ids.isEmpty then - funext none + ext none else for id in ids do - withRef id <| funext id.getId + withRef id <| ext id.getId end Lean.Elab.Tactic.Conv diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean index 6b6bdd33c3..c85f6bba90 100644 --- a/tests/lean/conv1.lean +++ b/tests/lean/conv1.lean @@ -56,13 +56,31 @@ example : id (fun x y => 0 + x + y) = Nat.add := by conv => lhs arg 1 - funext a b + ext a b traceState rw [Nat.zero_add] traceState +example : id (fun x y => 0 + x + y) = Nat.add := by + conv => + lhs + arg 1 + intro a b + rw [Nat.zero_add] + example : id (fun x y => 0 + x + y) = Nat.add := by conv => enter [1, 1, a, b] traceState rw [Nat.zero_add] + +example (p : Nat → Prop) (h : ∀ a, p a) : ∀ a, p (id (0 + a)) := by + conv => + intro x + traceState + arg 1 + traceState + simp only [id] + traceState + rw [Nat.zero_add] + exact h diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out index bb90fb3c0f..57165cb4c4 100644 --- a/tests/lean/conv1.lean.expected.out +++ b/tests/lean/conv1.lean.expected.out @@ -16,3 +16,16 @@ a b : Nat case h.h a b : Nat ⊢ 0 + a + b +case h +p : Nat → Prop +h : ∀ (a : Nat), p a +x : Nat +⊢ p (id (0 + x)) +p : Nat → Prop +h : ∀ (a : Nat), p a +x : Nat +⊢ id (0 + x) +p : Nat → Prop +h : ∀ (a : Nat), p a +x : Nat +⊢ 0 + x