chore: update stage0

stage0/src/Init.lean

@@ -18,3 +18,4 @@ import Init.Meta
 import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
+import Init.Conv

stage0/src/Init/Conv.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Notation for operators defined at Prelude.lean
+-/
+prelude
+import Init.Notation
+
+namespace Lean.Parser.Tactic
+
+declare_syntax_cat conv (behavior := both)
+
+syntax convSeq1Indented := withPosition((colGe conv ";"?)+)
+syntax convSeqBracketed := "{" (conv ";"?)+ "}"
+syntax convSeq := convSeq1Indented <|> convSeqBracketed
+
+syntax "skip " : conv
+syntax "lhs"   : conv
+syntax "rhs"   : conv
+syntax "whnf"  : conv
+syntax "congr" : conv
+syntax "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
+
+end Lean.Parser.Tactic

stage0/src/Lean/Elab/InfoTree.lean

@@ -78,6 +78,7 @@ structure TacticInfo extends ElabInfo where
   goalsBefore : List MVarId
   mctxAfter   : MetavarContext
   goalsAfter  : List MVarId
+  inConv      : Bool
   deriving Inhabited
 
 structure MacroExpansionInfo where
@@ -188,17 +189,17 @@ def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
   ctx.runMetaM info.lctx do
     return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
 
-def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
+def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) (inConv : Bool) : IO Format :=
   if goals.isEmpty then
     return "no goals"
   else
-    ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM Meta.ppGoal))
+    ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal . inConv)))
 
 def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
   let ctxB := { ctx with mctx := info.mctxBefore }
   let ctxA := { ctx with mctx := info.mctxAfter }
-  let goalsBefore ← ctxB.ppGoals info.goalsBefore
-  let goalsAfter  ← ctxA.ppGoals info.goalsAfter
+  let goalsBefore ← ctxB.ppGoals info.goalsBefore info.inConv
+  let goalsAfter  ← ctxA.ppGoals info.goalsAfter info.inConv
   return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
 def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do

stage0/src/Lean/Elab/Quotation.lean

@@ -195,6 +195,7 @@ elab_stx_quot Parser.Term.attr.quot
 elab_stx_quot Parser.Term.prio.quot
 elab_stx_quot Parser.Term.doElem.quot
 elab_stx_quot Parser.Term.dynamicQuot
+-- elab_stx_quot Parser.Term.conv.quot
 
 /- match -/
 

stage0/src/Lean/Elab/Tactic/Basic.lean

@@ -39,6 +39,8 @@ structure Context where
   main       : MVarId
   -- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
   elaborator : Name
+  -- `true` when in `conv` tactic mode. This flag is only used to pretty print the goals showing just the left-hand-side
+  inConv     : Bool := false
 
 structure State where
   goals : List MVarId
@@ -119,6 +121,7 @@ def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx
     stx           := stx
     mctxAfter     := (← getMCtx)
     goalsAfter    := (← getUnsolvedGoals)
+    inConv        := (← read).inConv
   }
 
 def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do

stage0/src/Lean/Meta/PPGoal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 import Lean.Meta.InferType
+import Lean.Meta.MatchUtil
 
 namespace Lean.Meta
 
@@ -143,7 +144,7 @@ end ToHide
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ Format.line
 
-def ppGoal (mvarId : MVarId) : MetaM Format := do
+def ppGoal (mvarId : MVarId) (convGoal := false) : MetaM Format := do
   match (← getMCtx).findDecl? mvarId with
   | none          => pure "unknown goal"
   | some mvarDecl => do
@@ -200,7 +201,14 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
            ppVars varNames prevType? fmt localDecl
       let fmt ← pushPending varNames type? fmt
       let fmt := addLine fmt
-      let typeFmt ← ppExpr mvarDecl.type
+      let typeFmt ←
+        if convGoal then
+          if let some (_, lhs, _) ← matchEq? mvarDecl.type then
+            ppExpr lhs
+          else
+            ppExpr mvarDecl.type
+        else
+          ppExpr mvarDecl.type
       let fmt := fmt ++ "⊢ " ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => pure fmt

stage0/src/Lean/Parser/Term.lean

