From d0bd317dbdafa8308e68446d3d2557fde465c448 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Sat, 15 Aug 2026 12:18:06 -0500 Subject: [PATCH 1/4] feat: Add API of basic constructions --- Cslib.lean | 1 + Cslib/Foundations/Data/PFunctor/Basic.lean | 148 +++++++++++++++++++++ CslibTests.lean | 1 + CslibTests/PFunctor.lean | 88 ++++++++++++ 4 files changed, 238 insertions(+) create mode 100644 Cslib/Foundations/Data/PFunctor/Basic.lean create mode 100644 CslibTests/PFunctor.lean diff --git a/Cslib.lean b/Cslib.lean index 24bcae5c1..3ddd94c0d 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -77,6 +77,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OmegaSequence.Init public import Cslib.Foundations.Data.OmegaSequence.Temporal +public import Cslib.Foundations.Data.PFunctor.Basic public import Cslib.Foundations.Data.PFunctor.Free public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Set.Saturation diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean new file mode 100644 index 000000000..235e0316a --- /dev/null +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Quang Dao +-/ +module + +public import Cslib.Init +public import Mathlib.Data.PFunctor.Univariate.Basic + +/-! +# Polynomial Functors + +This file defines additional constructions on `PFunctor` that don't belong in core mathlib. +The main definition is `monomial A B` for the `PFunctor` with constant family `B` over `A`, +with special cases `const`, `linear`, `selfMonomial`, `purePower`, the indeterminate `X`, +and canonical choices of `0` and `1`. + +We also define the sum `P + Q`, whose shapes are a sum of the shapes of `P` and `Q`, +with a type family defined by sum elimination into the individual child types, +and the product `P * Q`, whose shapes are pairs of shapes, +with a type family defined by sums of the individual child types. +-/ + +@[expose] public section + +universe uA uB uA₁ uA₂ uB₁ uB₂ + +namespace PFunctor + +/-- Two polynomial functors are equal if their head types are equal and their child types +agree over that equality. -/ +@[ext (iff := false)] +theorem ext {P Q : PFunctor.{uA, uB}} (h : P.A = Q.A) (h' : ∀ a, P.B a = Q.B (h ▸ a)) : + P = Q := by + cases P; cases Q; simp only [mk.injEq] at h h' ⊢; subst h + simp_all only [heq_eq_eq, true_and]; funext; exact h' _ + +section monomial + +/-- The monomial `PFunctor` with head type `A` and constant `B` for any `a : A`. -/ +abbrev monomial (A : Type uA) (B : Type uB) : PFunctor := ⟨A, fun _ => B⟩ + +lemma monomial_A (A : Type uA) (B : Type uB) : (monomial A B).A = A := rfl + +lemma monomial_B (A : Type uA) (B : Type uB) (a : (monomial A B).A) : + (monomial A B).B a = B := rfl + +end monomial + +section zero + +/-- The zero polynomial functor, defined as `A = PEmpty` and `B _ = PEmpty`, is the identity with + respect to sum (up to equivalence) -/ +@[simps] instance instZeroPFunctor : Zero PFunctor where zero := monomial PEmpty PEmpty + +instance : IsEmpty (0 : PFunctor.{uA, uB}).A := inferInstanceAs (IsEmpty PEmpty) + +end zero + +section one + +/-- The unit polynomial functor, defined as `A = PUnit` and `B _ = PEmpty`, is the identity with + respect to product (up to equivalence) -/ +@[simps] instance instOnePFunctor : One PFunctor where one := monomial PUnit PEmpty + +instance : Unique (1 : PFunctor.{uA, uB}).A := inferInstanceAs (Unique PUnit) + +instance (a : (1 : PFunctor.{uA, uB}).A) : IsEmpty ((1 : PFunctor.{uA, uB}).B a) := + inferInstanceAs (IsEmpty PEmpty) + +end one + +/-- The constant polynomial functor `P(X) = A X^ PEmpty = A` -/ +abbrev const (A : Type uA) : PFunctor := monomial A PEmpty + +/-- The linear polynomial functor `P(X) = A X` -/ +abbrev linear (A : Type uA) : PFunctor := monomial A PUnit + +/-- The self monomial polynomial functor `P(X) = S X^ S` -/ +abbrev selfMonomial (S : Type uA) : PFunctor.{uA, uA} := monomial S S + +/-- The pure power polynomial functor `P(X) = X^ B` -/ +abbrev purePower (B : Type uB) : PFunctor := monomial PUnit B + +/-- The indeterminate polynomial functor `P(X) = X`, the identity with respect to +composition and tensor product (up to equivalence). -/ +abbrev X : PFunctor := monomial PUnit PUnit + +/- Note: no explicit `IsEmpty`/`Unique` instances are needed for the positions and directions +of the abbreviations above: being reducible, they unfold to `PEmpty`/`PUnit` during instance +search. Only `0` and `1` need the explicit instances above, since the `Zero`/`One` instance +projections are not reducible. -/ + +@[simp] lemma const_pempty : const PEmpty = 0 := rfl + +@[simp] lemma const_punit : const PUnit = 1 := rfl + +@[simp] lemma linear_punit : linear PUnit = X := rfl + +@[simp] lemma selfMonomial_punit : selfMonomial PUnit = X := rfl + +@[simp] lemma purePower_punit : purePower PUnit = X := rfl + +section add + +/-- The sum of two polynomial functors `P` and `Q`, written as `P + Q`, +defined as the sum of the head types and the sum case analysis for the child types. + +This is kept as a `def` alongside the `HAdd` instance below, even though that instance is +exactly as universe-general as `add` itself: the `binop%` elaborator behind `+` eagerly +unifies the types of both operands with the expected type, so when the expected type carries +universe metavariables (e.g. inside `PFunctor.W (P.add (.const α))` with `α : Type v`), +`P + Q` can fail to elaborate where `P.add Q` succeeds; see `CslibTests/PFunctor.lean`. -/ +@[simps] def add (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : + PFunctor.{max uA₁ uA₂, uB} := ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩ + +/-- Addition of polynomial functors, defined as the sum construction. -/ +instance instHAddPFunctor : + HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where + hAdd := add + +@[simp] lemma add_def (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : + P + Q = P.add Q := rfl + +end add + +section prod + +/-- The product of two polynomial functors `P` and `Q`, written as `P * Q`, +defined as the product of the head types and the sum of the child types. +Unlike `add`, the child types of `P` and `Q` may live in different universes, +since they are combined with `⊕` rather than `Sum.elim`. -/ +@[simps] def prod (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : + PFunctor.{max uA₁ uA₂, max uB₁ uB₂} := ⟨P.A × Q.A, fun ab => P.B ab.1 ⊕ Q.B ab.2⟩ + +/-- Multiplication of polynomial functors, defined as the product construction. +As with addition, we deliberately do not add a homogeneous `Mul` instance. -/ +instance instHMulPFunctor : + HMul PFunctor.{uA₁, uB₁} PFunctor.{uA₂, uB₂} PFunctor.{max uA₁ uA₂, max uB₁ uB₂} where + hMul := prod + +@[simp] lemma mul_def (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : + P * Q = P.prod Q := rfl + +end prod + +end PFunctor diff --git a/CslibTests.lean b/CslibTests.lean index 99f1d31f5..51bcb8b7e 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -15,5 +15,6 @@ import CslibTests.LTS import CslibTests.LambdaCalculus import CslibTests.MLL import CslibTests.Modal +import CslibTests.PFunctor import CslibTests.Reduction import CslibTests.StatefulProcesses diff --git a/CslibTests/PFunctor.lean b/CslibTests/PFunctor.lean new file mode 100644 index 000000000..f77508a9f --- /dev/null +++ b/CslibTests/PFunctor.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Devon Tuma. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +import Cslib.Foundations.Data.PFunctor.Basic + +/-! +# Polynomial Functor Tests + +These tests exercise the universe-polymorphic polynomial sum and product, the simp API for +the basic constructions, and the extensionality lemma. +-/ + +universe uA uB uA₁ uA₂ uB₁ uB₂ v + +namespace CslibTests + +open PFunctor + +/-- Addition notation is available when its result universe is fixed by the expected type. -/ +example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : + PFunctor.{max uA₁ uA₂, uB} := P + Q + +/-- Multiplication notation is likewise available, including for child types in +different universes. -/ +example (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : + PFunctor.{max uA₁ uA₂, max uB₁ uB₂} := P * Q + +/-- The `def` spelling `P.add (.const α)` elaborates under `PFunctor.W` even when the +expected type only determines the universe levels up to a `max`. This is the motivating +use case for keeping `PFunctor.add` as a `def` alongside the `HAdd` instance. -/ +example (P : PFunctor.{uA₁, uB}) (α : Type v) : Type (max uA₁ uB v) := + PFunctor.W (P.add (.const α)) + +/- The `+` spelling of the same type fails: the `binop%` elaborator behind `+` commits the +universe metavariables in the expected type to the first operand's universes before it +considers the heterogeneous `HAdd` instance. -/ +/-- +error: Type mismatch + P + const α +has type + PFunctor.{max uA₁ v, uB} +of sort + Type (max (max (uA₁ + 1) (uB + 1)) (v + 1)) +but is expected to have type + PFunctor.{uA₁, uB} +of sort `Type (max (uA₁ + 1) (uB + 1))` +--- +error: failed to solve universe constraint + max (max uA₁ uB) v =?= max uB uA₁ +while trying to unify + Type (max uA₁ uB v) : Type ((max uA₁ uB v) + 1) +with + Type (max uA₁ uB) : Type ((max uA₁ uB) + 1) +-/ +#guard_msgs in +example (P : PFunctor.{uA₁, uB}) (α : Type v) : Type (max uA₁ uB v) := + PFunctor.W (P + PFunctor.const α) + +/-- The simp set rewrites the head type of a sum through the `+` notation. -/ +example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : + (P + Q).A = (P.A ⊕ Q.A) := by simp + +/-- The simp set computes child types of a sum on both shapes. -/ +example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) : + (P.add Q).B (.inl a) = P.B a := by simp + +example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A) : + (P.add Q).B (.inr a) = Q.B a := by simp + +/-- The simp set computes head and child types of a product. -/ +example (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (a : P.A) (b : Q.A) : + (P * Q).B (a, b) = (P.B a ⊕ Q.B b) := by simp + +/-- The named monomials reduce to the canonical `0`, `1`, and `X`. -/ +example : (const PUnit : PFunctor.{uA, uB}) = 1 := by simp +example : (linear PUnit : PFunctor.{uA, uB}) = X := by simp + +/-- The `ext` tactic picks up the registered extensionality lemma. -/ +example (P Q : PFunctor.{uA, uB}) (h : P.A = Q.A) (h' : ∀ a, P.B a = Q.B (h ▸ a)) : + P = Q := by + ext + · exact h + · exact h' _ + +end CslibTests From 5011c5b4cd9e031a7dd4bd9a5497c47602f75ab5 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Sun, 16 Aug 2026 23:43:39 -0500 Subject: [PATCH 2/4] give explicit names to instances to avoid linter errors --- Cslib/Foundations/Data/PFunctor/Basic.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean index 235e0316a..96cea282b 100644 --- a/Cslib/Foundations/Data/PFunctor/Basic.lean +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -54,7 +54,8 @@ section zero respect to sum (up to equivalence) -/ @[simps] instance instZeroPFunctor : Zero PFunctor where zero := monomial PEmpty PEmpty -instance : IsEmpty (0 : PFunctor.{uA, uB}).A := inferInstanceAs (IsEmpty PEmpty) +instance instIsEmptyZeroPFunctor : IsEmpty (0 : PFunctor.{uA, uB}).A := + inferInstanceAs (IsEmpty PEmpty) end zero @@ -64,9 +65,9 @@ section one respect to product (up to equivalence) -/ @[simps] instance instOnePFunctor : One PFunctor where one := monomial PUnit PEmpty -instance : Unique (1 : PFunctor.{uA, uB}).A := inferInstanceAs (Unique PUnit) +instance instUniqueOneA : Unique (1 : PFunctor.{uA, uB}).A := inferInstanceAs (Unique PUnit) -instance (a : (1 : PFunctor.{uA, uB}).A) : IsEmpty ((1 : PFunctor.{uA, uB}).B a) := +instance instIsEmptyOneB (a : (1 : PFunctor.{uA, uB}).A) : IsEmpty ((1 : PFunctor.{uA, uB}).B a) := inferInstanceAs (IsEmpty PEmpty) end one From 7ba8471d0b63dc902fff5147d43da2f8fe1a205a Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Mon, 17 Aug 2026 01:31:47 -0500 Subject: [PATCH 3/4] address PR feedback --- Cslib/Foundations/Data/PFunctor/Basic.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean index 96cea282b..173d981dd 100644 --- a/Cslib/Foundations/Data/PFunctor/Basic.lean +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -11,15 +11,13 @@ public import Mathlib.Data.PFunctor.Univariate.Basic /-! # Polynomial Functors -This file defines additional constructions on `PFunctor` that don't belong in core mathlib. -The main definition is `monomial A B` for the `PFunctor` with constant family `B` over `A`, -with special cases `const`, `linear`, `selfMonomial`, `purePower`, the indeterminate `X`, -and canonical choices of `0` and `1`. - -We also define the sum `P + Q`, whose shapes are a sum of the shapes of `P` and `Q`, -with a type family defined by sum elimination into the individual child types, -and the product `P * Q`, whose shapes are pairs of shapes, -with a type family defined by sums of the individual child types. +Definitions of common `PFunctor` constructions: +- `monomial A B`: constant direction `B` for any shape `a : A` +- `P + Q`: shapes are a disjoint sum, directions are define by sum elimination on `a : P.A ⊕ Q.A` +- `P * Q`: shapes are pairs of underlying shapes, directions are a disjoint sum over both shapes. + +Special cases `const`, `linear`, `selfMonomial`, `purePower`, the indeterminate `X`, +and canonical choices of `0` and `1` are defined as `abbrev` over `monomial`. -/ @[expose] public section @@ -121,6 +119,7 @@ instance instHAddPFunctor : HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where hAdd := add +/-- Normalize addition of `PFunctor`s to avoid `simp` mismatches between the notations. -/ @[simp] lemma add_def (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P + Q = P.add Q := rfl @@ -141,6 +140,7 @@ instance instHMulPFunctor : HMul PFunctor.{uA₁, uB₁} PFunctor.{uA₂, uB₂} PFunctor.{max uA₁ uA₂, max uB₁ uB₂} where hMul := prod +/-- Normalize multiplication of `PFunctor`s to avoid `simp` mismatches between the notations. -/ @[simp] lemma mul_def (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P * Q = P.prod Q := rfl From 342a94dc252645a43db02ff216eead40e903262b Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Mon, 17 Aug 2026 01:33:46 -0500 Subject: [PATCH 4/4] wording correction --- Cslib/Foundations/Data/PFunctor/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean index 173d981dd..efbb7aba5 100644 --- a/Cslib/Foundations/Data/PFunctor/Basic.lean +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -17,7 +17,7 @@ Definitions of common `PFunctor` constructions: - `P * Q`: shapes are pairs of underlying shapes, directions are a disjoint sum over both shapes. Special cases `const`, `linear`, `selfMonomial`, `purePower`, the indeterminate `X`, -and canonical choices of `0` and `1` are defined as `abbrev` over `monomial`. +and canonical choices of `0` and `1` are defined as `abbrev` or instances over `monomial`. -/ @[expose] public section