feat: no-operation simps attribute, to avoid unnecessary errors in mathport output (#106)

This is lame: not an actual port of `@[simps]` in all its glory, just a no-operation attribute so we have fewer errors on declarations in the output of mathport.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -55,6 +55,7 @@ import Mathlib.Tactic.Rcases
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunTac
 import Mathlib.Tactic.ShowTerm
+import Mathlib.Tactic.Simps
 import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.Spread
 import Mathlib.Tactic.SudoSetOption

Mathlib/Mathport/Syntax.lean

@@ -12,6 +12,7 @@ import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.ShowTerm
+import Mathlib.Tactic.Simps
 import Mathlib.Tactic.SolveByElim
 
 -- To fix upstream:
@@ -638,8 +639,9 @@ syntax (name := protectProj) "protectProj" (&" without" (ppSpace ident)+)? : att
 
 syntax (name := notationClass) "notationClass" "*"? (ppSpace ident)? : attr
 
-syntax (name := simps) "simps" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
-syntax (name := simps?) "simps?" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
+-- Moved to Mathlib/Tactic/Simps.lean, but not yet implemented.
+-- syntax (name := simps) "simps" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
+-- syntax (name := simps?) "simps?" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
 
 syntax (name := mono) "mono" (ppSpace Tactic.mono.side)? : attr
 
@@ -691,14 +693,15 @@ syntax (name := restateAxiom) "restate_axiom " ident (ppSpace ident)? : command
 syntax (name := simp) "#simp" (&" only")? (" [" Tactic.simpArg,* "]")?
   (" with " ident+)? " :"? ppSpace term : command
 
-syntax simpsRule.rename := ident " → " ident
-syntax simpsRule.erase := "-" ident
-syntax simpsRule := (simpsRule.rename <|> simpsRule.erase) &" as_prefix"?
-syntax simpsProj := ident (" (" simpsRule,+ ")")?
-syntax (name := initializeSimpsProjections) "initialize_simps_projections"
-  (ppSpace simpsProj)* : command
-syntax (name := initializeSimpsProjections?) "initialize_simps_projections?"
-  (ppSpace simpsProj)* : command
+-- Moved to Mathlib/Tactic/Simps.lean, but not yet implemented.
+-- syntax simpsRule.rename := ident " → " ident
+-- syntax simpsRule.erase := "-" ident
+-- syntax simpsRule := (simpsRule.rename <|> simpsRule.erase) &" as_prefix"?
+-- syntax simpsProj := ident (" (" simpsRule,+ ")")?
+-- syntax (name := initializeSimpsProjections) "initialize_simps_projections"
+--   (ppSpace simpsProj)* : command
+-- syntax (name := initializeSimpsProjections?) "initialize_simps_projections?"
+--   (ppSpace simpsProj)* : command
 
 syntax (name := «where») "#where" : command
 

Mathlib/Tactic/Simps.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2019 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+
+import Lean
+
+/-!
+# Stub for implementation of the `@[simps]` attribute.
+
+This file is currently just a stub that creates a no-operation `@[simps]` attribute.
+Without this, all declarations in the mathport output for mathlib3 that use `@[simps]` fail.
+With the no-operation attribute, the declarations can succeed,
+but of course all later proofs that rely on the existence of the automatically generated lemmas
+will fail.
+
+Later we will need to port the implementation from mathlib3.
+
+-/
+
+
+open Lean Meta
+
+namespace Attr
+
+syntax (name := simps) "simps" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
+syntax (name := simps?) "simps?" (" (" &"config" " := " term ")")? (ppSpace ident)* : attr
+
+end Attr
+
+namespace Command
+
+syntax simpsRule.rename := ident " → " ident
+syntax simpsRule.erase := "-" ident
+syntax simpsRule := (simpsRule.rename <|> simpsRule.erase) &" as_prefix"?
+syntax simpsProj := ident (" (" simpsRule,+ ")")?
+syntax (name := initializeSimpsProjections) "initialize_simps_projections"
+  (ppSpace simpsProj)* : command
+syntax (name := initializeSimpsProjections?) "initialize_simps_projections?"
+  (ppSpace simpsProj)* : command
+
+end Command
+
+-- Defines the user attribute `simps` for automatic generation of `@[simp]` lemmas for projections.
+initialize simpsAttr : ParametricAttribute (Array Name) ←
+  registerParametricAttribute {
+    name := `simps
+    descr := "Automatically derive lemmas specifying the projections of this declaration.",
+    getParam := fun decl stx =>
+      match stx with
+        -- TODO implement support for `config := ...`
+        | `(attr|simps $[$ids]*) => ids.mapM (·.getId.eraseMacroScopes)
+        | _ => throwError "unexpected simps syntax {stx}"
+  }

test/Simps.lean

@@ -0,0 +1,14 @@
+import Mathlib.Tactic.Simps
+
+/-!
+We currently only have a no-operation implementation of `@[simps]`,
+so there isn't much to test here.
+-/
+
+structure X :=
+(a : Nat)
+(h : a = 3)
+
+@[simps]
+def x : X :=
+⟨3, rfl⟩