fix: match_expr parser

closes #3989
closes #3990

src/Lean/Elab/StructInst.lean

@@ -821,9 +821,7 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
-    -- to ensure they are unfolded here
-    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
+    match (← reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn

src/Lean/Elab/Structure.lean

@@ -82,6 +82,15 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
   | StructFieldKind.subobject => true
   | _                         => false
 
+structure ElabStructResult where
+  decl            : Declaration
+  projInfos       : List ProjectionInfo
+  projInstances   : List Name -- projections (to parent classes) that must be marked as instances.
+  mctx            : MetavarContext
+  lctx            : LocalContext
+  localInsts      : LocalInstances
+  defaultAuxDecls : Array (Name × Expr × Expr)
+
 private def defaultCtorName := `mk
 
 /-
@@ -704,8 +713,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some info =>
-                match info.type.getForallBody.getAppFn with
+              | some (ConstantInfo.defnInfo val) =>
+                match val.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

src/Lean/Meta/Basic.lean

@@ -313,12 +313,6 @@ structure Context where
   progress processing universe constraints.
   -/
   univApprox        : Bool := false
-  /--
-  `inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
-   resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
-   This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
-  -/
-  inTypeClassResolution : Bool := false
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the

src/Lean/Meta/ExprDefEq.lean

@@ -1759,7 +1759,7 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .eq =>
       -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
       -- if `f` is not a projection. The projection case generates a performance regression.
-      if tInfo.name == sInfo.name then
+      if tInfo.name == sInfo.name && !(← isProjectionFn tInfo.name) then
         if t.isApp && s.isApp && (← tryHeuristic t s) then
           return .eq
         else
@@ -1803,11 +1803,8 @@ where
     | _, _ => Meta.isExprDefEqAux t s
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | .proj m i t, .proj n j s => do
-    if (← read).inTypeClassResolution then
-      -- See comment at `inTypeClassResolution`
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
-    else if i == j && m == n then
+  | .proj m i t, .proj n j s =>
+    if i == j && m == n then
       isDefEqProjDelta t s i
     else
       return false

src/Lean/Meta/ExprLens.lean

@@ -21,28 +21,27 @@ section ExprLens
 
 open Lean.SubExpr
 
-variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
+variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
 
 /-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
 If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
 Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
 
 See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
-private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
-  match n, e with
-  | 0, .app f a         => return e.updateApp! (← g f) a
-  | 1, .app f a         => return e.updateApp! f (← g a)
-  | 0, .lam _ y b _     => return e.updateLambdaE! (← g y) b
-  | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
-  | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
-  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
-  | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .proj _ _ b      => e.updateProj! <$> g b
-  | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a
-  | 3, _                => throwError "Lensing on types is not supported"
-  | c, e                => throwError "Invalid coordinate {c} for {e}"
+private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr
+  | 0, e@(Expr.app f a)         => return e.updateApp! (← g f) a
+  | 1, e@(Expr.app f a)         => return e.updateApp! f (← g a)
+  | 0, e@(Expr.lam _ y b _)     => return e.updateLambdaE! (← g y) b
+  | 1,   (Expr.lam n y b c)     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b
+  | 1,   (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.letE _ y a b _)  => return e.updateLet! (← g y) a b
+  | 1, e@(Expr.letE _ y a b _)  => return e.updateLet! y (← g a) b
+  | 2,   (Expr.letE n y a b _)  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.proj _ _ b)      => e.updateProj! <$> g b
+  | n, e@(Expr.mdata _ a)       => e.updateMData! <$> lensCoord g n a
+  | 3, _                        => throwError "Lensing on types is not supported"
+  | c, e                        => throwError "Invalid coordinate {c} for {e}"
 
 private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr
   | [], e => g e
@@ -57,21 +56,20 @@ def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Exp
 /-- Runs `k` on the given coordinate, including handling binders properly.
 The subexpression value passed to `k` is not instantiated with respect to the
 array of free variables. -/
