more pretty printers, drawn from https://github.com/ldct/LeanGT/blob/main/LeanGT/Texify.lean

Author: kmill

LeanTeXMathlib/Basic.lean

@@ -31,6 +31,10 @@ latex_pp_app_rules (const := Set.image)
     return ← f.protectRight funAppBP ++ X.brackets |>.mergeBP (lbp := .NonAssoc funAppBP) (rbp := .NonAssoc funAppBP)
       |>.maybeWithTooltip s!"image of \\({X.latex.1}\\) under \\({f.latex.1}\\)"
 
+-- Use the type itself as the universe
+latex_pp_app_rules (const := Finset.univ)
+  | _, #[ty, _] => latexPP ty
+
 latex_pp_app_rules (const := Finset.prod)
 | _, #[_α, _β, _inst, s, f] => do
   let set ← withExtraSmallness 2 <| latexPP s
@@ -49,7 +53,80 @@ latex_pp_app_rules (const := Finset.sum)
       let psum := (← (LatexData.atomString "\\sum" |>.bigger 1).sub (s!"{name.toLatex} \\in " ++ set) |>.maybeWithTooltip "Finset.sum") ++ pbody
       return psum |>.resetBP (lbp := .Infinity) |>.mergeBP (rbp := .NonAssoc 65)
 
+-- Suppress casts
+latex_pp_app_rules (const := Nat.cast)
+  | _, #[_, _, n] => latexPP n
+latex_pp_app_rules (const := Int.cast)
+  | _, #[_, _, n] => latexPP n
+
 latex_pp_const_rule Rat := (LatexData.atomString "\\mathbb{Q}").maybeWithTooltip "Rat"
 
 latex_pp_const_rule Real := (LatexData.atomString "\\mathbb{R}").maybeWithTooltip "Real"
 latex_pp_const_rule Real.pi := LatexData.atomString "\\pi" |>.maybeWithTooltip "real.pi"
+
+latex_pp_app_rules (const := Real.sqrt)
+  | _, #[x] => do
+    let v ← latexPP x
+    let (latex, bigness) := v.latex
+    -- Note: using an atom, but subscripts are incompatible with the square root symbol.
+    -- Assuming subscripts will never happen.
+    return .Atom ("\\sqrt{" ++ latex ++ "}") bigness none none
+
+macro "latex_pp_trig_rule" c:ident tex:str : command =>
+  `(
+  latex_pp_app_rules (const := $c)
+    | _, #[x] => do
+      let v ← latexPP x
+      return LatexData.atomString $tex ++ " " ++ v.protect (funAppBP - 1)
+        |>.mergeBP (lbp := .NonAssoc funAppBP) (rbp := .NonAssoc funAppBP)
+  )
+
+latex_pp_trig_rule Real.sin "\\sin"
+latex_pp_trig_rule Real.cos "\\cos"
+latex_pp_trig_rule Real.tan "\\tan"
+latex_pp_trig_rule Real.arcsin "\\sin^{-1}"
+latex_pp_trig_rule Real.arccos "\\cos^{-1}"
+latex_pp_trig_rule Real.arctan "\\tan^{-1}"
+
+latex_pp_app_rules (const := Finset.Icc)
+  | _, #[_, _, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "[" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Ico)
+  | _, #[_, _, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "[" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Ioc)
+  | _, #[_, _, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "(" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Ioo)
+  | _, #[_, _, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "(" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Iic)
+  | _, #[_, _, _, hi] => do
+    let hi ← latexPP hi
+    -- using infty is not technically correct. for example, ℕ would be starting from 0
+    return "(-\\infty, " ++ hi ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Iio)
+  | _, #[_, _, _, hi] => do
+    let hi ← latexPP hi
+    return "(-\\infty, " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Ici)
+  | _, #[_, _, _, lo] => do
+    let lo ← latexPP lo
+    return "[" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Finset.Ioi)
+  | _, #[_, _, _, lo] => do
+    let lo ← latexPP lo
+    return "(" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity
+
+latex_pp_app_rules (const := Finset.range)
+  | _, #[hi] => do
+    let hi ← latexPP hi
+    return "[0, " ++ hi ++ ")" |>.resetBP .Infinity .Infinity

test/basic.lean

@@ -11,6 +11,7 @@ def f : Nat → Nat → Nat := λ x y => x + y
 
 def g : Unit → Nat := λ _ => 22
 
+section
 variable (b : Nat) (s : Finset Nat) (t : Nat → Finset Nat) (c : Nat → Real → Real) (x : Real)
 
 /-- info: \sum_{x \in s}(x + 1) -/
@@ -56,3 +57,26 @@ latex_pp_app_rules (kind := any) (paramKinds := params)
 #texify s.sum (λ x => x + 1) * s.sum (λ x => 2 * x)
 #texify λ (c : Nat) => c * s.sum (λ x => (t x).sum (λ y => x * y))
 #texify s.sum id
+
+#texify Real.arcsin (Real.cos 2)
+
+end
+
+-- https://github.com/ldct/LeanGT/blob/main/LeanGT/TexifyDemo.lean
+
+example (a b c : ℝ)
+    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : a*b*c = 1) :
+    3 ≤ Real.sqrt ((a + b) / (a + 1)) + Real.sqrt ((b + c) / (b + 1)) + Real.sqrt ((c + a) / (c + 1)) := by
+  texify
+  sorry
+
+example (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2 := by
+  texify
+  sorry
+
+theorem imo1966_p4 (n : ℕ) (x : ℝ)
+    (hx : ∀ t : ℕ, ∀ k : ℤ, x ≠ k * Real.pi / 2^t) :
+    ∑ i ∈ Finset.range n, 1 / Real.sin (2^(i + 1) * x) =
+    1 / Real.tan x - 1 / Real.tan (2^n * x) := by
+  texify
+  sorry