From 5e1c22526baed55956efc851d6fa93f5ec9dfa78 Mon Sep 17 00:00:00 2001 From: Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Wed, 27 May 2026 21:45:00 -0400 Subject: [PATCH] chore: convert all comments to docstrings, fix lakefile linter config (#78) --- lean/ProofAtlas/Astrolabe/Nerve.lean | 37 +++++---- lean/ProofAtlas/Astrolabe/Net.lean | 107 +++++++++++++++------------ lean/lakefile.toml | 6 +- 3 files changed, 77 insertions(+), 73 deletions(-) diff --git a/lean/ProofAtlas/Astrolabe/Nerve.lean b/lean/ProofAtlas/Astrolabe/Nerve.lean index cc57ea3..2032d4e 100644 --- a/lean/ProofAtlas/Astrolabe/Nerve.lean +++ b/lean/ProofAtlas/Astrolabe/Nerve.lean @@ -3,6 +3,7 @@ Copyright (c) 2026 MathNetwork. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: MathNetwork -/ +import ProofAtlas.Util.Linter /-! # AstroNerve — a node in a content-addressable hypergraph @@ -11,9 +12,9 @@ Identity is computed from record + refs (Merkle property). Each reference carries an abstract role tag. -/ --- Two fields: refs (ordered references with roles) and record (content). --- Id, Role, Record are abstract types. identify computes id from --- record + refs — content-addressing by construction. +/-- A node in a content-addressable hypergraph. +`refs`: ordered references with role tags. `record`: content. +Identity computed from record + refs via `identify`. -/ structure AstroNerve {Id : Type} {Role : Type} {Record : Type} (identify : Record → Array (Role × Id) → Id) where refs : Array (Role × Id) @@ -25,43 +26,42 @@ namespace AstroNerve variable {Id : Type} {Role : Type} {Record : Type} {identify : Record → Array (Role × Id) → Id} --- Compute identity from record + refs. Not stored — always derived. +/-- Compute identity from record + refs. Not stored — always derived. -/ def id (n : AstroNerve identify) : Id := identify n.record n.refs --- Number of references this nerve has. +/-- Number of references this nerve has. -/ def width (n : AstroNerve identify) : Nat := n.refs.size --- True if the nerve has no references (an atom / leaf node). +/-- True if the nerve has no references (an atom / leaf node). -/ def isAtom (n : AstroNerve identify) : Bool := n.refs.isEmpty --- All referenced ids, in order, without roles. +/-- All referenced ids, in order, without roles. -/ def refIds (n : AstroNerve identify) : Array Id := n.refs.map (·.2) --- All roles, in order, without ids. +/-- All roles, in order, without ids. -/ def refRoles (n : AstroNerve identify) : Array Role := n.refs.map (·.1) --- Does this nerve reference a given id? +/-- Does this nerve reference a given id? -/ def containsRef [BEq Id] (n : AstroNerve identify) (i : Id) : Bool := n.refs.any (fun ref => ref.2 == i) --- Get the i-th ref (returns Option to handle out-of-bounds). +/-- Get the i-th ref. Returns `none` if out of bounds. -/ def refAt (n : AstroNerve identify) (i : Nat) : Option (Role × Id) := n.refs[i]? --- Add a ref at the end. Returns a new nerve (new id, Merkle property). +/-- Add a ref at the end. Returns a new nerve with a new id. -/ def pushRef (n : AstroNerve identify) (ref : Role × Id) : AstroNerve identify := { refs := n.refs.push ref, record := n.record } --- Remove the last ref. Returns a new nerve (new id). +/-- Remove the last ref. Returns a new nerve with a new id. -/ def popRef (n : AstroNerve identify) : AstroNerve identify := { refs := n.refs.pop, record := n.record } --- Keep only refs matching a predicate. Returns a new nerve (new id). +/-- Keep only refs matching a predicate. Returns a new nerve. -/ def filterRefs (n : AstroNerve identify) (p : (Role × Id) → Bool) : AstroNerve identify := { refs := n.refs.filter p, record := n.record } --- Swap two refs by index. Returns a new nerve (new id). --- Panics if indices out of bounds. +/-- Swap two refs by index. Returns a new nerve with a new id. -/ def swapRefs [Inhabited Role] [Inhabited Id] (n : AstroNerve identify) (i j : Nat) : AstroNerve identify := let a := n.refs @@ -70,18 +70,17 @@ def swapRefs [Inhabited Role] [Inhabited Id] let a := a.set! j tmp { refs := a, record := n.record } --- Reverse the order of all refs. Returns a new nerve (new id). +/-- Reverse the order of all refs. Returns a new nerve. -/ def reverseRefs (n : AstroNerve identify) : AstroNerve identify := { refs := n.refs.reverse, record := n.record } --- Replace ref at position i. Returns a new nerve (new id). --- Panics if index out of bounds. +/-- Replace ref at position i. Returns a new nerve with a new id. -/ def setRef (n : AstroNerve identify) (i : Nat) (ref : Role × Id) : AstroNerve identify := { refs := n.refs.set! i ref, record := n.record } end AstroNerve --- ToString: show nerve as "Nerve(id=..., width=N)". +/-- Show nerve as `Nerve(id=..., width=N)`. -/ instance {Id Role Record : Type} {identify : Record → Array (Role × Id) → Id} [ToString Id] : ToString (AstroNerve identify) where toString n := s!"Nerve(id={n.id}, width={n.width})" diff --git a/lean/ProofAtlas/Astrolabe/Net.lean b/lean/ProofAtlas/Astrolabe/Net.lean index c3a6470..a3995ba 100644 --- a/lean/ProofAtlas/Astrolabe/Net.lean +++ b/lean/ProofAtlas/Astrolabe/Net.lean @@ -12,7 +12,7 @@ Built incrementally via `empty` and `addNerve!`. Injectivity and closure checked at compile time. -/ --- A net is an array of nerves sharing the same identify function. +/-- A net is an array of nerves sharing the same identify function. -/ structure AstroNet {Id : Type} [DecidableEq Id] {Role : Type} {Record : Type} (identify : Record → Array (Role × Id) → Id) where @@ -24,129 +24,132 @@ variable {Id : Type} [DecidableEq Id] {Role : Type} [DecidableEq Role] {Record : Type} [DecidableEq Record] {identify : Record → Array (Role × Id) → Id} --- Create an empty net. +/-- Create an empty net. -/ def empty (identify : Record → Array (Role × Id) → Id) : AstroNet identify where nerves := #[] --- Number of nerves in the net. +/-- Number of nerves in the net. -/ def size (net : AstroNet identify) : Nat := net.nerves.size --- Check if any nerve in the net has this id. +/-- Check if any nerve in the net has this id. -/ def hasId (net : AstroNet identify) (i : Id) : Bool := net.nerves.any (fun n => n.id == i) --- Find the nerve with this id. Returns none if not found. +/-- Find the nerve with this id. Returns none if not found. -/ def findById (net : AstroNet identify) (i : Id) : Option (AstroNerve identify) := net.nerves.find? (fun n => n.id == i) --- Get the record of the nerve with this id. Returns none if not found. +/-- Get the record of the nerve with this id. Returns none if not found. -/ def getRecord (net : AstroNet identify) (i : Id) : Option Record := (net.findById i).map (·.record) --- Check if a nerve can be safely added: --- all refs must exist in the net (closure), and id must be fresh (injectivity). +/-- Check if a nerve can be safely added: +all refs must exist in the net (closure), and id must be fresh (injectivity). -/ def canAdd (net : AstroNet identify) (n : AstroNerve identify) : Bool := n.refs.all (fun ref => net.hasId ref.2) && !net.hasId n.id --- Add a nerve. Closure + injectivity checked at compile time. --- If the check fails, the file won't compile. +/-- Add a nerve. Closure + injectivity checked at compile time. +If the check fails, the file won't compile. -/ def addNerve! (net : AstroNet identify) (n : AstroNerve identify) (_h : net.canAdd n = true := by native_decide) : AstroNet identify where nerves := net.nerves.push n --- All ids in the net, in insertion order. +/-- All ids in the net, in insertion order. -/ def ids (net : AstroNet identify) : Array Id := net.nerves.map (·.id) --- All atoms (nerves with no refs). +/-- All atoms (nerves with no refs). -/ def atoms (net : AstroNet identify) : Array (AstroNerve identify) := net.nerves.filter (·.isAtom) --- All non-atoms (nerves with refs). +/-- All non-atoms (nerves with refs). -/ def edges (net : AstroNet identify) : Array (AstroNerve identify) := net.nerves.filter (!·.isAtom) --- All nerves that reference a given id (reverse lookup). +/-- All nerves that reference a given id (reverse lookup). -/ def refsTo (net : AstroNet identify) (i : Id) : Array (AstroNerve identify) := net.nerves.filter (·.containsRef i) --- Does the net contain a nerve with this id? +/-- Does the net contain a nerve with this id? -/ def contains (net : AstroNet identify) (n : AstroNerve identify) : Bool := net.hasId n.id --- Is the net empty? +/-- Is the net empty? -/ def isEmpty (net : AstroNet identify) : Bool := net.nerves.isEmpty --- Number of atoms. +/-- Number of atoms. -/ def atomCount (net : AstroNet identify) : Nat := net.atoms.size --- Number of non-atoms (edges). +/-- Number of non-atoms (edges). -/ def edgeCount (net : AstroNet identify) : Nat := net.edges.size --- Convert to List. +/-- Convert to List. -/ def toList (net : AstroNet identify) : List (AstroNerve identify) := net.nerves.toList --- Map a function over all nerves' records, producing a list of results. +/-- Map a function over all nerves' records, producing a list of results. -/ def mapRecords (net : AstroNet identify) (f : Record → α) : Array α := net.nerves.map (fun n => f n.record) --- Filter nerves by a predicate. Returns a plain array (not a net, --- since filtered result may violate closure). +/-- Filter nerves by a predicate. Returns a plain array (not a net, +since filtered result may violate closure). -/ def filterNerves (net : AstroNet identify) (p : AstroNerve identify → Bool) : Array (AstroNerve identify) := net.nerves.filter p --- Remove a nerve by id. Returns a plain array (not a net, --- since removing a nerve may break closure for nerves that referenced it). +/-- Remove a nerve by id. Returns a plain array (not a net, +since removing a nerve may break closure for nerves that referenced it). -/ def removeById (net : AstroNet identify) (i : Id) : Array (AstroNerve identify) := net.nerves.filter (fun n => n.id != i) --- Merge two nets. Returns a plain array (not a net, --- since duplicates / broken closure must be resolved by the caller). +/-- Merge two nets. Returns a plain array (not a net, +since duplicates / broken closure must be resolved by the caller). -/ def mergeNerves (net1 net2 : AstroNet identify) : Array (AstroNerve identify) := net1.nerves ++ net2.nerves --- Is every nerve in net1 also in net2 (by id)? +/-- Is every nerve in net1 also in net2 (by id)? -/ def isSubnetOf (net1 net2 : AstroNet identify) : Bool := net1.nerves.all (fun n => net2.hasId n.id) --- Get the i-th nerve by insertion order. +/-- Get the i-th nerve by insertion order. -/ def nerveAt (net : AstroNet identify) (i : Nat) : Option (AstroNerve identify) := net.nerves[i]? --- Total number of refs across all nerves. +/-- Total number of refs across all nerves. -/ def totalRefs (net : AstroNet identify) : Nat := net.nerves.foldl (fun acc n => acc + n.width) 0 --- How many times is this id referenced across all nerves (in-degree). +/-- How many times is this id referenced across all nerves (in-degree). -/ def degree (net : AstroNet identify) (i : Id) : Nat := net.nerves.foldl (fun acc n => acc + n.refs.foldl (fun c ref => if ref.2 == i then c + 1 else c) 0) 0 --- Nerves that no other nerve references (root nodes). +/-- Nerves that no other nerve references (root nodes). -/ def orphans (net : AstroNet identify) : Array (AstroNerve identify) := net.nerves.filter (fun n => net.degree n.id == 0) --- Fold over all nerves from left. +/-- Fold over all nerves from left. -/ def foldl (net : AstroNet identify) (f : α → AstroNerve identify → α) (init : α) : α := net.nerves.foldl f init --- Map a function over all nerves. +/-- Map a function over all nerves. -/ def map (net : AstroNet identify) (f : AstroNerve identify → α) : Array α := net.nerves.map f --- Result of depth computation: finite depth, cycle, or not found. +/-- Result of depth computation: finite depth, cycle, or not found. -/ inductive DepthResult where - | depth (n : Nat) -- finite depth - | cycle -- participates in a cycle (infinite depth) - | notFound -- id not in the net + /-- Finite depth. -/ + | depth (n : Nat) + /-- Participates in a cycle (infinite depth). -/ + | cycle + /-- Id not in the net. -/ + | notFound deriving Repr, BEq, Inhabited --- Compute depth of a nerve in the net. --- atom = .depth 0, others = .depth (1 + max of refs), cycle = .cycle +/-- Compute depth of a nerve in the net. +atom = `.depth 0`, others = `.depth (1 + max of refs)`, cycle = `.cycle`. -/ partial def depthOf (net : AstroNet identify) (i : Id) : DepthResult := go i #[] where @@ -167,38 +170,41 @@ where match d with | .depth n => max acc n | _ => acc) 0 .depth (maxD + 1) --- Is the net acyclic? (all nerves have finite depth) +/-- Is the net acyclic? (all nerves have finite depth) -/ def isAcyclic (net : AstroNet identify) : Bool := net.nerves.all (fun n => match net.depthOf n.id with | .depth _ => true | _ => false) --- Maximum depth in the net (none if any nerve has a cycle). +/-- Maximum depth in the net (none if any nerve has a cycle). -/ def maxDepth (net : AstroNet identify) : Option Nat := let depths := net.nerves.map (fun n => net.depthOf n.id) if depths.any (· == .cycle) then none else some (depths.foldl (fun acc d => match d with | .depth n => max acc n | _ => acc) 0) --- Build a net directly from an array, without checking axioms. --- Use this for testing or when you guarantee correctness externally. +/-- Build a net directly from an array, without checking axioms. +Use this for testing or when you guarantee correctness externally. -/ def ofArray (nerves : Array (AstroNerve identify)) : AstroNet identify where nerves := nerves --- Count the number of nerves involved in cycles. +/-- Count the number of nerves involved in cycles. -/ def cycleCount (net : AstroNet identify) : Nat := net.nerves.filter (fun n => net.depthOf n.id == .cycle) |>.size --- All nerves that are part of a cycle. +/-- All nerves that are part of a cycle. -/ def cyclicNerves (net : AstroNet identify) : Array (AstroNerve identify) := net.nerves.filter (fun n => net.depthOf n.id == .cycle) --- Depth of every nerve: list of (id, depth result) pairs. +/-- Depth of every nerve: list of (id, depth result) pairs. -/ def depthMap (net : AstroNet identify) [ToString Id] : Array (String × DepthResult) := net.nerves.map (fun n => (toString n.id, net.depthOf n.id)) end AstroNet --- SCC support: outside namespace to avoid implicit parameter issues. +/-! ## SCC support +Outside namespace to avoid implicit parameter issues. -/ + +/-- Can we reach `to_` from `from_` following refs? -/ partial def _root_.AstroNet.canReach {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} (net : AstroNet f) (from_ to_ : α) : Bool := @@ -213,6 +219,7 @@ where | some n => (n.refs.map Prod.snd).any (fun rid => go rid (visited.push cur)) +/-- Compute strongly connected components of the net. -/ def _root_.AstroNet.sccs {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} (net : AstroNet f) : Array (Array α) := Id.run do @@ -231,24 +238,26 @@ def _root_.AstroNet.sccs {α β γ : Type} [DecidableEq α] components := components.push comp return components +/-- Number of non-trivial SCCs (size > 1, i.e. actual cycles). -/ def _root_.AstroNet.sccCount {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} (net : AstroNet f) : Nat := (net.sccs.filter (·.size > 1)).size +/-- All non-trivial SCCs (cycles) as arrays of ids. -/ def _root_.AstroNet.printCycles {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} (net : AstroNet f) : Array (Array α) := net.sccs.filter (·.size > 1) --- BEq: two nets are equal if they have the same nerves. +/-- Two nets are equal if they have the same nerves. -/ instance {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} [BEq (AstroNerve f)] : BEq (AstroNet f) where beq a b := a.nerves == b.nerves --- ToString: show net as "AstroNet(n nerves)". +/-- Show net as `AstroNet(n nerves)`. -/ instance {α β γ : Type} [DecidableEq α] {f : γ → Array (β × α) → α} : ToString (AstroNet f) where diff --git a/lean/lakefile.toml b/lean/lakefile.toml index d02f2a2..2205efb 100644 --- a/lean/lakefile.toml +++ b/lean/lakefile.toml @@ -6,16 +6,12 @@ name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" rev = "b2958bc1a0e2db353d06d6c019cd3f8bb8a1163c" -[[lean_lib]] -name = "ProofAtlasUtil" -roots = ["ProofAtlas.Util.Linter.MathTag"] - [[lean_lib]] name = "ProofAtlas" roots = ["ProofAtlas"] leanOptions = [ { name = "weak.linter.mathlibStandardSet", value = true }, - { name = "weak.linter.proofAtlasMathTag", value = true }, + { name = "weak.linter.proofAtlasDocstringRequired", value = true }, ] [[lean_lib]]