From 90b08ef22e0285a5bc92d4eb807b8f3084b963cf Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 12 Feb 2024 10:25:04 +1100 Subject: [PATCH] feat: upstream guard_expr (#3297) Co-authored-by: Leonardo de Moura --- src/Init.lean | 1 + src/Init/Guard.lean | 129 ++++++++++++++++++++++++++ src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/Guard.lean | 158 ++++++++++++++++++++++++++++++++ tests/lean/run/guardexpr.lean | 57 ++++++++++++ 5 files changed, 346 insertions(+) create mode 100644 src/Init/Guard.lean create mode 100644 src/Lean/Elab/Tactic/Guard.lean create mode 100644 tests/lean/run/guardexpr.lean diff --git a/src/Init.lean b/src/Init.lean index 6aeeb5525c..7daabd1a7b 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -25,5 +25,6 @@ import Init.NotationExtra import Init.SimpLemmas import Init.Hints import Init.Conv +import Init.Guard import Init.Simproc import Init.SizeOfLemmas diff --git a/src/Init/Guard.lean b/src/Init/Guard.lean new file mode 100644 index 0000000000..03877c2eb9 --- /dev/null +++ b/src/Init/Guard.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2021 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +prelude +import Init.Tactics +import Init.Conv +import Init.NotationExtra + +namespace Lean.Parser + +/-- Reducible defeq matching for `guard_hyp` types -/ +syntax colonR := " : " +/-- Default-reducibility defeq matching for `guard_hyp` types -/ +syntax colonD := " :~ " +/-- Syntactic matching for `guard_hyp` types -/ +syntax colonS := " :ₛ " +/-- Alpha-eq matching for `guard_hyp` types -/ +syntax colonA := " :ₐ " +/-- The `guard_hyp` type specifier, one of `:`, `:~`, `:ₛ`, `:ₐ` -/ +syntax colon := colonR <|> colonD <|> colonS <|> colonA + +/-- Reducible defeq matching for `guard_hyp` values -/ +syntax colonEqR := " := " +/-- Default-reducibility defeq matching for `guard_hyp` values -/ +syntax colonEqD := " :=~ " +/-- Syntactic matching for `guard_hyp` values -/ +syntax colonEqS := " :=ₛ " +/-- Alpha-eq matching for `guard_hyp` values -/ +syntax colonEqA := " :=ₐ " +/-- The `guard_hyp` value specifier, one of `:=`, `:=~`, `:=ₛ`, `:=ₐ` -/ +syntax colonEq := colonEqR <|> colonEqD <|> colonEqS <|> colonEqA + +/-- Reducible defeq matching for `guard_expr` -/ +syntax equalR := " = " +/-- Default-reducibility defeq matching for `guard_expr` -/ +syntax equalD := " =~ " +/-- Syntactic matching for `guard_expr` -/ +syntax equalS := " =ₛ " +/-- Alpha-eq matching for `guard_expr` -/ +syntax equalA := " =ₐ " +/-- The `guard_expr` matching specifier, one of `=`, `=~`, `=ₛ`, `=ₐ` -/ +syntax equal := equalR <|> equalD <|> equalS <|> equalA + +namespace Tactic + +/-- +Tactic to check equality of two expressions. +* `guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency. +* `guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency. +* `guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal. +* `guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent. + +Both `e` and `e'` are elaborated then have their metavariables instantiated before the equality +check. Their types are unified (using `isDefEqGuarded`) before synthetic metavariables are +processed, which helps with default instance handling. +-/ +syntax (name := guardExpr) "guard_expr " term:51 equal term : tactic +@[inherit_doc guardExpr] +syntax (name := guardExprConv) "guard_expr " term:51 equal term : conv + +/-- +Tactic to check that the target agrees with a given expression. +* `guard_target = e` checks that the target is defeq at reducible transparency to `e`. +* `guard_target =~ e` checks that the target is defeq at default transparency to `e`. +* `guard_target =ₛ e` checks that the target is syntactically equal to `e`. +* `guard_target =ₐ e` checks that the target is alpha-equivalent to `e`. + +The term `e` is elaborated with the type of the goal as the expected type, which is mostly +useful within `conv` mode. +-/ +syntax (name := guardTarget) "guard_target " equal term : tactic +@[inherit_doc guardTarget] +syntax (name := guardTargetConv) "guard_target " equal term : conv + +/-- +Tactic to check that a named hypothesis has a given type and/or value. + +* `guard_hyp h : t` checks the type up to reducible defeq, +* `guard_hyp h :~ t` checks the type up to default defeq, +* `guard_hyp h :ₛ t` checks the type up to syntactic equality, +* `guard_hyp h :ₐ t` checks the type up to alpha equality. +* `guard_hyp h := v` checks value up to reducible defeq, +* `guard_hyp h :=~ v` checks value up to default defeq, +* `guard_hyp h :=ₛ v` checks value up to syntactic equality, +* `guard_hyp h :=ₐ v` checks the value up to alpha equality. + +The value `v` is elaborated using the type of `h` as the expected type. +-/ +syntax (name := guardHyp) + "guard_hyp " term:max (colon term)? (colonEq term)? : tactic +@[inherit_doc guardHyp] syntax (name := guardHypConv) + "guard_hyp " term:max (colon term)? (colonEq term)? : conv + +end Tactic + +namespace Command + +/-- +Command to check equality of two expressions. +* `#guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency. +* `#guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency. +* `#guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal. +* `#guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent. + +This is a command version of the `guard_expr` tactic. -/ +syntax (name := guardExprCmd) "#guard_expr " term:51 equal term : command + +/-- +Command to check that an expression evaluates to `true`. + +`#guard e` elaborates `e` ensuring its type is `Bool` then evaluates `e` and checks that +the result is `true`. The term is elaborated *without* variables declared using `variable`, since +these cannot be evaluated. + +Since this makes use of coercions, so long as a proposition `p` is decidable, one can write +`#guard p` rather than `#guard decide p`. A consequence to this is that if there is decidable +equality one can write `#guard a = b`. Note that this is not exactly the same as checking +if `a` and `b` evaluate to the same thing since it uses the `DecidableEq` instance to do +the evaluation. + +Note: this uses the untrusted evaluator, so `#guard` passing is *not* a proof that the +expression equals `true`. -/ +syntax (name := guardCmd) "#guard " term : command + +end Command + +end Lean.Parser diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 0c477250a0..b8e83c8444 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -23,4 +23,5 @@ import Lean.Elab.Tactic.Unfold import Lean.Elab.Tactic.Cache import Lean.Elab.Tactic.Calc import Lean.Elab.Tactic.Congr +import Lean.Elab.Tactic.Guard import Lean.Elab.Tactic.RCases diff --git a/src/Lean/Elab/Tactic/Guard.lean b/src/Lean/Elab/Tactic/Guard.lean new file mode 100644 index 0000000000..60e7822bba --- /dev/null +++ b/src/Lean/Elab/Tactic/Guard.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2021 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, Leonardo de Moura +-/ +import Lean.Elab.Command +import Lean.Elab.Tactic.Conv.Basic +import Lean.Meta.Basic +import Lean.Meta.Eval + +namespace Lean.Elab.Tactic.GuardExpr +open Meta + +/-- +The various `guard_*` tactics have similar matching specifiers for how equal expressions +have to be to pass the tactic. +This inductive gives the different specifiers that can be selected. +-/ +inductive MatchKind +/-- A syntactic match means that the `Expr`s are `==` after stripping `MData` -/ +| syntactic +/-- A defeq match `isDefEqGuarded` returns true. (Note that unification is allowed here.) -/ +| defEq (red : TransparencyMode := .reducible) +/-- An alpha-eq match means that `Expr.eqv` returns true. -/ +| alphaEq + +open Lean.Parser Lean.Parser.Tactic Lean.Parser.Command + +/-- Converts a `colon` syntax into a `MatchKind` -/ +def colon.toMatchKind : TSyntax ``colon → Option MatchKind + | `(colon| :) => some .defEq + | `(colon| :~) => some (.defEq .default) + | `(colon| :ₛ) => some .syntactic + | `(colon| :ₐ) => some .alphaEq + | _ => none + +/-- Converts a `colonEq` syntax into a `MatchKind` -/ +def colonEq.toMatchKind : TSyntax ``colonEq → Option MatchKind + | `(colonEq| :=) => some .defEq + | `(colonEq| :=~) => some (.defEq .default) + | `(colonEq| :=ₛ) => some .syntactic + | `(colonEq| :=ₐ) => some .alphaEq + | _ => none + +/-- Converts a `equal` syntax into a `MatchKind` -/ +def equal.toMatchKind : TSyntax ``equal → Option MatchKind + | `(equal| =) => some .defEq + | `(equal| =~) => some (.defEq .default) + | `(equal| =ₛ) => some .syntactic + | `(equal| =ₐ) => some .alphaEq + | _ => none + +/-- Applies the selected matching rule to two expressions. -/ +def MatchKind.isEq (a b : Expr) : MatchKind → MetaM Bool + | .syntactic => return a.consumeMData == b.consumeMData + | .alphaEq => return a.eqv b + | .defEq red => withoutModifyingState <| withTransparency red <| Lean.Meta.isDefEqGuarded a b + + +/-- Elaborate `a` and `b` and then do the given equality test `mk`. We make sure to unify +the types of `a` and `b` after elaboration so that when synthesizing pending metavariables +we don't get the wrong instances due to default instances (for example, for nat literals). -/ +def elabAndEvalMatchKind (mk : MatchKind) (a b : Term) : TermElabM Bool := + Term.withoutErrToSorry do + let a ← Term.elabTerm a none + let b ← Term.elabTerm b none + -- Unify types before synthesizing pending metavariables: + _ ← isDefEqGuarded (← inferType a) (← inferType b) + Term.synthesizeSyntheticMVarsNoPostponing + mk.isEq (← instantiateMVars a) (← instantiateMVars b) + +@[builtin_tactic guardExpr] +def evalGuardExpr : Tactic := fun + | `(tactic| guard_expr $r $eq:equal $p) + | `(conv| guard_expr $r $eq:equal $p) => withMainContext do + let some mk := equal.toMatchKind eq | throwUnsupportedSyntax + let res ← elabAndEvalMatchKind mk r p + -- Note: `{eq}` itself prints a space before the relation. + unless res do throwError "failed: {r}{eq} {p} is not true" + | _ => throwUnsupportedSyntax + +-- TODO: This is workaround. We currently allow two occurrences of `builtin_tactic`. +@[builtin_tactic guardExprConv] +def evalGuardExprConv : Tactic := evalGuardExpr + +@[builtin_tactic guardTarget] +def evalGuardTarget : Tactic := + let go eq r getTgt := withMainContext do + let t ← getTgt >>= instantiateMVars + let r ← elabTerm r (← inferType t) + let some mk := equal.toMatchKind eq | throwUnsupportedSyntax + unless ← mk.isEq r t do + throwError "target of main goal is{indentExpr t}\nnot{indentExpr r}" + fun + | `(tactic| guard_target $eq $r) => go eq r getMainTarget + | `(conv| guard_target $eq $r) => go eq r Conv.getLhs + | _ => throwUnsupportedSyntax + +-- See comment above +@[builtin_tactic guardTargetConv] +def evalGuardTargetConv : Tactic := evalGuardTarget + +@[builtin_tactic guardHyp] +def evalGuardHyp : Tactic := fun + | `(tactic| guard_hyp $h $[$c $ty]? $[$eq $val]?) + | `(conv| guard_hyp $h $[$c $ty]? $[$eq $val]?) => withMainContext do + let fvarid ← getFVarId h + let lDecl ← + match (← getLCtx).find? fvarid with + | none => throwError m!"hypothesis {h} not found" + | some lDecl => pure lDecl + if let (some c, some p) := (c, ty) then + let some mk := colon.toMatchKind c | throwUnsupportedSyntax + let e ← elabTerm p none + let hty ← instantiateMVars lDecl.type + unless ← mk.isEq e hty do + throwError m!"hypothesis {h} has type{indentExpr hty}\nnot{indentExpr e}" + match lDecl.value?, val with + | none, some _ => throwError m!"{h} is not a let binding" + | some _, none => throwError m!"{h} is a let binding" + | some hval, some val => + let some mk := eq.bind colonEq.toMatchKind | throwUnsupportedSyntax + let e ← elabTerm val lDecl.type + let hval ← instantiateMVars hval + unless ← mk.isEq e hval do + throwError m!"hypothesis {h} has value{indentExpr hval}\nnot{indentExpr e}" + | none, none => pure () + | _ => throwUnsupportedSyntax + +@[builtin_tactic guardHypConv] +def evalGuardHypConv : Tactic := evalGuardHyp + +@[builtin_command_elab guardExprCmd] +def evalGuardExprCmd : Lean.Elab.Command.CommandElab + | `(command| #guard_expr $r $eq:equal $p) => + Lean.Elab.Command.runTermElabM fun _ => do + let some mk := equal.toMatchKind eq | throwUnsupportedSyntax + let res ← elabAndEvalMatchKind mk r p + -- Note: `{eq}` itself prints a space before the relation. + unless res do throwError "failed: {r}{eq} {p} is not true" + | _ => throwUnsupportedSyntax + +@[builtin_command_elab guardCmd] +def evalGuardCmd : Lean.Elab.Command.CommandElab + | `(command| #guard $e:term) => Lean.Elab.Command.liftTermElabM do + let e ← Term.elabTermEnsuringType e (mkConst ``Bool) + Term.synthesizeSyntheticMVarsNoPostponing + let e ← instantiateMVars e + let mvars ← getMVars e + if mvars.isEmpty then + let v ← unsafe evalExpr Bool (mkConst ``Bool) e + unless v do + throwError "expression{indentExpr e}\ndid not evaluate to `true`" + else + _ ← Term.logUnassignedUsingErrorInfos mvars + | _ => throwUnsupportedSyntax + +end Lean.Elab.Tactic.GuardExpr diff --git a/tests/lean/run/guardexpr.lean b/tests/lean/run/guardexpr.lean new file mode 100644 index 0000000000..e84fae31c9 --- /dev/null +++ b/tests/lean/run/guardexpr.lean @@ -0,0 +1,57 @@ +example (n : Nat) : Nat := by + guard_hyp n :ₛ Nat + let m : Nat := 1 + guard_expr 1 =ₛ (by exact 1) + fail_if_success guard_expr 1 = (by exact 2) + guard_hyp m := 1 + guard_hyp m : (fun x => x) Nat :=~ id 1 + guard_target = Nat + have : 1 = 1 := by conv => + guard_hyp m := 1 + guard_expr ‹Nat› = m + fail_if_success guard_target = 1 + lhs + guard_target = 1 + exact 0 + +-- Now with a generic type to test that default instances work correctly +example [∀ n, OfNat α n] (n : α) : α := by + guard_hyp n + fail_if_success guard_hyp m + guard_hyp n :ₛ α + let q : α := 1 + guard_expr (1 : α) =ₛ 1 + fail_if_success guard_expr 1 =ₛ (2 : α) + fail_if_success guard_expr 1 =ₛ (by exact (2 : α)) + guard_hyp q := 1 + guard_hyp q : α := 1 + guard_hyp q : (fun x => x) α :=~ id 1 + guard_target = α + have : (1 : α) = 1 := by conv => + guard_hyp q := 1 + guard_expr ‹α› = q + fail_if_success guard_target = 1 + lhs + guard_target = 1 + exact 0 + +#guard_expr 1 = 1 +#guard_expr 1 =ₛ 1 +#guard_expr 2 = 1 + 1 + +section +variable {α : Type} [∀ n, OfNat α n] +#guard_expr (1 : α) = 1 +end + +#guard true +#guard 2 == 1 + 1 +#guard 2 = 1 + 1 + +instance (p : Bool → Prop) [DecidablePred p] : Decidable (∀ b, p b) := + if h : p false ∧ p true then + isTrue (by { intro b; cases h; cases b <;> assumption }) + else + isFalse (by { intro h'; simp [h'] at h }) + +#guard ∀ (b : Bool), b = !!b