feat: products

WIP

Manual/BasicTypes.lean

@@ -15,6 +15,7 @@ import Manual.BasicTypes.Fin
 import Manual.BasicTypes.UInt
 import Manual.BasicTypes.Option
 import Manual.BasicTypes.Empty
+import Manual.BasicTypes.Products
 
 open Manual.FFIDocType
 
@@ -345,20 +346,7 @@ end ShortCircuit
 
 {include 0 Manual.BasicTypes.Option}
 
-# Tuples
-%%%
-tag := "tuples"
-%%%
-
-:::planned 171
-Describe {name}`Prod` and {name}`PProd`, their syntax and API
-:::
-
-{docstring Prod}
-
-{docstring PProd}
-
-{docstring MProd}
+{include 0 Manual.BasicTypes.Products}
 
 # Sum Types
 %%%
@@ -373,18 +361,6 @@ Describe {name}`Sum` and {name}`PSum`, their syntax and API
 
 {docstring PSum}
 
-# Dependent Pairs
-%%%
-tag := "sigma-types"
-%%%
-
-:::planned 176
-Describe {name}`Sigma` and {name}`PSigma`, their syntax and API. What is the relationship to {lean}`Subtype` and {lean}`Exists`?
-:::
-
-{docstring Sigma}
-
-{docstring PSigma}
 
 # Linked Lists
 %%%

Manual/BasicTypes/Products.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+
+import Manual.Meta
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+#doc (Manual) "Tuples" =>
+%%%
+tag := "tuples"
+%%%
+
+
+
+:::paragraph
+The Lean standard library includes a variety of tuple-like types.
+In practice, they differ in four ways:
+ * whether the first projection is a type or a proposition
+ * whether the second projection is a type or a proposition
+ * whether the second projection's type depends on the first projection's value
+ * whether the type as a whole is a proposition or type
+:::
+
+:::table (header := true)
+* + Type
+  + First Projection
+  + Second Projection
+  + Dependent?
+  + Universe
+* + {name}`Prod`
+  + {lean universes:="u"}`Type u`
+  + {lean universes:="v"}`Type v`
+  + ❌️
+  + {lean universes:="u v"}`Type (max u v)`
+* + {name}`And`
+  + {lean universes:="u v"}`Prop`
+  + {lean universes:="u v"}`Prop`
+  + ❌️
+  + {lean universes:="u v"}`Prop`
+* + {name}`Sigma`
+  + {lean universes:="u"}`Type u`
+  + {lean universes:="v"}`Type v`
+  + ✔
+  + {lean universes:="u v"}`Type (max u v)`
+* + {name}`Subtype`
+  + {lean universes:="u"}`Type u`
+  + {lean universes:="v"}`Prop`
+  + ✔
+  + {lean universes:="u v"}`Type u`
+* + {name}`Exists`
+  + {lean universes:="u"}`Type u`
+  + {lean universes:="v"}`Prop`
+  + ✔
+  + {lean universes:="u v"}`Prop`
+:::
+
+:::paragraph
+Some potential rows in this table do not exist in the library:
+
+ * There is no dependent pair where the first projection is a proposition, because {tech}[proof irrelevance] renders this meaningless.
+
+ * There is no non-dependent pair that combines a type with a proposition because the situation is rare in practice: grouping data with _unrelated_ proofs is uncommon.
+:::
+
+These differences lead to very different use cases.
+{name}`Prod` and its variants {name}`PProd` and {name}`MProd` simply group data together—they are products.
+Because its second projection is dependent, {name}`Sigma` has the character of a sum: for each element of the first projection's type, there may be a different type in the second projection.
+{name}`Subtype` selects the values of a type that satisfy a predicate.
+Even though it syntactically resembles a pair, in practice it is treated as an actual subset.
+{name}`And` is a logical connective, and {name}`Exists` is a quantifier.
+This chapter documents the tuple-like pairs, namely {name}`Prod` and {name}`Sigma`.
+
+# Ordered Pairs
+%%%
+tag := "pairs"
+%%%
+
+```lean (show:=false)
+section
+variable {α : Type u} {β : Type v} {γ : Type w} {x : α} {y : β} {z : γ}
+```
+
+The type {lean}`α × β`, which is a {tech}[notation] for {lean}`Prod α β`, contains ordered pairs in which the first item is an {lean}`α` and the second is a {lean}`β`.
+These pairs are written in parentheses, separated by commas.
+Larger tuples are represented as nested tuples, so {lean}`α × β × γ` is equivalent to {lean}`α × (β × γ)` and {lean}`(x, y, z)` is equivalent to {lean}`(x, (y, z))`.
+
+:::syntax term title:="Product Types"
+```grammar
+$_ × $_
+```
+The product {lean}`Prod α β` is written {lean}`α × β`.
+:::
+
+:::syntax term title:="Pairs"
+```grammar
+($_, $_)
+```
+:::
+
+{docstring Prod}
+
+```lean (show:=false)
+section
+variable {α : Sort u} {β : Sort v} {γ : Type w}
+```
+
+There are also the variants {lean}`α ×' β` (which is notation for {lean}`PProd α β`) and {lean}`MProd`, which differ with respect to {tech}[universe] levels: like {name}`PSum`, {name}`PProd` allows either {lean}`α` or {lean}`β` to be a proposition, while {lean}`MProd` requires that both be types at the _same_ universe level.
+Generally speaking, {name}`PProd` is primarily used in the implementation of proof automation and the elaborator, as it tends to give rise to universe level unification problems that can't be solved.
+{lean}`MProd`, on the other hand, can simplify universe level issues in certain advanced use cases.
+
+```lean (show:=false)
+end
+```
+
+:::syntax term title:="Product Types"
+```grammar
+$_ ×' $_
+```
+The product {lean}`PProd α β`, in which both types could be propositions, is written {lean}`α × β`.
+:::
+
+
+{docstring PProd}
+
+{docstring MProd}
+
+## API Reference
+%%%
+tag := "prod-api"
+%%%
+
+As a mere pair, the primary API for {lean}`Prod` is provided by pattern matching and by the first and second projections {name}`Prod.fst` and {name}`Prod.snd`.
+
+### Ordering
+
+{docstring Prod.lexLt}
+
+### Transformation
+
+{docstring Prod.map}
+
+{docstring Prod.swap}
+
+
+### Natural Number Ranges
+
+{docstring Prod.allI}
+
+{docstring Prod.anyI}
+
+{docstring Prod.foldI}
+
+
+
+# Dependent Pairs
+%%%
+tag := "sigma-types"
+%%%
+
+:::planned 176
+Describe {name}`Sigma` and {name}`PSigma`, their syntax and API.
+:::
+
+:::TODO
+ * Sigma and PSigma syntax
+ * Example of a "product-like" use of {name}`Sigma`
+:::
+
+{docstring Sigma}
+
+{docstring PSigma}
+
+
+:::example "Dependent Pairs as Sums"
+{name}`Sigma` can be used to implement sums of {lean}`Type`s.
+```lean
+def Sum' (α : Type) (β : Type) : Type :=
+  Σ (b : Bool), match b with | true => α | false => β
+```
+
+The injections pair a tag with a value of the indicated type.
+Annotating them with {attr}`match_pattern` allows them to be used in patterns as well as in ordinary terms.
+```lean
+variable {α β : Type}
+
+@[match_pattern]
+def Sum'.inl (x : α) : Sum' α β := ⟨true, x⟩
+
+@[match_pattern]
+def Sum'.inr (x : β) : Sum' α β := ⟨false, x⟩
+
+def Sum'.swap : Sum' α β → Sum' β α
+  | .inl x => .inr x
+  | .inr y => .inl y
+```
+:::

