From ad6e522875aa1644849a4cda8b71f92223d98cc0 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 6 Oct 2026 09:56:55 +0200 Subject: [PATCH] fix(theories): make Dexcepted phoare bounds SMT-free `phoare_indirect` and `ll_phoare_indirect` discharged their bound with `smt(... ge0_mu)`, which fails with recent provers (Z3 5.1, CVC5 1.4). Prove them directly from `pr_indirect`/`ll_pr_indirect`, as already done for `phoare_direct`. --- theories/distributions/Dexcepted.ec | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index 4bcaee7d4..d75464dde 100644 --- a/theories/distributions/Dexcepted.ec +++ b/theories/distributions/Dexcepted.ec @@ -154,7 +154,10 @@ qed. phoare phoare_indirect x' X' P: [ S.indirect: x = x' /\ X = X' ==> P res ] = (weight (dt x) * mu (dt x \ X x) P). -proof. bypr=> &m; smt(pr_indirect ge0_mu). qed. +proof. +bypr=> &m; rewrite mulr_ge0 1:ge0_weight 1:ge0_mu /= => [#] -> ->. +exact/(@pr_indirect &m x' X' P). +qed. (* -------------------------------------------------------------------- *) lemma ll_pr_indirect &m x' X' P: @@ -166,7 +169,9 @@ phoare ll_phoare_indirect x' X' P: [ S.indirect: x = x' /\ X = X' /\ is_lossless (dt x') ==> P res ] = (mu (dt x \ X x) P). proof. -by bypr=> &m; smt(ll_pr_indirect ge0_mu). qed. +bypr=> &m; rewrite ge0_mu /= => [#] -> -> dt_ll. +exact/(@ll_pr_indirect &m x' X' P dt_ll). +qed. (* -------------------------------------------------------------------- *) lemma indirect_direct &m x X P: