Merge pull request #66 from leanprover-community/bump/v4.9.0-rc2

Bump toolchain to leanprover/lean4:v4.9.0-rc2 and assorted features

ProofWidgets/Component/Basic.lean

@@ -88,3 +88,12 @@ def InteractiveMessage : Component InteractiveMessageProps where
   "
 
 end ProofWidgets
+
+/-- Construct a structured message from a ProofWidgets component.
+
+For the meaning of `alt`, see `MessageData.ofWidget`. -/
+def Lean.MessageData.ofComponent [Server.RpcEncodable Props]
+    (c : ProofWidgets.Component Props) (p : Props) (alt : String) : CoreM MessageData := do
+  let wi ← Widget.WidgetInstance.ofHash c.javascriptHash
+    (Server.RpcEncodable.rpcEncode p)
+  return .ofWidget wi alt

ProofWidgets/Component/HtmlDisplay.lean

@@ -83,3 +83,9 @@ def elabHtmlTac : Tactic | _ => pure ()
 
 end HtmlCommand
 end ProofWidgets
+
+/-- Construct a structured message from ProofWidgets HTML.
+
+For the meaning of `alt`, see `MessageData.ofWidget`. -/
+def Lean.MessageData.ofHtml (h : ProofWidgets.Html) (alt : String) : CoreM MessageData :=
+  MessageData.ofComponent ProofWidgets.HtmlDisplay ⟨h⟩ alt

ProofWidgets/Component/PenroseDiagram.lean

@@ -5,10 +5,13 @@ namespace ProofWidgets.Penrose
 open Lean Server
 
 structure DiagramProps where
-  embeds : Array (String × Html)
-  dsl    : String
-  sty    : String
-  sub    : String
+  embeds      : Array (String × Html)
+  dsl         : String
+  sty         : String
+  sub         : String
+  /-- Maximum number of optimization steps to take before showing the diagram.
+  Optimization may converge earlier, before taking this many steps. -/
+  maxOptSteps : Nat := 500
   deriving Inhabited, RpcEncodable
 
 /-- Displays the given diagram using [Penrose](https://penrose.cs.cmu.edu/).
@@ -38,7 +41,7 @@ the editor theme. -/
 def Diagram : Component DiagramProps where
   javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "penroseDisplay.js"
 
-/-! # `PenroseBuilderM` -/
+/-! # `DiagramBuilderM` -/
 
 structure DiagramState where
   /-- The Penrose substance program.
@@ -57,7 +60,7 @@ open scoped Jsx in
 /-- Assemble the diagram using the provided domain and style programs.
 
 `none` is returned iff nothing was added to the diagram. -/
-def buildDiagram (dsl sty : String) : DiagramBuilderM (Option Html) := do
+def buildDiagram (dsl sty : String) (maxOptSteps : Nat := 500) : DiagramBuilderM (Option Html) := do
   let st ← get
   if st.sub == "" && st.embeds.isEmpty then
     return none
@@ -66,12 +69,12 @@ def buildDiagram (dsl sty : String) : DiagramBuilderM (Option Html) := do
   for (n, (tp, h)) in st.embeds.toArray do
     sub := sub ++ s!"{tp} {n}\n"
     embedHtmls := embedHtmls.push (n, h)
+  -- Note: order matters here, embed variables are declared first.
   sub := sub ++ st.sub
   return <Diagram
     embeds={embedHtmls}
-    dsl={dsl}
-    sty={sty}
-    sub={sub} />
+    dsl={dsl} sty={sty} sub={sub}
+    maxOptSteps={maxOptSteps} />
 
 /-- Add an object `nm` of Penrose type `tp`,
 labelled by `h`, to the substance program. -/

ProofWidgets/Demos/Euclidean.lean

@@ -30,16 +30,24 @@ class IncidenceGeometry where
   between : Point → Point → Point → Prop -- implies colinearity
   onLine : Point → Line → Prop
   onCircle : Point → Circle → Prop
+  inCircle : Point → Circle → Prop
   centerCircle : Point → Circle → Prop
+  circlesInter : Circle → Circle → Prop
+
   ne_23_of_between : ∀ {a b c : Point}, between a b c → b ≠ c
   line_unique_of_pts : ∀ {a b : Point}, ∀ {L M : Line},
     a ≠ b → onLine a L → onLine b L → onLine a M → onLine b M → L = M
   onLine_2_of_between : ∀ {a b c : Point}, ∀ {L : Line},
     between a b c → onLine a L → onLine c L → onLine b L
   line_of_pts : ∀ a b, ∃ L, onLine a L ∧ onLine b L
   circle_of_ne : ∀ a b, a ≠ b → ∃ C, centerCircle a C ∧ onCircle b C
+  circlesInter_of_onCircle_inCircle :
+    ∀ {a b α β}, onCircle b α → onCircle a β → inCircle a α →
+    inCircle b β → circlesInter α β
+  pts_of_circlesInter : ∀ {α β}, circlesInter α β →
+    ∃ a b, a ≠ b ∧ onCircle a α ∧ onCircle a β ∧ onCircle b α ∧ onCircle b β
+  inCircle_of_centerCircle : ∀ {a α}, centerCircle a α → inCircle a α
 
-variable [i : IncidenceGeometry]
 open IncidenceGeometry
 
 /-! # Metaprogramming utilities to break down expressions -/
@@ -59,11 +67,21 @@ def isOnCirclePred? (e : Expr) : Option (Expr × Expr) := do
   let some (_, a, C) := e.app3? ``onCircle | none
   return (a, C)
 
+/-- If `e == inCircle a C` return `some (a, C)`, otherwise `none`. -/
+def isInCirclePred? (e : Expr) : Option (Expr × Expr) := do
+  let some (_, a, C) := e.app3? ``inCircle | none
+  return (a, C)
+
 /-- If `e == centerCircle a C` return `some (a, C)`, otherwise `none`. -/
 def isCenterCirclePred? (e : Expr) : Option (Expr × Expr) := do
   let some (_, a, C) := e.app3? ``centerCircle | none
   return (a, C)
 
+/-- If `e == circlesInter a C` return `some (a, C)`, otherwise `none`. -/
+def isCirclesInterPred? (e : Expr) : Option (Expr × Expr) := do
+  let some (_, a, C) := e.app3? ``circlesInter | none
+  return (a, C)
+
 def isPoint? (e : Expr) : Bool :=
   e.isAppOf ``Point
 
@@ -93,10 +111,18 @@ def addHypotheses (hyps : Array LocalDecl) : DiagramBuilderM Unit := do
       let sa ← addExpr "Point" a
       let sC ← addExpr "Circle" C
       addInstruction s!"OnCircle({sa}, {sC})"
+    if let some (a, C) := isInCirclePred? tp then
+      let sa ← addExpr "Point" a
+      let sC ← addExpr "Circle" C
+      addInstruction s!"InCircle({sa}, {sC})"
     if let some (a, C) := isCenterCirclePred? tp then
       let sa ← addExpr "Point" a
       let sC ← addExpr "Circle" C
       addInstruction s!"CenterCircle({sa}, {sC})"
+    if let some (C, D) := isCirclesInterPred? tp then
+      let sC ← addExpr "Circle" C
+      let sD ← addExpr "Circle" D
+      addInstruction s!"CirclesInter({sC}, {sD})"
 
 /-! # Implementation of the widget -/
 
@@ -154,12 +180,13 @@ def EuclideanDisplay : Component PanelWidgetProps :=
 
 /-! # Example usage -/
 
-example {a b c : Point} {L M : Line} {C D E: Circle} (Babc : between a b c)
-   (aL : onLine a L) (bM : onLine b M) (cL : onLine c L) (cM : onLine c M)
-   (aC : onCircle a C) (aD : onCircle a D) (bC : centerCircle b C) (cE : centerCircle c E) :
-   L = M := by
+variable [i : IncidenceGeometry]
+
+example {a b c : Point} {L M : Line} (Babc : between a b c)
+    (aL : onLine a L) (bM : onLine b M) (cL : onLine c L) (cM : onLine c M) :
+    L = M := by
   with_panel_widgets [EuclideanDisplay]
-      -- Place your cursor here.
+    -- Place your cursor here.
     have bc := ne_23_of_between Babc
     have bL := onLine_2_of_between Babc aL cL
     exact line_unique_of_pts bc bL cL bM cM
@@ -172,12 +199,15 @@ to the diagram.
 Lines are labelled with links to insert them into the proof script. -/
 def constructLines (hyps : Array LocalDecl) (meta : Server.DocumentMeta) (cursorPos : Lsp.Position)
     : DiagramBuilderM Unit := do
-  -- Identify all the points.
+  -- Identify objects and hypotheses from which constructions can be made.
   let mut points : Array LocalDecl := {}
+  let mut circleInters : Array (LocalDecl × LocalDecl × LocalDecl) := {}
   for h in hyps do
     let tp ← instantiateMVars h.type
     if isPoint? tp then
       points := points.push h
+    if let some (.fvar C, .fvar D) := isCirclesInterPred? tp then
+      circleInters := circleInters.push (h, ← C.getDecl, ← D.getDecl)
 
   -- Add a plausible construction, labelled with a link that makes the text edit.
   let addConstruction (nm tp ctr : String) : DiagramBuilderM Unit := do
@@ -207,15 +237,29 @@ def constructLines (hyps : Array LocalDecl) (meta : Server.DocumentMeta) (cursor
 
       -- Add two possible circles.
       let nm := s!"C{sp}{sq}"
-      addConstruction nm "Circle" s!"let ⟨{nm}, _, _⟩ := circle_of_ne {sp} {sq} sorry"
+      addConstruction nm "Circle" s!"let ⟨{nm}, _, _⟩ := circle_of_ne {sp} {sq} (by assumption)"
       addInstruction s!"CenterCircle({sp}, {nm})"
       addInstruction s!"OnCircle({sq}, {nm})"
 
       let nm := s!"C{sq}{sp}"
-      addConstruction nm "Circle" s!"let ⟨{nm}, _, _⟩ := circle_of_ne {sq} {sp} sorry"
+      addConstruction nm "Circle" s!"let ⟨{nm}, _, _⟩ := circle_of_ne {sq} {sp} (by assumption)"
       addInstruction s!"CenterCircle({sq}, {nm})"
       addInstruction s!"OnCircle({sp}, {nm})"
 
+  -- Construct every possible circle intersection.
+  for hi : i in [0:circleInters.size] do
+    let (h, C, D) := circleInters[i]
+    let sC ← addExpr "Circle" C.toExpr
+    let sD ← addExpr "Circle" D.toExpr
+    let nm := s!"{sC}{sD}"
+    let nm' := s!"{sD}{sC}"
+    addConstruction nm "Point" s!"let ⟨{nm}, {nm'}, _, _, _, _, _⟩ := pts_of_circlesInter {h.userName}"
+    addEmbed nm' "Point" <b>{.text nm'}</b>
+    addInstruction s!"OnCircle({nm'}, {sC})"
+    addInstruction s!"OnCircle({nm}, {sD})"
+    addInstruction s!"OnCircle({nm}, {sC})"
+    addInstruction s!"OnCircle({nm'}, {sD})"
+
 open scoped Jsx in
 @[server_rpc_method]
 def EuclideanConstructions.rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
@@ -247,7 +291,7 @@ def EuclideanConstructions.rpc (props : PanelWidgetProps) : RequestM (RequestTas
           DiagramBuilderM.run do
             addHypotheses allHyps
             constructLines selectedHyps doc.meta props.pos
-            match ← DiagramBuilderM.buildDiagram EuclideanDisplay.dsl EuclideanDisplay.sty with
+            match ← DiagramBuilderM.buildDiagram EuclideanDisplay.dsl EuclideanDisplay.sty 1500 with
             | some html => return html
             | none => return <span>No Euclidean goal.</span>)
 
@@ -263,10 +307,13 @@ def EuclideanConstructions : Component PanelWidgetProps :=
 
 axiom test_sorry {α} : α
 
-example {a b c d : Point} : ∃ L, onLine a L ∧ onLine b L := by
-  with_panel_widgets [EuclideanConstructions]
-    -- Place your cursor below.
-    -- Shift-click points in 'Tactic state' to select them.
-    let ⟨Cdb, _, _⟩ := circle_of_ne d b sorry
+show_panel_widgets [local EuclideanConstructions]
+
+-- Try constructing an equilateral triangle abc
+-- with line segment ab as the base.
+example {a b : Point} (hab : a ≠ b) :
+    ∃ L M c, onLine a L ∧ onLine b M ∧ onLine c M ∧ onLine c L := by
+  -- Place your cursor below.
+  -- Shift-click hypotheses in 'Tactic state' to select them.
 
-    exact test_sorry
+  exact test_sorry

lake-manifest.json

@@ -1,10 +1,10 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0-rc2