From f303b5d202025148047023fe3a4342028cd92ad5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Dobranowski?= Date: Fri, 12 Dec 2025 20:43:33 +0100 Subject: [PATCH 1/3] Add some instances for Plausible --- Apportionmentlib.lean | 1 + Apportionmentlib/Basic.lean | 4 ++ Apportionmentlib/PlausibleInstances.lean | 61 ++++++++++++++++++++++++ 3 files changed, 66 insertions(+) create mode 100644 Apportionmentlib/PlausibleInstances.lean diff --git a/Apportionmentlib.lean b/Apportionmentlib.lean index 2d0d72b..33b30ea 100644 --- a/Apportionmentlib.lean +++ b/Apportionmentlib.lean @@ -1 +1,2 @@ import Apportionmentlib.Basic +import Apportionmentlib.PlausibleInstances diff --git a/Apportionmentlib/Basic.lean b/Apportionmentlib/Basic.lean index 734f937..0a57ba5 100644 --- a/Apportionmentlib/Basic.lean +++ b/Apportionmentlib/Basic.lean @@ -60,6 +60,10 @@ structure Election (n : ℕ) where houseSize : ℕ deriving DecidableEq +instance {n : ℕ} : Repr (Election n) where + reprPrec e _ := + "Election(votes = " ++ repr e.votes.toArray ++ ", houseSize = " ++ repr e.houseSize ++ ")" + /-- An apportionment is a vector of natural numbers representing the number of seats allocated to each party (at the corresponding index). -/ abbrev Apportionment (n : ℕ) : Type := Vector ℕ n diff --git a/Apportionmentlib/PlausibleInstances.lean b/Apportionmentlib/PlausibleInstances.lean new file mode 100644 index 0000000..07bb723 --- /dev/null +++ b/Apportionmentlib/PlausibleInstances.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2025 Michał Dobranowski. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michał Dobranowski +-/ +import Plausible.Arbitrary +import Apportionmentlib.Basic + +/-! +# Instances for Plausible + +In this file, we define some instances (like `Shrinkable`, `Arbitrary`, `SampleableExt`) so that +you can use the `plausible` tactic with Apportionmentlib. For example, try: + +```lean4 +import Apportionmentlib +import Plausible + +open Apportionmentlib + +example {n : ℕ} (e : Election n) (h : 2 < n) : e.votes[0] > e.votes[1] := by + plausible +``` +-/ + +open Plausible + +namespace Apportionmentlib + +instance {n : ℕ} : Shrinkable (Election n) where + shrink e := + let shrunkHouseSizes := Shrinkable.shrink e.houseSize + Election.mk + <$> pure e.votes + <*> shrunkHouseSizes + +instance {n : ℕ} : Arbitrary (Election n) where + arbitrary := do + let votes ← (Vector.replicate n ()).mapM fun _ => Gen.chooseNat + let houseSize ← Gen.choose Nat 1 20 (by decide) + return { + votes := votes, + houseSize := houseSize + } + +instance {n : ℕ} : SampleableExt (Election n) := SampleableExt.selfContained + +#eval Shrinkable.shrink 10 + +#eval Shrinkable.shrink ({ + votes := #v[100, 200, 300], + houseSize := 10 +} : Election 3) + +-- #sample Election 3 + + +example {n : ℕ} (e : Election n) (h : 2 < n) : e.votes[0] > e.votes[1] := by + plausible + +end Apportionmentlib From 6713ee055de76fa9674b9d7cf99c87dc5986875f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Dobranowski?= Date: Sun, 28 Dec 2025 20:57:45 +0100 Subject: [PATCH 2/3] Clean up --- Apportionmentlib/PlausibleInstances.lean | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/Apportionmentlib/PlausibleInstances.lean b/Apportionmentlib/PlausibleInstances.lean index 07bb723..594f369 100644 --- a/Apportionmentlib/PlausibleInstances.lean +++ b/Apportionmentlib/PlausibleInstances.lean @@ -20,6 +20,8 @@ open Apportionmentlib example {n : ℕ} (e : Election n) (h : 2 < n) : e.votes[0] > e.votes[1] := by plausible + +#sample Election 2 ``` -/ @@ -45,17 +47,4 @@ instance {n : ℕ} : Arbitrary (Election n) where instance {n : ℕ} : SampleableExt (Election n) := SampleableExt.selfContained -#eval Shrinkable.shrink 10 - -#eval Shrinkable.shrink ({ - votes := #v[100, 200, 300], - houseSize := 10 -} : Election 3) - --- #sample Election 3 - - -example {n : ℕ} (e : Election n) (h : 2 < n) : e.votes[0] > e.votes[1] := by - plausible - end Apportionmentlib From 9a6dd53656c1f417c7872e568a680de0b6fdc08b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Dobranowski?= Date: Sun, 28 Dec 2025 21:22:02 +0100 Subject: [PATCH 3/3] Apply suggestions --- Apportionmentlib/Basic.lean | 2 +- Apportionmentlib/PlausibleInstances.lean | 13 ++++++++++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/Apportionmentlib/Basic.lean b/Apportionmentlib/Basic.lean index 0a57ba5..3c8d88e 100644 --- a/Apportionmentlib/Basic.lean +++ b/Apportionmentlib/Basic.lean @@ -62,7 +62,7 @@ structure Election (n : ℕ) where instance {n : ℕ} : Repr (Election n) where reprPrec e _ := - "Election(votes = " ++ repr e.votes.toArray ++ ", houseSize = " ++ repr e.houseSize ++ ")" + "{ votes := " ++ repr e.votes.toArray ++ ", houseSize := " ++ repr e.houseSize ++ " }" /-- An apportionment is a vector of natural numbers representing the number of seats allocated to each party (at the corresponding index). -/ diff --git a/Apportionmentlib/PlausibleInstances.lean b/Apportionmentlib/PlausibleInstances.lean index 594f369..2315420 100644 --- a/Apportionmentlib/PlausibleInstances.lean +++ b/Apportionmentlib/PlausibleInstances.lean @@ -29,12 +29,19 @@ open Plausible namespace Apportionmentlib +instance {n : ℕ} : Shrinkable (Vector ℕ n) where + shrink v := + (List.finRange n).flatMap fun (i : Fin n) => + (Shrinkable.shrink v[i]).map fun v' => v.set i v' + instance {n : ℕ} : Shrinkable (Election n) where shrink e := + let shrunkVotes := Shrinkable.shrink e.votes let shrunkHouseSizes := Shrinkable.shrink e.houseSize - Election.mk - <$> pure e.votes - <*> shrunkHouseSizes + -- shrink votes only, shrink houseSize only, or shrink both + (shrunkVotes.map fun v => Election.mk v e.houseSize) ++ + (shrunkHouseSizes.map fun h => Election.mk e.votes h) ++ + (shrunkVotes.flatMap fun v => shrunkHouseSizes.map fun h => Election.mk v h) instance {n : ℕ} : Arbitrary (Election n) where arbitrary := do