-private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
-  match n, e with
-  | 3, _                => throwError "Internal: Types should be handled by viewAux"
-  | 0, .app f _         => k fvars f
-  | 1, .app _ a         => k fvars a
-  | 0, .lam _ y _ _     => k fvars y
-  | 1, .lam n y b c     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .forallE _ y _ _ => k fvars y
-  | 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .letE _ y _ _ _  => k fvars y
-  | 1, .letE _ _ a _ _  => k fvars a
-  | 2, .letE n y a b _  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .proj _ _ b      => k fvars b
-  | n, .mdata _ a       => viewCoordAux k fvars n a
-  | c, e                => throwError "Invalid coordinate {c} for {e}"
+private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α
+  | 3, _                      => throwError "Internal: Types should be handled by viewAux"
+  | 0, (Expr.app f _)         => k fvars f
+  | 1, (Expr.app _ a)         => k fvars a
+  | 0, (Expr.lam _ y _ _)     => k fvars y
+  | 1, (Expr.lam n y b c)     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.forallE _ y _ _) => k fvars y
+  | 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.letE _ y _ _ _)  => k fvars y
+  | 1, (Expr.letE _ _ a _ _)  => k fvars a
+  | 2, (Expr.letE n y a b _)  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.proj _ _ b)      => k fvars b
+  | n, (Expr.mdata _ a)       => viewCoordAux k fvars n a
+  | c, e                      => throwError "Invalid coordinate {c} for {e}"
 
 private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
   | [],         e => k fvars <| e.instantiateRev fvars
@@ -121,24 +119,24 @@ open Lean.SubExpr
 
 section ViewRaw
 
-variable [Monad M] [MonadError M]
+variable {M} [Monad M] [MonadError M]
 
 /-- Get the raw subexpression without performing any instantiation. -/
-private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
-  match e, n with
-  | e,                3 => throwError "Can't viewRaw the type of {e}"
-  | .app f _,         0 => pure f
-  | .app _ a,         1 => pure a
-  | .lam _ y _ _,     0 => pure y
-  | .lam _ _ b _,     1 => pure b
-  | .forallE _ y _ _, 0 => pure y
-  | .forallE _ _ b _, 1 => pure b
-  | .letE _ y _ _ _,  0 => pure y
-  | .letE _ _ a _ _,  1 => pure a
-  | .letE _ _ _ b _,  2 => pure b
-  | .proj _ _ b,      0 => pure b
-  | .mdata _ a,       n => viewCoordRaw a n
-  | e,                c => throwError "Bad coordinate {c} for {e}"
+private def viewCoordRaw: Expr → Nat → M Expr
+  | e                     , 3 => throwError "Can't viewRaw the type of {e}"
+  | (Expr.app f _)        , 0 => pure f
+  | (Expr.app _ a)        , 1 => pure a
+  | (Expr.lam _ y _ _)    , 0 => pure y
+  | (Expr.lam _ _ b _)    , 1 => pure b
+  | (Expr.forallE _ y _ _), 0 => pure y
+  | (Expr.forallE _ _ b _), 1 => pure b
+  | (Expr.letE _ y _ _ _) , 0 => pure y
+  | (Expr.letE _ _ a _ _) , 1 => pure a
+  | (Expr.letE _ _ _ b _) , 2 => pure b
+  | (Expr.proj _ _ b)     , 0 => pure b
+  | (Expr.mdata _ a)      , n => viewCoordRaw a n
+  | e                     , c => throwError "Bad coordinate {c} for {e}"
+
 
 /-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
 If the given `SubExpr` has a type subexpression coordinate, then throw an error.
@@ -150,20 +148,21 @@ def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
 
 private def viewBindersCoord : Nat → Expr → Option (Name × Expr)
-  | 1, .lam n y _ _     => some (n, y)
-  | 1, .forallE n y _ _ => some (n, y)
-  | 2, .letE n y _ _ _  => some (n, y)
-  | _, _                => none
+  | 1, (Expr.lam n y _ _)     => some (n, y)
+  | 1, (Expr.forallE n y _ _) => some (n, y)
+  | 2, (Expr.letE n y _ _ _)  => some (n, y)
+  | _, _                      => none
 
 /-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
 def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
