From 232eefcef9686efd5266d8ac12c64f4cba158d76 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jul 2020 16:11:44 -0700
Subject: [PATCH] feat: add auxiliary constructions for inductive types

---
 src/Lean/Elab/Command.lean     |  3 +++
 src/Lean/Elab/Inductive.lean   | 26 +++++++++++++++++++++++++-
 tests/lean/run/inductive1.lean |  6 ++++++
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 6b56cbfeb4..e8422eae35 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -249,6 +249,9 @@ _root_.dbgTrace (toString a) $ fun _ => pure ()
 def setEnv (newEnv : Environment) : CommandElabM Unit :=
 modify $ fun s => { s with env := newEnv }
 
+@[inline] def modifyEnv (f : Environment → Environment) : CommandElabM Unit :=
+modify $ fun s => { s with env := f s.env }
+
 def getCurrNamespace : CommandElabM Name := do
 scope ← getScope; pure scope.currNamespace
 
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index a54bfcc96e..59ce9d23af 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Util.ReplaceLevel
 import Lean.Util.ReplaceExpr
 import Lean.Util.CollectLevelParams
+import Lean.Util.Constructions
 import Lean.Elab.Command
 import Lean.Elab.CollectFVars
 import Lean.Elab.Definition
@@ -441,10 +442,33 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
         let indTypes := applyInferMod views numParams indTypes;
         pure $ Declaration.inductDecl levelParams numParams indTypes isUnsafe
 
+private def mkAuxConstructions (views : Array InductiveView) : CommandElabM Unit := do
+env ← getEnv;
+let hasEq   := env.contains `Eq;
+let hasHEq  := env.contains `HEq;
+let hasUnit := env.contains `PUnit;
+let hasProd := env.contains `Prod;
+views.forM fun view => do {
+  let n := view.declName;
+  modifyEnv fun env => mkRecOn env n;
+  when hasUnit $ modifyEnv fun env => mkCasesOn env n;
+  when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env n;
+  when (hasUnit && hasProd) $ modifyEnv fun env => mkBelow env n;
+  when (hasUnit && hasProd) $ modifyEnv fun env => mkIBelow env n;
+  pure ()
+};
+views.forM fun view => do {
+  let n := view.declName;
+  when (hasUnit && hasProd) $ modifyEnv fun env => mkBRecOn env n;
+  when (hasUnit && hasProd) $ modifyEnv fun env => mkBInductionOn env n;
+  pure ()
+}
+
 def elabInductiveCore (views : Array InductiveView) : CommandElabM Unit := do
 let view0 := views.get! 0;
 decl ← runTermElabM view0.declName $ fun vars => mkInductiveDecl vars views;
-addDecl view0.ref decl
+addDecl view0.ref decl;
+mkAuxConstructions views
 
 end Command
 end Elab
diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean
index cf3cf9b638..fff597b530 100644
--- a/tests/lean/run/inductive1.lean
+++ b/tests/lean/run/inductive1.lean
@@ -43,3 +43,9 @@ inductive V (α : Type _) : Nat → Type _
 #check @V.nil
 #check @V.cons
 #check @V.rec
+#check @V.noConfusion
+#check @V.brecOn
+#check @V.binductionOn
+#check @V.casesOn
+#check @V.recOn
+#check @V.below