diff --git a/Cslib.lean b/Cslib.lean index bc59cb3de..48caacd2b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -72,6 +72,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..d8e934d27 --- /dev/null +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -0,0 +1,101 @@ +/- +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 definitions is `monomial A B` for the `PFunctor` with constant family `B` over `A`, +as well as special cases of this such as a canonical choice 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 of `P` and `Q`. +-/ + +@[expose] public section + +universe uA uB uA₁ uA₂ + +namespace PFunctor + +section monomial + +/-- The monomial `PFunctor` with head type `A` and constant `B` for any `a : A`. -/ +@[reducible] def 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) -/ +@[reducible] protected def zero : PFunctor := monomial PEmpty PEmpty + +instance instZeroPFunctor : Zero PFunctor where zero := PFunctor.zero + +@[simp] lemma zero_A : (0 : PFunctor).A = PEmpty := rfl + +@[simp] lemma zero_B (a : (0 : PFunctor).A) : (0 : PFunctor).B a = PEmpty := rfl + +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) -/ +@[reducible] protected def one : PFunctor := monomial PUnit PEmpty + +instance instOnePFunctor : One PFunctor where one := PFunctor.one + +@[simp] lemma one_A : (1 : PFunctor).A = PUnit := rfl + +@[simp] lemma one_B (a : (1 : PFunctor).A) : (1 : PFunctor).B a = PEmpty := rfl + +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 + +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. -/ +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⟩ + +instance instHAddPFunctor : + HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where + hAdd := add + +@[simp] lemma add_A (P Q : PFunctor) : (add P Q).A = (P.A ⊕ Q.A) := rfl + +@[simp] lemma add_B_inl (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) : + (add P Q).B (.inl a) = P.B a := rfl + +@[simp] lemma add_B_inr (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A) : + (add P Q).B (.inr a) = Q.B a := rfl + +end add + +end PFunctor diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index a29e97470..530a7b6be 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -6,7 +6,7 @@ Authors: Quang Dao module -public import Cslib.Init +public import Cslib.Foundations.Data.PFunctor.Basic public import Mathlib.Data.PFunctor.Univariate.Basic /-! @@ -14,8 +14,9 @@ public import Mathlib.Data.PFunctor.Univariate.Basic We define the free monad on a **polynomial functor** (`PFunctor`), and prove some basic properties. -The free monad `PFunctor.FreeM P` extends the W-type construction with an extra `pure` -constructor, yielding a monad that is free over the polynomial functor `P`. +The free monad `PFunctor.FreeM P` definitionally extends the W-type construction with +an extra `pure` constructor (represented by adding a `PFunctor.linear` term over the return type), +yielding a monad that is free over the polynomial functor `P`. ## Comparison with `Cslib.FreeM` @@ -61,6 +62,14 @@ This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) - `PFunctor.FreeM.lift`: Lift a shape of the base polynomial functor into the free monad. - `PFunctor.FreeM.liftObj`: Lift an object of the base polynomial functor into the free monad. - `PFunctor.FreeM.liftM`: Interpret `FreeM P` into any other monad. + +## Implementation Notes + +`FreeM P α` is a `def`, not an `inductive`: it is the W-type of the polynomial functor +`P.add (C α)`, whose `C α`-shaped nodes are leaves carrying pure values. The raw W-type +representation is confined to the constructors `FreeM.pure` and `FreeM.liftBind`, the +recursor `FreeM.rec`, and a few (dis)equality lemmas; every other definition and proof +factors through this interface. -/ @[expose] public section @@ -69,42 +78,58 @@ universe u v uA uB namespace PFunctor --- Disable generation of unneeded lemmas which the simpNF linter would complain about. -set_option genInjectivity false in -set_option genSizeOfSpec false in -/-- The free monad on a polynomial functor. -This extends `WType` with an extra `pure` constructor. -/ -inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v) - /-- A leaf node wrapping a pure value. -/ - | protected pure {α} (a : α) : P.FreeM α - /-- Invoke the operation `a : P.A` with continuation `cont : P.B a → P.FreeM α`. -/ - | liftBind {α} (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α -deriving Inhabited +/-- The free monad on a polynomial functor: the W-type of the polynomial functor obtained by\ +adjoining a constant shape for each pure value to `P`. -/ +def FreeM (P : PFunctor.{uA, uB}) (α : Type v) : Type (max uA uB v) := + PFunctor.W (P.add (.const α)) namespace FreeM variable {P : PFunctor.{uA, uB}} {α β γ : Type*} +/-- A leaf node wrapping a pure value. -/ +protected def pure (a : α) : P.FreeM α := ⟨.inr a, PEmpty.elim⟩ + +/-- Invoke the operation `a : P.A` with continuation `cont : P.B a → P.FreeM α`. -/ +@[match_pattern] +def liftBind (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α := ⟨.inl a, cont⟩ + +/-- Lift a shape of the base polynomial functor into the free monad. -/ +def lift (a : P.A) : P.FreeM (P.B a) := ⟨.inl a, PFunctor.FreeM.pure⟩ + +instance [Inhabited α] : Inhabited (P.FreeM α) := ⟨.pure default⟩ + instance : Pure (P.FreeM) where pure := .pure +/-- All continuations stored at a pure W-node are equal because their domain is empty. -/ +lemma pure_eq_mk_inl (a : α) (cont : PEmpty → P.FreeM α) : + FreeM.pure a = (⟨.inr a, cont⟩ : P.FreeM α) := + congr_arg (WType.mk (Sum.inr a)) (funext PEmpty.rec) + +/-- Recursor for `FreeM`, stated in terms of its pure and effect-node interface. +This is the only place the W-type representation is consumed; all other definitions factor +through it. Definitions made with it compute definitionally on both node shapes, see +`FreeM.rec_pure` and `FreeM.rec_lift_bind`. -/ +protected def rec {motive : P.FreeM α → Sort u} (pure : ∀ a, motive (pure a)) + (liftBind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)), + motive (FreeM.liftBind a cont)) : ∀ x, motive x + | ⟨.inr a, cont⟩ => pure_eq_mk_inl a cont ▸ pure a + | ⟨.inl a, cont⟩ => liftBind a cont fun u => FreeM.rec pure liftBind (cont u) + @[simp] theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl -/-- Lift a shape of the base polynomial functor into the free monad. -/ -def lift (a : P.A) : P.FreeM (P.B a) := FreeM.liftBind a pure - @[simp] lemma lift_ne_pure (a : P.A) (y : P.B a) : - (lift a : P.FreeM (P.B a)) ≠ pure y := by simp [lift] + (lift a : P.FreeM (P.B a)) ≠ pure y := fun h => by cases congrArg PFunctor.W.head h @[simp] lemma pure_ne_lift (a : P.A) (y : P.B a) : - pure y ≠ (lift a : P.FreeM (P.B a)) := by simp [lift] + pure y ≠ (lift a : P.FreeM (P.B a)) := (lift_ne_pure a y).symm -/-- Bind operation for the `FreeM` monad. +/-- Bind operation for the `FreeM` monad, defined via `FreeM.rec`. The builtin `>>=` notation should be preferred when `α` and `β` are in the same universe. -/ -protected def bind : P.FreeM α → (α → P.FreeM β) → P.FreeM β - | FreeM.pure a, f => f a - | FreeM.liftBind a cont, f => FreeM.liftBind a (fun u ↦ FreeM.bind (cont u) f) +protected def bind (x : P.FreeM α) (f : α → P.FreeM β) : P.FreeM β := + FreeM.rec (motive := fun _ => P.FreeM β) f (fun a _ cont => .liftBind a cont) x instance : Bind (P.FreeM) where bind := .bind @@ -113,12 +138,10 @@ instance : Bind (P.FreeM) where bind := .bind theorem bind_eq_bind {α β : Type v} : (FreeM.bind : P.FreeM α → _ → P.FreeM β) = Bind.bind := rfl -/-- Map a function over a `FreeM` computation. +/-- Map a function over a `FreeM` computation, defined in terms of `FreeM.bind`. The builtin `<$>` notation should be preferred when `α` and `β` are in the same universe. -/ -def map (f : α → β) : P.FreeM α → P.FreeM β - | .pure a => .pure (f a) - | .liftBind a cont => .liftBind a fun u => FreeM.map f (cont u) +def map (f : α → β) (x : P.FreeM α) : P.FreeM β := x.bind (FreeM.pure ∘ f) instance : Functor (P.FreeM) where map := .map @@ -132,6 +155,21 @@ theorem map_eq_map {α β : Type v} : lemma liftBind_eq (a : P.A) (cont : P.B a → P.FreeM α) : FreeM.liftBind a cont = (FreeM.lift a).bind cont := rfl +@[simp] +lemma rec_pure {motive : P.FreeM α → Sort u} (hp : ∀ a, motive (pure a)) + (hlb : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)), + motive (FreeM.liftBind a cont)) (a : α) : + FreeM.rec hp hlb (pure a) = hp a := rfl + +/-- `FreeM.rec` computes definitionally on effect nodes. +Stated for the simp-normal form `(FreeM.lift a).bind cont` of `FreeM.liftBind a cont`. -/ +@[simp] +lemma rec_lift_bind {motive : P.FreeM α → Sort u} (hp : ∀ a, motive (pure a)) + (hlb : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)), + motive (FreeM.liftBind a cont)) (a : P.A) (cont : P.B a → P.FreeM α) : + FreeM.rec hp hlb ((FreeM.lift a).bind cont) = + hlb a cont fun i => FreeM.rec hp hlb (cont i) := rfl + /-- Lift an object of the base polynomial functor into the free monad. This lifts the shape `x.1` with `lift` and relabels the responses with `x.2`. We use the @@ -142,14 +180,17 @@ abbrev liftObj (x : P.Obj α) : P.FreeM α := (lift x.1).map x.2 instance : MonadLift P (P.FreeM) where monadLift x := FreeM.liftObj x -@[simp] lemma liftObj_ne_pure (x : P.Obj α) (y : α) : - (liftObj x : P.FreeM α) ≠ pure y := by simp [liftObj, lift, map, -liftBind_eq] - -@[simp] lemma pure_ne_liftObj (x : P.Obj α) (y : α) : - pure y ≠ (liftObj x : P.FreeM α) := by simp [liftObj, lift, map, -liftBind_eq] - lemma monadLift_eq_liftObj (x : P.Obj α) : (x : P.FreeM α) = FreeM.liftObj x := rfl +/-- Case analysis for `FreeM`, stated in terms of its pure and effect-node interface and in +the same simp-normal form as `FreeM.induction`. -/ +@[cases_eliminator] +protected def cases {motive : P.FreeM α → Sort u} + (pure : ∀ a, motive (pure a)) + (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α), motive ((FreeM.lift a).bind cont)) : + ∀ x, motive x := + FreeM.rec pure fun a cont _ => lift_bind a cont + set_option linter.unusedVariables false in /-- An override for the default induction principle that is in simp-normal form. @@ -158,37 +199,40 @@ Note that when `α` and `P.B a` are in the same universe, this simplifies slight protected theorem induction {motive : P.FreeM α → Prop} (pure : ∀ a, motive (pure a)) (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (ih : ∀ i, motive (cont i)), - motive ((FreeM.lift a).bind cont)) : ∀ x, motive x - | .pure a => pure a - | liftBind a cont => lift_bind a cont fun u => FreeM.induction pure lift_bind (cont u) + motive ((FreeM.lift a).bind cont)) : ∀ x, motive x := + FreeM.rec pure lift_bind + +/-- `.pure a` followed by `bind` collapses immediately. -/ +@[simp] +lemma pure_bind (a : α) (f : α → P.FreeM β) : + (pure a : P.FreeM α).bind f = f a := rfl + +@[simp] +lemma liftBind_bind (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) : + ((FreeM.lift a).bind cont).bind f = (FreeM.lift a).bind (fun u ↦ (cont u).bind f) := rfl protected theorem bind_assoc (x : P.FreeM α) (f : α → P.FreeM β) (g : β → P.FreeM γ) : (x.bind f).bind g = x.bind (fun a => (f a).bind g) := by induction x with | pure a => rfl - | lift_bind a cont ih => simp [← liftBind_eq, FreeM.bind, ih] at * + | lift_bind a cont ih => simp [ih] -/-- `.pure a` followed by `bind` collapses immediately. -/ @[simp] -lemma pure_bind (a : α) (f : α → P.FreeM β) : - (pure a : P.FreeM α).bind f = f a := rfl +lemma bind_pure (x : P.FreeM α) : x.bind pure = x := by + induction x with + | pure a => rfl + | lift_bind a cont ih => simp [ih] @[simp] -lemma bind_pure : ∀ x : P.FreeM α, x.bind pure = x - | .pure a => rfl - | .liftBind a cont => by - simp only [FreeM.bind]; congr 1; funext u; exact bind_pure (cont u) +lemma bind_pure_comp (f : α → β) (x : P.FreeM α) : x.bind (pure ∘ f) = map f x := rfl @[simp] -lemma bind_pure_comp (f : α → β) : ∀ x : P.FreeM α, x.bind (pure ∘ f) = map f x - | .pure a => rfl - | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp] +lemma map_pure (f : α → β) (a : α) : + (pure a : P.FreeM α).map f = pure (f a) := rfl @[simp] -lemma liftBind_bind (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) : - ((FreeM.lift a).bind cont).bind f = (FreeM.lift a).bind (fun u ↦ (cont u).bind f) := by - simp only [lift] - exact FreeM.bind_assoc (FreeM.liftBind a pure) cont f +lemma map_lift_bind (f : α → β) (a : P.A) (cont : P.B a → P.FreeM α) : + ((FreeM.lift a).bind cont).map f = (FreeM.lift a).bind (fun u ↦ (cont u).map f) := rfl @[simp] lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) : @@ -198,7 +242,7 @@ lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) : x.bind f = pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by cases x with | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩ - | liftBind a cont => + | lift_bind a cont => constructor · intro h cases h @@ -209,32 +253,33 @@ lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) : pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by cases x with | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩ - | liftBind a cont => + | lift_bind a cont => constructor · intro h cases h · rintro ⟨_, h, _⟩ cases h +lemma lift_bind_ne_pure (a : P.A) (cont : P.B a → P.FreeM α) (y : α) : + (FreeM.lift a).bind cont ≠ pure y := by simp + +lemma pure_ne_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) (y : α) : + pure y ≠ (FreeM.lift a).bind cont := by simp + +@[simp] lemma liftObj_ne_pure (x : P.Obj α) (y : α) : + (liftObj x : P.FreeM α) ≠ pure y := lift_bind_ne_pure _ _ _ + +@[simp] lemma pure_ne_liftObj (x : P.Obj α) (y : α) : + pure y ≠ (liftObj x : P.FreeM α) := pure_ne_lift_bind _ _ _ + instance : Monad (P.FreeM) where @[simp] -theorem id_map : ∀ x : P.FreeM α, map id x = x - | .pure a => rfl - | .liftBind a cont => by - simp only [map] - congr 1 - funext u - exact id_map (cont u) +theorem id_map (x : P.FreeM α) : map id x = x := bind_pure x -theorem comp_map (h : β → γ) (g : α → β) : - ∀ x : P.FreeM α, map (h ∘ g) x = map h (map g x) - | .pure a => rfl - | .liftBind a cont => by - simp only [map] - congr 1 - funext u - exact comp_map h g (cont u) +theorem comp_map (h : β → γ) (g : α → β) (x : P.FreeM α) : + map (h ∘ g) x = map h (map g x) := + (FreeM.bind_assoc x (FreeM.pure ∘ g) (FreeM.pure ∘ h)).symm instance : LawfulMonad (P.FreeM) := LawfulMonad.mk' (bind_pure_comp := bind_pure_comp) @@ -266,9 +311,8 @@ variable {m : Type uB → Type v} {α : Type uB} /-- Interpret a `FreeM P` computation into any monad `m` by providing an interpretation `interp : (a : P.A) → m (P.B a)` for each operation. -/ -protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α - | .pure a => pure a - | .liftBind a cont => interp a >>= fun u ↦ (cont u).liftM interp +protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α := + FreeM.rec (motive := fun _ => m α) (fun a => pure a) (fun a _ ih => interp a >>= ih) variable [Monad m] (interp : (a : P.A) → m (P.B a)) @@ -278,9 +322,7 @@ lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure @[simp] lemma liftM_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : FreeM.liftM interp (FreeM.lift a >>= cont) = - (do let u ← interp a; (cont u).liftM interp) := by - dsimp only [FreeM.liftM, FreeM.bind, FreeM.lift] - rfl + (do let u ← interp a; (cont u).liftM interp) := rfl /-- A predicate stating that `eval : P.FreeM α → m α` is an interpreter for the polynomial diff --git a/CslibTests.lean b/CslibTests.lean index b26f3aa5d..69f07dfa9 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -12,4 +12,5 @@ import CslibTests.ImportWithMathlib import CslibTests.LTS import CslibTests.LambdaCalculus import CslibTests.MLL +import CslibTests.PFunctor import CslibTests.Reduction diff --git a/CslibTests/PFunctor.lean b/CslibTests/PFunctor.lean new file mode 100644 index 000000000..92a0d2aac --- /dev/null +++ b/CslibTests/PFunctor.lean @@ -0,0 +1,50 @@ +/- +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.Free + +/-! +# Polynomial Functor Universe Tests + +These tests exercise the universe-polymorphic polynomial sum and the W-type representation of +`PFunctor.FreeM`. +-/ + +universe uA₁ uA₂ uB v + +namespace CslibTests + +open PFunctor + +variable {P : PFunctor.{uA₁, uB}} {α : Type v} {β : Type uA₂} + +/-- Addition notation remains 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 + +private def isPure {P : PFunctor.{uA₁, uB}} {α : Type v} : P.FreeM α → Bool := + FreeM.rec (motive := fun _ => Bool) (fun _ => true) (fun _ _ _ => false) + +/-- The `cases` tactic picks up the registered case eliminator. -/ +example (x : P.FreeM α) : isPure x = true ∨ isPure x = false := by + cases x with + | pure a => left; rfl + | lift_bind a cont => right; rfl + +/-- The `induction` tactic picks up the registered induction eliminator. -/ +example (x : P.FreeM α) : x.bind FreeM.pure = x := by + induction x with + | pure a => rfl + | lift_bind a cont ih => simp only [FreeM.liftBind_bind, ih] + +private def coin : PFunctor.{0, 0} := ⟨Bool, fun b => if b then Bool else Nat⟩ + +/-- A ground free computation remains small enough to serve as another polynomial's directions. -/ +private def scheduler : PFunctor.{0, 0} := ⟨Unit, fun _ => coin.FreeM Bool⟩ + +example : scheduler.B () = coin.FreeM Bool := rfl + +end CslibTests