-  let (acc, _) ← p.foldlM (init := (#[], root)) fun (acc, e) c => do
+  let (acc, _) ← p.foldlM (fun (acc, e) c => do
     let e₂ ← viewCoordRaw e c
     let acc :=
       match viewBindersCoord c e with
       | none => acc
       | some b => acc.push b
     return (acc, e₂)
+  ) (#[], root)
   return acc
 
 /-- Returns the number of binders above a given subexpr position. -/

src/Lean/Meta/SynthInstance.lean

@@ -25,12 +25,6 @@ register_builtin_option synthInstance.maxSize : Nat := {
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
 
-register_builtin_option backward.synthInstance.canonInstances : Bool := {
-  defValue := true
-  group    := "backward compatibility"
-  descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
-}
-
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -555,17 +549,16 @@ def generate : SynthM Unit := do
     let mctx := gNode.mctx
     let mvar := gNode.mvar
     /- See comment at `typeHasMVars` -/
-    if backward.synthInstance.canonInstances.get (← getOptions) then
-      unless gNode.typeHasMVars do
-        if let some entry := (← get).tableEntries.find? key then
-          unless entry.answers.isEmpty do
-            /-
-            We already have an answer for this node, and since its type does not have metavariables,
-            we can skip other solutions because we assume instances are "morally canonical".
-            We have added this optimization to address issue #3996.
-            -/
-            modify fun s => { s with generatorStack := s.generatorStack.pop }
-            return
+    unless gNode.typeHasMVars do
+      if let some entry := (← get).tableEntries.find? key then
+        unless entry.answers.isEmpty do
+          /-
+          We already have an answer for this node, and since its type does not have metavariables,
+          we can skip other solutions because we assume instances are "morally canonical".
+          We have added this optimization to address issue #3996.
+          -/
+          modify fun s => { s with generatorStack := s.generatorStack.pop }
+          return
     discard do withMCtx mctx do
       withTraceNode `Meta.synthInstance
         (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
@@ -718,7 +711,6 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
-  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type

src/Lean/SubExpr.lean

@@ -54,24 +54,24 @@ def push (p : Pos) (c : Nat) : Pos :=
 variable {α : Type} [Inhabited α]
 
 /-- Fold over the position starting at the root and heading to the leaf-/
-partial def foldl  (f : α → Nat → α) (init : α) (p : Pos) : α :=
-  if p.isRoot then init else f (foldl f init p.tail) p.head
+partial def foldl  (f : α → Nat → α) (a : α) (p : Pos) : α :=
+  if p.isRoot then a else f (foldl f a p.tail) p.head
 
 /-- Fold over the position starting at the leaf and heading to the root-/
-partial def foldr  (f : Nat → α → α) (p : Pos) (init : α) : α :=
-  if p.isRoot then init else foldr f p.tail (f p.head init)
+partial def foldr  (f : Nat → α → α) (p : Pos) (a : α) : α :=
+  if p.isRoot then a else foldr f p.tail (f p.head a)
 
 /-- monad-fold over the position starting at the root and heading to the leaf -/
-partial def foldlM  [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α :=
+partial def foldlM  [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α :=
   have : Inhabited (M α) := inferInstance
-  if p.isRoot then pure init else do foldlM f init p.tail >>= (f · p.head)
+  if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
 
 /-- monad-fold over the position starting at the leaf and finishing at the root. -/
-partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α :=
-  if p.isRoot then pure init else f p.head init >>= foldrM f p.tail
+partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α :=
+  if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
 
 def depth (p : Pos) :=
-  p.foldr (init := 0) fun _ => Nat.succ
+  p.foldr (fun _ => Nat.succ) 0
 
 /-- Returns true if `pred` is true for each coordinate in `p`.-/
 def all (pred : Nat → Bool) (p : Pos) : Bool :=
@@ -134,8 +134,8 @@ protected def fromString? : String → Except String Pos
 
 protected def fromString! (s : String) : Pos :=
   match Pos.fromString? s with
-  | .ok a => a
-  | .error e => panic! e
+  | Except.ok a => a
+  | Except.error e => panic! e
 
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
@@ -213,7 +213,7 @@ open SubExpr in
 `SubExpr.Pos` argument for tracking subexpression position. -/
 def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr :=
   match e with
-  | .app f a =>
+  | Expr.app f a =>
     e.updateApp!
       <$> traverseAppWithPos visit p.pushAppFn f
       <*> visit p.pushAppArg a

src/kernel/declaration.cpp

@@ -205,10 +205,6 @@ declaration mk_definition(environment const & env, name const & n, names const &
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
 }
 
-declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
-}
-
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n))));
 }

src/kernel/declaration.h

@@ -223,12 +223,10 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
 inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
-bool use_unsafe(environment const & env, expr const & e);
 declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
                           reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
 declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
                           definition_safety safety = definition_safety::safe);
-declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val);
 declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
 declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);

src/library/constructions/projection.cpp

@@ -86,8 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
         expr result_type   = consume_type_annotations(binding_domain(cnstr_type));
-        bool is_prop       = type_checker(new_env, lctx).is_prop(result_type);
-        if (is_predicate && !is_prop) {
+        if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
                             << "type is an inductive predicate, but field is not a proposition");
         }
@@ -98,24 +97,13 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         proj_type      = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit);
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
-        declaration new_d;
-        if (is_prop) {
-            bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
-            if (unsafe) {
-                // theorems cannot be unsafe
-                new_d = mk_opaque(proj_name, lvl_params, proj_type, proj_val, unsafe);
-            } else {
-                new_d = mk_theorem(proj_name, lvl_params, proj_type, proj_val);
-            }
-        } else {
-            new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
+        declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
                                                            reducibility_hints::mk_abbreviation());
-        }
         new_env = new_env.add(new_d);
-        if (!inst_implicit && !is_prop)
+        if (!inst_implicit)
             new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);
         new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit);
-        expr proj    = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
+        expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
         cnstr_type   = instantiate(binding_body(cnstr_type), proj);
         i++;
     }

tests/lean/run/2575.lean

@@ -1,12 +0,0 @@
-structure AtLeastThirtySeven where
-  val : Nat
-  le : 37 ≤ val
-
-theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
-
-/--
-info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
-fun self => self.2
--/
-#guard_msgs in
-#print AtLeastThirtySeven.le

tests/lean/run/3965_3.lean

@@ -1,298 +0,0 @@
-section Mathlib.Init.Order.Defs
-
-universe u
-variable {α : Type u}
-
-class Preorder (α : Type u) extends LE α, LT α
-
-theorem le_trans [Preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c := sorry
-
-class PartialOrder (α : Type u) extends Preorder α where
-  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
-
-end Mathlib.Init.Order.Defs
-
-section Mathlib.Init.Set
-
-set_option autoImplicit true
-
-def Set (α : Type u) := α → Prop
-
-namespace Set
-
-protected def Mem (a : α) (s : Set α) : Prop :=
-  s a
-
-instance : Membership α (Set α) :=
-  ⟨Set.Mem⟩
-
-def image (f : α → β) (s : Set α) : Set β := fun b => ∃ a, ∃ (_ : a ∈ s), f a = b
-
-end Set
-
-end Mathlib.Init.Set
-
-section Mathlib.Data.Subtype
-
-attribute [coe] Subtype.val
-
-end Mathlib.Data.Subtype
-
-section Mathlib.Order.Notation
-
-class Sup (α : Type _) where
-  sup : α → α → α
-
-class Inf (α : Type _) where
-  inf : α → α → α
-
-@[inherit_doc]
-infixl:68 " ⊔ " => Sup.sup
-
-@[inherit_doc]
-infixl:69 " ⊓ " => Inf.inf
-
-class Top (α : Type _) where
-  top : α
-
-class Bot (α : Type _) where
-  bot : α
-
-notation "⊤" => Top.top
-
-notation "⊥" => Bot.bot
-
-end Mathlib.Order.Notation
-
-section Mathlib.Data.Set.Defs
-
-universe u
-
-namespace Set
-
-variable {α : Type u}
-
-@[coe, reducible] def Elem (s : Set α) : Type u := {x // x ∈ s}
-
-instance : CoeSort (Set α) (Type u) := ⟨Elem⟩
-
-end Set
-
-end Mathlib.Data.Set.Defs
-
-section Mathlib.Order.Basic
-
-universe u
-
-variable {α : Type u}
-
-def Preorder.lift {α β} [Preorder β] (f : α → β) : Preorder α where
-  le x y := f x ≤ f y
-  lt x y := f x < f y
-
-def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) : PartialOrder α :=
-  { Preorder.lift f with le_antisymm := sorry }
-
-namespace Subtype
-
-instance le [LE α] {p : α → Prop} : LE (Subtype p) :=
-  ⟨fun x y ↦ (x : α) ≤ y⟩
-
-instance lt [LT α] {p : α → Prop} : LT (Subtype p) :=
-  ⟨fun x y ↦ (x : α) < y⟩
-
-instance partialOrder [PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p) :=
-  PartialOrder.lift (fun (a : Subtype p) ↦ (a : α))
-
-end Subtype
-
-end Mathlib.Order.Basic
-
-section Mathlib.Order.Lattice
-
-universe u
-variable {α : Type u}
-
-class SemilatticeSup (α : Type u) extends Sup α, PartialOrder α where
-  protected le_sup_left : ∀ a b : α, a ≤ a ⊔ b
-  protected le_sup_right : ∀ a b : α, b ≤ a ⊔ b
-  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
-
-section SemilatticeSup
-
-variable [SemilatticeSup α] {a b c : α}
-
-theorem sup_le : a ≤ c → b ≤ c → a ⊔ b ≤ c := sorry
-
-end SemilatticeSup
-
-class SemilatticeInf (α : Type u) extends Inf α, PartialOrder α where
-  protected inf_le_left : ∀ a b : α, a ⊓ b ≤ a
-  protected inf_le_right : ∀ a b : α, a ⊓ b ≤ b
-  protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c
-
-section SemilatticeInf
-
-variable [SemilatticeInf α] {a b c d : α}
-
-theorem inf_le_left : a ⊓ b ≤ a := sorry
-
-theorem le_inf_iff : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c := sorry
-
-end SemilatticeInf
-
-class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α
-
-namespace Subtype
-
-protected def semilatticeSup [SemilatticeSup α] {P : α → Prop}
-    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) :
-    SemilatticeSup { x : α // P x } where
-  sup x y := ⟨x.1 ⊔ y.1, sorry⟩
-  le_sup_left _ _ := sorry
-  le_sup_right _ _ := sorry
-  sup_le _ _ _ h1 h2 := sorry
-
-protected def semilatticeInf [SemilatticeInf α] {P : α → Prop}
-    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
-    SemilatticeInf { x : α // P x } where
-  inf x y := ⟨x.1 ⊓ y.1, sorry⟩
-  inf_le_left _ _ := sorry
-  inf_le_right _ _ := sorry
-  le_inf _ _ _ h1 h2 := sorry
-
-end Subtype
-
-
-end Mathlib.Order.Lattice
-
-section Mathlib.Order.BoundedOrder
-
-universe u
-
-class OrderTop (α : Type u) [LE α] extends Top α where
-  le_top : ∀ a : α, a ≤ ⊤
-
-class OrderBot (α : Type u) [LE α] extends Bot α where
-  bot_le : ∀ a : α, ⊥ ≤ a
-
-end Mathlib.Order.BoundedOrder
-
-section Mathlib.Data.Set.Intervals.Basic
-
-variable {α : Type _} [Preorder α]
-
-def Set.Iic (b : α) : Set α := fun x => x ≤ b
-
-end Mathlib.Data.Set.Intervals.Basic
-
-section Mathlib.Order.SetNotation
-
-universe u
-variable {α : Type u}
-
-class SupSet (α : Type _) where
-  sSup : Set α → α
-
-class InfSet (α : Type _) where
-  sInf : Set α → α
-
-export SupSet (sSup)
-
-export InfSet (sInf)
-
-end Mathlib.Order.SetNotation
-
-section Mathlib.Order.CompleteLattice
-
-variable {α : Type _}
-
-class CompleteSemilatticeSup (α : Type _) extends PartialOrder α, SupSet α where
-  sSup_le : ∀ s a, (∀ b ∈ s, b ≤ a) → sSup s ≤ a
-
-section
-
-variable [CompleteSemilatticeSup α] {s t : Set α} {a b : α}
-
-theorem sSup_le : (∀ b ∈ s, b ≤ a) → sSup s ≤ a := sorry
-end
-
-class CompleteSemilatticeInf (α : Type _) extends PartialOrder α, InfSet α where
-  le_sInf : ∀ s a, (∀ b ∈ s, a ≤ b) → a ≤ sInf s
-
-section
-
-variable [CompleteSemilatticeInf α] {s t : Set α} {a b : α}
-
-theorem le_sInf : (∀ b ∈ s, a ≤ b) → a ≤ sInf s := sorry
-
-end
-
-class CompleteLattice (α : Type _) extends Lattice α, CompleteSemilatticeSup α,
-  CompleteSemilatticeInf α, Top α, Bot α where
-  protected le_top : ∀ x : α, x ≤ ⊤
-  protected bot_le : ∀ x : α, ⊥ ≤ x
-
-instance (priority := 100) CompleteLattice.toOrderTop [h : CompleteLattice α] : OrderTop α :=
-  { h with }
-instance (priority := 100) CompleteLattice.toOrderBot [h : CompleteLattice α] : OrderBot α :=
-  { h with }
-
-end Mathlib.Order.CompleteLattice
-
-section Mathlib.Order.LatticeIntervals
-
-variable {α : Type _}
-
-namespace Set
-
-namespace Iic
-
-instance semilatticeInf [SemilatticeInf α] {a : α} : SemilatticeInf (Iic a) :=
-  Subtype.semilatticeInf fun _ _ hx _ => le_trans inf_le_left hx
-
-instance semilatticeSup [SemilatticeSup α] {a : α} : SemilatticeSup (Iic a) :=
-  Subtype.semilatticeSup fun _ _ hx hy => sup_le hx hy
-
-instance [Lattice α] {a : α} : Lattice (Iic a) :=
-  { Iic.semilatticeInf, Iic.semilatticeSup with }
-
-instance orderTop [Preorder α] {a : α} : OrderTop (Iic a) := sorry
-
-instance orderBot [Preorder α] [OrderBot α] {a : α} : OrderBot (Iic a) := sorry
-
-end Iic
-
-end Set
-
-end Mathlib.Order.LatticeIntervals
-
-section Mathlib.Order.CompleteLatticeIntervals
-
-variable {α : Type _}
-
-namespace Set.Iic
-
-variable [CompleteLattice α] {a : α}
-
-def instCompleteLattice : CompleteLattice (Iic a) where
-  sSup S := ⟨sSup (Set.image (fun x : Iic a => (x : α)) S), sorry⟩
-  sInf S := ⟨a ⊓ sInf (Set.image (fun x : Iic a => (x : α)) S), sorry⟩
-  sSup_le S b hb := sSup_le <| fun c' ⟨c, hc, hc'⟩ ↦ hc' ▸ hb c hc
-  le_sInf S b hb := le_inf_iff.mpr
-    ⟨b.property, le_sInf fun d' ⟨d, hd, hd'⟩  ↦ hd' ▸ hb d hd⟩
-  le_top := sorry
-  bot_le := sorry
-
-example : CompleteLattice (Iic a) where
-  sSup S := ⟨sSup (Set.image (fun x : Iic a => (x : α)) S), sorry⟩
-  sInf S := ⟨a ⊓ sInf (Set.image (fun x : Iic a => (x : α)) S), sorry⟩
-  sSup_le S b hb := sSup_le (α := α) <| fun c' ⟨c, hc, hc'⟩ ↦ hc' ▸ hb c hc
-  le_sInf S b hb := (le_inf_iff (α := α)).mpr
-    ⟨b.property, le_sInf fun d' ⟨d, hd, hd'⟩  ↦ hd' ▸ hb d hd⟩
-  le_top := sorry
-  bot_le := sorry
-
-  end Set.Iic
-
-  end Mathlib.Order.CompleteLatticeIntervals