[sgraf812]

This PR states the laws of Std.WP as Prop classes over predicate transformers. WP carries only the transformer trans, and MonadicWP (formerly WPMonad) carries only the interpretation of a monad. So wp and Triple take no orders, and an interpretation whose assertions form only a partial order, such as quantum effects under the Löwner order (Discovering formally verified quantum programs with AI), works with vcgen.

The laws:

• PredTrans.IsMonotone t and PredTrans.IsConjunctive t for a transformer t, with instances for pure, >>=, pushArg, pushExceptT and pushOptionT.
• WP.IsMonotone Prog and WP.IsConjunctive x: abbreviations for the transformer of every program of type Prog being monotone, and for the transformer of the program x being conjunctive. MonadicWP.IsMonotone m and MonadicWP.IsConjunctive m state the same for all programs of a monad m.
• MonadicWP.IsLaxMonadMorphism m: pure and bind of the transformers lie below the transformers of pure and bind.
• MonadicWP.IsMonadMorphism m: the transformer commutes with pure and bind.

A WP instance declares only trans. Its monotonicity is a separate instance WP.IsMonotone Prog, whose proof is the former trans_monotone field. WPMonad m Pred EPosts becomes [MonadicWP m Pred EPosts] [MonadicWP.IsMonotone m] [MonadicWP.IsLaxMonadMorphism m], WPConjunctive x becomes WP.IsConjunctive x, and Std.WP.Assertion is deprecated in favour of CompleteLattice.

Stacked on #16425.

🤖 Generated with Claude Code

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 61fe1b8 against 16f65a4 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +2.9G (+0.03%)

Large changes (2🟥)

• 🟥 vcgen/AddSubCancelDeep/100/vcgen//wall-clock: +98ms (+391.82%)
• 🟥 vcgen/AddSubCancelDeep/500/vcgen//wall-clock: +15ms (+19.75%)

Small changes (17✅, 20🟥)

• ✅ build/profile/grind ac//wall-clock: -3ms (-62.83%)
• 🟥 elab/big_deceq//instructions: +15.3M (+0.56%)
• 🟥 elab/big_deceq_rec//instructions: +15.6M (+0.43%)
• 🟥 elab/big_match//instructions: +17.8M (+0.23%)
• 🟥 elab/big_match_nat//instructions: +15.3M (+0.48%)
• ✅ vcgen/AddSubCancel/1200/vcgen//wall-clock: -9ms (-6.28%)
• ✅ vcgen/AddSubCancel/2200/vcgen//wall-clock: -17ms (-5.78%)
• ✅ vcgen/AddSubCancelDeep/100/kernel//wall-clock: -2ms (-9.84%)
• 🟥 vcgen/AddSubCancelDeep/900/vcgen//wall-clock: +13ms (+9.71%)
• 🟥 vcgen/GetThrowSet/200/vcgen//wall-clock: +9ms (+21.14%)
• 🟥 vcgen/GetThrowSetGrind/100/vcgen//wall-clock: +8ms (+10.97%)
• and 26 hidden

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 8059fce against 16f65a4 are in. There are significant results. @sgraf812

• 🟥 build//instructions: +3.3G (+0.04%)

Large changes (7✅, 2🟥)

• ✅ compiled/incr_header_save//maxrss: -82MiB (-4.45%)
• 🟥 compiled/rbmap_checkpoint//task-clock: +460ms (+33.84%)
• 🟥 compiled/rbmap_checkpoint//wall-clock: +472ms (+34.21%)
• ✅ elab/bv_decide_incremental//maxrss: -125MiB (-6.28%)
• ✅ lake/inundation/config/elab//maxrss: -42MiB (-5.10%)
• ✅ lake/inundation/config/import//maxrss: -41MiB (-5.18%)
• ✅ lake/inundation/config/tree//maxrss: -42MiB (-5.24%)
• ✅ lake/inundation/env//maxrss: -41MiB (-5.14%)
• ✅ lake/inundation/setups//maxrss: -41MiB (-4.85%)

Medium changes (2✅)

• ✅ build/profile/grind ac//wall-clock: -3ms (-63.04%)
• ✅ lake/inundation/build/no-op//maxrss: -45MiB (-5.58%)

Small changes (71✅, 16🟥)

• ✅ elab/big_beq//maxrss: -39MiB (-2.24%)
• ✅ elab/big_beq_rec//maxrss: -38MiB (-2.19%)
• ✅ elab/big_deceq//maxrss: -39MiB (-2.24%)
• ✅ elab/big_deceq_rec//maxrss: -38MiB (-2.20%)
• ✅ elab/big_match//maxrss: -38MiB (-2.17%)
• ✅ elab/big_match_nat//maxrss: -39MiB (-2.29%)
• ✅ elab/big_match_nat_split//maxrss: -37MiB (-2.10%)
• ✅ elab/big_match_partial//maxrss: -40MiB (-2.26%)
• ✅ elab/cbv_decide//maxrss: -68MiB (-3.74%)
• ✅ elab/cbv_divisors//maxrss: -70MiB (-4.05%)
• ✅ elab/cbv_merge_sort//maxrss: -70MiB (-3.87%)
• ✅ elab/charactersIn//maxrss: -18MiB (-1.85%)
• ✅ elab/delayed_assign//maxrss: -66MiB (-3.83%)
• ✅ elab/delayed_lift//maxrss: -67MiB (-3.81%)
• ✅ elab/delayed_sharing//maxrss: -68MiB (-3.96%)
• ✅ elab/deriving_mutual_block//maxrss: -67MiB (-3.45%)
• ✅ elab/grind_cases_next//maxrss: -57MiB (-3.16%)
• ✅ elab/inferTypeCache//maxrss: -18MiB (-1.95%)
• ✅ elab/irDeclLookup//maxrss: -23MiB (-2.56%)
• ✅ elab/let_to_have_chain//maxrss: -68MiB (-3.93%)
• and 38 more
• and 29 hidden