Manual/Meta/Lean.lean

@@ -77,9 +77,13 @@ def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [Mona
 structure LeanInlineConfig extends LeanBlockConfig where
   /-- The expected type of the term -/
   type : Option StrLit
+  /-- Universe variables allowed in the term -/
+  universes : Option StrLit
+
+
 
 def LeanInlineConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanInlineConfig :=
-  LeanInlineConfig.mk <$> LeanBlockConfig.parse <*> .named `type strLit true
+  LeanInlineConfig.mk <$> LeanBlockConfig.parse <*> .named `type strLit true <*> .named `universes strLit true
 where
   strLit : ValDesc m StrLit := {
     description := "string literal containing an expected type",
@@ -214,7 +218,7 @@ def leanTerm : CodeBlockExpander
         try
           Core.resetMessageLog
           let tree' ← runWithOpenDecls <| runWithVariables fun _vars => do
-            let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none
+            let e ←  Elab.Term.elabTerm (catchExPostpone := true) stx none
             Term.synthesizeSyntheticMVarsNoPostponing
             let _ ← Term.levelMVarToParam (← instantiateMVars e)
 
@@ -291,11 +295,19 @@ def leanInline : RoleExpander
       | throwErrorAt arg "Expected code literal with the example name"
     let altStr ← parserInputString term
 
+    let leveller :=
+      if let some us := config.universes then
+        let us :=
+          us.getString.splitOn " " |>.filterMap fun (s : String) =>
+            if s.isEmpty then none else some s.toName
+        Elab.Term.withLevelNames us
+      else id
+
     let expectedType ← config.type.mapM fun (s : StrLit) => do
       match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with
       | .error e => throwErrorAt term e
       | .ok stx => withEnableInfoTree false <| runWithOpenDecls <| runWithVariables fun _ => do
-        let t ← Elab.Term.elabType stx
+        let t ← leveller <| Elab.Term.elabType stx
         Term.synthesizeSyntheticMVarsNoPostponing
         let t ← instantiateMVars t
         if t.hasExprMVar || t.hasLevelMVar then
@@ -310,7 +322,7 @@ def leanInline : RoleExpander
         try
           Core.resetMessageLog
           let tree' ← runWithOpenDecls <| runWithVariables fun _ => do
-            let e ← Elab.Term.elabTerm (catchExPostpone := true) stx expectedType
+            let e ← leveller <| Elab.Term.elabTerm (catchExPostpone := true) stx expectedType
             Term.synthesizeSyntheticMVarsNoPostponing
             let _ ← Term.levelMVarToParam (← instantiateMVars e)
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f7423ce560d2b39bca9e67ca355aed2b2a6d39be",
+   "rev": "2996a15e182ca18d7d3a70b5a5fc77aa4bedc9ce",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",