feat: port the 'alias' command (#293)

Compare to https://github.com/leanprover-community/mathlib/blob/07c83c81c0016c1ac08e8c9c3f1260c2f4c6ac7f/src/tactic/alias.lean

The `mkIffMpApp` and `aliasIff` functions are direct translations of the mathlib3 versions.

Author: dwrensha

Mathlib.lean

@@ -57,6 +57,7 @@ import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename
 import Mathlib.Mathport.SpecialNames
 import Mathlib.Mathport.Syntax
+import Mathlib.Tactic.Alias
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Cache
 import Mathlib.Tactic.Cases

Mathlib/Mathport/Syntax.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.Command
 import Lean.Elab.Quotation
+import Mathlib.Tactic.Alias
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.CommandQuote
@@ -582,8 +583,6 @@ namespace Command
   (" from" (ppSpace ident)+)? (" := " str)? : command
 
 /- M -/ syntax (name := addHintTactic) "add_hint_tactic " tactic : command
-/- M -/ syntax (name := alias) "alias " ident " ← " ident* : command
-/- M -/ syntax (name := aliasLR) "alias " ident " ↔ " (".." <|> (binderIdent binderIdent)) : command
 
 /- S -/ syntax (name := explode) "#explode " ident : command
 

Mathlib/Tactic/Alias.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, David Renshaw
+-/
+import Lean.Elab.Command
+import Lean.Elab.Term
+import Lean
+
+/-!
+# The `alias` command
+
+This file defines an `alias` command, which can be used to create copies
+of a theorem or definition with different names.
+
+Syntax:
+
+```lean
+/-- doc string -/
+alias my_theorem ← alias1 alias2 ...
+```
+
+This produces defs or theorems of the form:
+
+```lean
+/-- doc string -/
+theorem alias1 : <type of my_theorem> := my_theorem
+
+/-- doc string -/
+theorem alias2 : <type of my_theorem> := my_theorem
+```
+
+Iff alias syntax:
+
+```lean
+alias A_iff_B ↔ B_of_A A_of_B
+alias A_iff_B ↔ ..
+```
+
+This gets an existing biconditional theorem `A_iff_B` and produces
+the one-way implications `B_of_A` and `A_of_B` (with no change in
+implicit arguments). A blank `_` can be used to avoid generating one direction.
+The `..` notation attempts to generate the 'of'-names automatically when the
+input theorem has the form `A_iff_B` or `A_iff_B_left` etc.
+-/
+
+namespace Tactic
+namespace Alias
+
+open Lean
+
+/-- Adds some copies of a theorem or definition. -/
+syntax (name := alias) "alias " ident " ← " ident* : command
+
+/-- Adds one-way implication declarations. -/
+syntax (name := aliasLR) "alias " ident " ↔ " binderIdent binderIdent : command
+
+/-- Adds one-way implication declarations, inferring names for them. -/
+syntax (name := aliasLRDots) "alias " ident " ↔ " ".." : command
+
+/-- Like `++`, except that if the right argument starts with `_root_` the namespace will be
+ignored.
+```
+appendNamespace `a.b `c.d = `a.b.c.d
+appendNamespace `a.b `_root_.c.d = `c.d
+```
+
+TODO: Move this declaration to a more central location.
+-/
+def appendNamespace (ns : Name) : Name → Name
+| Name.str Name.anonymous s _ => if s = "_root_" then Name.anonymous else Name.mkStr ns s
+| Name.str p s _              => Name.mkStr (appendNamespace ns p) s
+| Name.num p n _              => Name.mkNum (appendNamespace ns p) n
+| Name.anonymous              => ns
+
+/-- Elaborates an `alias ←` command. -/
+@[commandElab «alias»] def elabAlias : Elab.Command.CommandElab
+| `(alias $name:ident ← $aliases:ident*) => do
+  let resolved ← resolveGlobalConstNoOverload name
+  let constant ← getConstInfo resolved
+  let ns ← getCurrNamespace
+
+  for a in aliases do
+    let decl ← match constant with
+    | Lean.ConstantInfo.defnInfo d =>
+      pure $ .defnDecl {
+        d with name := (appendNamespace ns a.getId)
+               value := mkConst resolved (d.levelParams.map mkLevelParam)
+      }
+    | Lean.ConstantInfo.thmInfo t =>
+      pure $ .thmDecl {
+        t with name := (appendNamespace ns a.getId)
+               value := mkConst resolved (t.levelParams.map mkLevelParam)
+      }
+    | _ => throwError "alias only works with def or theorem"
+
+    -- TODO add @alias attribute
+    Lean.addDecl decl
+
+| _ => Lean.Elab.throwUnsupportedSyntax
+
+
+/--
+  Given a possibly forall-quantified iff expression `prf`, produce a value for one
+  of the implication directions (determined by `mp`).
+-/
+def mkIffMpApp (mp : Bool) (prf : Expr) : MetaM Expr := do
+  Meta.forallTelescope (← Meta.inferType prf) fun xs ty => do
+    let some (lhs, rhs) := ty.iff?
+        | throwError "Target theorem must have the form `∀ x y z, a ↔ b`"
+    Meta.mkLambdaFVars xs <|
+      mkApp3 (mkConst (if mp then ``Iff.mp else ``Iff.mpr)) lhs rhs (mkAppN prf xs)
+
+/--
+  Given a constant representing an iff decl, adds a decl for one of the implication
+  directions.
+-/
+def aliasIff (ci : ConstantInfo) (al : Name) (isForward : Bool) : MetaM Unit := do
+  let ls := ci.levelParams
+  let v ← mkIffMpApp isForward ci.value!
+  let t' ← Meta.inferType v
+  -- TODO add @alias attribute
+  addDecl $ .thmDecl {
+      name := al
+      value := v
+      type := t'
+      levelParams := ls
+  }
+
+/-- Elaborates an `alias ↔` command. -/
+@[commandElab aliasLR] def elabAliasLR : Lean.Elab.Command.CommandElab
+| `(alias $name:ident ↔ $left:binderIdent $right:binderIdent ) => do
+   let resolved ← resolveGlobalConstNoOverload name
+   let constant ← getConstInfo resolved
+   let ns ← getCurrNamespace
+
+   Lean.Elab.Command.liftTermElabM none do
+     if let `(binderIdent| $x:ident) := left
+     then aliasIff constant (appendNamespace ns x.getId) true
+
+     if let `(binderIdent| $x:ident) := right
+     then aliasIff constant (appendNamespace ns x.getId) false
+
+| _ => Lean.Elab.throwUnsupportedSyntax
+
+/-- Elaborates an `alias ↔ ..` command. -/
+@[commandElab aliasLRDots] def elabAliasLRDots : Lean.Elab.Command.CommandElab
+| `(alias $name:ident ↔ ..) => do
+  let resolved ← resolveGlobalConstNoOverload name
+  let constant ← getConstInfo resolved
+
+  let (parent, base) ← match resolved with
+                       | Name.str n s _ => pure (n,s)
+                       | _ => throwError "alias only works for string names"
+
+  let components := base.splitOn "_iff_"
+  if components.length != 2 then throwError "LHS must be of the form *_iff_*"
+  let forward := String.intercalate "_of_" components.reverse
+  let backward := String.intercalate "_of_" components
+  let forwardName := Name.mkStr parent forward
+  let backwardName := Name.mkStr parent backward
+
+  Lean.Elab.Command.liftTermElabM none do
+    aliasIff constant forwardName true
+    aliasIff constant backwardName false
+
+| _ => Lean.Elab.throwUnsupportedSyntax
+
+end Alias
+end Tactic

test/Alias.lean

@@ -0,0 +1,58 @@
+import Mathlib
+
+namespace Alias
+namespace A
+
+theorem foo : 1 + 1 = 2 := rfl
+alias foo ← foo1 foo2 foo3 _root_.B.foo4
+example : 1 + 1 = 2 := foo1
+example : 1 + 1 = 2 := foo2
+example : 1 + 1 = 2 := foo3
+
+def bar : Nat := 5
+alias bar ← bar1 bar2
+example : bar1 = 5 := rfl
+example : bar2 = 5 := rfl
+
+theorem baz (x : Nat) : x = x := rfl
+alias baz ← baz1
+example : 3 = 3 := baz1 3
+
+theorem ab_iff_ba {t : Type} {a b : t} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
+alias ab_iff_ba ↔ ba_of_ab ab_of_ba
+example {a b : Nat} : a = b → b = a := ba_of_ab
+example {t : Type} {a b : t} : b = a → a = b := ab_of_ba
+
+theorem a_iff_a_and_a (a : Prop) : a ↔ a ∧ a :=
+  Iff.intro (λ x => ⟨x,x⟩) (λ x => x.1)
+
+alias a_iff_a_and_a ↔ forward _
+alias a_iff_a_and_a ↔ _ backward
+
+example : True → True ∧ True := forward True
+example : True ∧ True → True := backward True
+
+alias a_iff_a_and_a ↔ ..
+example : True → True ∧ True := a_and_a_of_a True
+example : True ∧ True → True := a_of_a_and_a True
+
+end A
+
+-- test namespacing
+example : 1 + 1 = 2 := A.foo1
+example : 1 + 1 = 2 := B.foo4
+example : True → True ∧ True := A.a_and_a_of_a True
+example : True → True ∧ True := A.forward True
+example : True ∧ True → True := A.backward True
+
+namespace C
+
+alias A.a_iff_a_and_a ↔ _root_.B.forward2 _
+alias A.a_iff_a_and_a ↔ _ _root_.B.backward2
+
+end C
+
+example : True → True ∧ True := B.forward2 True
+example : True ∧ True → True := B.backward2 True
+
+end Alias