@@ -26,6 +26,9 @@ builtin_initialize
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
   categoryParser `tactic rbp
 
+@[inline] def convParser (rbp : Nat := 0) : Parser :=
+  categoryParser `conv rbp
+
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
@@ -242,6 +245,7 @@ def bracketedBinderF := bracketedBinder  -- no default arg
 @[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|"  >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
 @[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|"  >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
 @[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|"  >> incQuotDepth attrParser >> ")"
+@[builtinTermParser] def conv.quot : Parser := leading_parser "`(conv|"  >> incQuotDepth convParser >> ")"
 
 @[builtinTermParser] def panic       := leading_parser:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"

stage0/stdlib/Init.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init
-// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints
+// Imports: Init.Prelude Init.Notation Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.Meta Init.NotationExtra Init.SimpLemmas Init.Hints Init.Conv
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -27,6 +27,7 @@ lean_object* initialize_Init_Meta(lean_object*);
 lean_object* initialize_Init_NotationExtra(lean_object*);
 lean_object* initialize_Init_SimpLemmas(lean_object*);
 lean_object* initialize_Init_Hints(lean_object*);
+lean_object* initialize_Init_Conv(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init(lean_object* w) {
 lean_object * res;
@@ -74,6 +75,9 @@ lean_dec_ref(res);
 res = initialize_Init_Hints(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Conv(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Elab/Quotation.c

@@ -30901,7 +30901,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__2;
 x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__3___closed__5;
-x_3 = lean_unsigned_to_nat(496u);
+x_3 = lean_unsigned_to_nat(497u);
 x_4 = lean_unsigned_to_nat(12u);
 x_5 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__4;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

stage0/stdlib/Lean/Elab/Term.c

@@ -366,7 +366,7 @@ lean_object* l_Lean_throwKernelException___at_Lean_Elab_Term_evalExpr___spec__4(
 lean_object* l_Lean_Elab_Term_mkFreshIdent___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_isMonadApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
-lean_object* l_Lean_Meta_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_ppGoal(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicit___boxed(lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__5(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -10953,9 +10953,10 @@ return x_11;
 lean_object* l_Lean_Elab_Term_ppGoal(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
-lean_object* x_9; 
-x_9 = l_Lean_Meta_ppGoal(x_1, x_4, x_5, x_6, x_7, x_8);
-return x_9;
+uint8_t x_9; lean_object* x_10; 
+x_9 = 0;
+x_10 = l_Lean_Meta_ppGoal(x_1, x_9, x_4, x_5, x_6, x_7, x_8);
+return x_10;
 }
 }
 lean_object* l_Lean_Elab_Term_ppGoal___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {

stage0/stdlib/Lean/PrettyPrinter.c

@@ -44,7 +44,6 @@ static lean_object* l_Lean_PPContext_runMetaM___rarg___closed__4;
 uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_noContext___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
-lean_object* l_Lean_Meta_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_PPContext_runMetaM___rarg___closed__9;
 extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
@@ -114,6 +113,7 @@ lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext
 lean_object* l_Lean_Parser_Module_module_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_ppGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParserCompiler_registerParserCompiler___rarg(lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_instBEqExpr;
 lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1910,13 +1910,16 @@ return x_6;
 lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_4 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal), 6, 1);
-lean_closure_set(x_4, 0, x_2);
-x_5 = lean_alloc_closure((void*)(l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1), 6, 1);
-lean_closure_set(x_5, 0, x_4);
-x_6 = l_Lean_PPContext_runMetaM___rarg(x_1, x_5, x_3);
-return x_6;
+uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_4 = 0;
+x_5 = lean_box(x_4);
+x_6 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal___boxed), 7, 2);
+lean_closure_set(x_6, 0, x_2);
+lean_closure_set(x_6, 1, x_5);
+x_7 = lean_alloc_closure((void*)(l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1), 6, 1);
+lean_closure_set(x_7, 0, x_6);
+x_8 = l_Lean_PPContext_runMetaM___rarg(x_1, x_7, x_3);
+return x_8;
 }
 }
 static lean_object* _init_l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____closed__1() {

stage0/stdlib/Lean/Widget/InteractiveCode.c

@@ -388,17 +388,19 @@ return x_3;
 static lean_object* _init_l_Lean_Widget_instInhabitedInfoWithCtx___closed__19() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; 
 x_1 = lean_box(0);
 x_2 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__18;
 x_3 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__12;
-x_4 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_4, 0, x_2);
-lean_ctor_set(x_4, 1, x_3);
-lean_ctor_set(x_4, 2, x_1);
-lean_ctor_set(x_4, 3, x_3);
-lean_ctor_set(x_4, 4, x_1);
-return x_4;
+x_4 = 0;
+x_5 = lean_alloc_ctor(0, 5, 1);
+lean_ctor_set(x_5, 0, x_2);
+lean_ctor_set(x_5, 1, x_3);
+lean_ctor_set(x_5, 2, x_1);
+lean_ctor_set(x_5, 3, x_3);
+lean_ctor_set(x_5, 4, x_1);
+lean_ctor_set_uint8(x_5, sizeof(void*)*5, x_4);
+return x_5;
 }
 }
 static lean_object* _init_l_Lean_Widget_instInhabitedInfoWithCtx___closed__20() {