Skip to content

Adapt to math-comp/math-comp#1580 #118

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
spitters merged 1 commit into from
May 2, 2026
Merged

Adapt to math-comp/math-comp#1580 #118

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions theories/Crypt/package/pkg_advantage.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ From SSProve.Relational Require Import OrderEnrichedCategory
OrderEnrichedRelativeMonadExamples.
Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
choice reals distr seq all_algebra fintype realsum.
choice order reals distr seq all_algebra fintype realsum.
Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
From extructures Require Import ord fset fmap.
From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr
Expand Down Expand Up @@ -207,7 +207,7 @@ Proof.
intros P l Q A.
induction l as [| R l ih] in P, Q |- *.
- simpl. auto.
- simpl. eapply order.Order.POrderTheory.le_trans.
- simpl. eapply Order.POrderTheory.le_trans.
+ eapply Advantage_triangle.
+ eapply lerD.
* auto.
Expand Down
32 changes: 16 additions & 16 deletions theories/Crypt/package/pkg_rhl.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ From SSProve.Relational Require Import OrderEnrichedCategory
OrderEnrichedRelativeMonadExamples.
Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
choice reals distr seq all_algebra fintype realsum.
choice order reals distr seq all_algebra fintype realsum.
Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
From extructures Require Import ord fset fmap.
From SSProve.Mon Require Import SPropBase.
Expand Down Expand Up @@ -98,7 +98,7 @@ Proof.
{ destruct ((get_heap s₁ ℓ, s₁, (get_heap s₂ ℓ, s₂)) == (b₁, s₃, (b₂, s₄))) eqn:e.
- move: e => /eqP e. assumption.
- rewrite e in hd. cbn in hd.
rewrite order.Order.POrderTheory.ltxx in hd. discriminate.
rewrite Order.POrderTheory.ltxx in hd. discriminate.
}
inversion e. subst. intuition auto.
Qed.
Expand Down Expand Up @@ -130,7 +130,7 @@ Proof.
{ destruct ((tt, set_heap s1 l v, (tt, set_heap s2 l v)) == (b1, s3, (b2, s4))) eqn:Heqd.
- move: Heqd. move /eqP => Heqd. assumption.
- rewrite Heqd in Hd. simpl in Hd.
rewrite order.Order.POrderTheory.ltxx in Hd. discriminate.
rewrite Order.POrderTheory.ltxx in Hd. discriminate.
}
inversion Heqs.
intuition eauto.
Expand Down Expand Up @@ -178,21 +178,21 @@ Proof.
assert (realsum.psum f ≠ 0) as Hneq.
{ intros Hgt.
rewrite Hgt in H.
rewrite order.Order.POrderTheory.ltxx in H.
rewrite Order.POrderTheory.ltxx in H.
auto. }
destruct (realsum.neq0_psum (R:=R) Hneq) as [x Hx].
exists x. specialize (Hpos x).
rewrite order.Order.POrderTheory.le_eqVlt in Hpos.
rewrite Order.POrderTheory.le_eqVlt in Hpos.
move: Hpos. move /orP => [H1 | H2].
- move: H1. move /eqP => H1. rewrite -H1.
rewrite order.Order.POrderTheory.ltxx. auto.
rewrite Order.POrderTheory.ltxx. auto.
- assumption.
Qed.

Lemma pmulr_me (x y : R) : 0 <= y -> (0 < y * x) -> (0 < x).
Proof.
rewrite le0r => /orP[/eqP->|].
- by rewrite GRing.mul0r order.Order.POrderTheory.ltxx.
- by rewrite GRing.mul0r Order.POrderTheory.ltxx.
- intros. by rewrite -(pmulr_rgt0 x b).
Qed.

Expand All @@ -201,7 +201,7 @@ Lemma ge0_eq {R : realType} {A : eqType} {x y : A} (H : 0 < ((x == y)%:R) :> R)
Proof.
destruct (x == y) eqn:Heq.
- move: Heq. by move /eqP.
- by rewrite order.Order.POrderTheory.ltxx in H.
- by rewrite Order.POrderTheory.ltxx in H.
Qed.

Lemma ne0_eq {R : ringType} {A : eqType} {x y : A} (H : ((x == y)%:R) ≠ (0 : R)) :
Expand Down Expand Up @@ -1265,7 +1265,7 @@ Proof.
end.
2:{
rewrite e in hh. simpl in hh.
rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
rewrite Order.POrderTheory.ltxx in hh. discriminate.
}
move: e => /eqP e. inversion e.
subst. assumption.
Expand Down Expand Up @@ -2569,7 +2569,7 @@ Proof.
unfold SDistr_bind. rewrite dlet_null.
reflexivity.
- intros [? ?] [? ?]. rewrite dnullE.
rewrite order.Order.POrderTheory.ltxx. discriminate.
rewrite Order.POrderTheory.ltxx. discriminate.
Qed.

Lemma r_assert' :
Expand Down Expand Up @@ -2635,7 +2635,7 @@ Proof.
unfold SDistr_bind. rewrite dlet_null.
reflexivity.
- intros [? ?] [? ?]. rewrite dnullE.
rewrite order.Order.POrderTheory.ltxx. discriminate.
rewrite Order.POrderTheory.ltxx. discriminate.
Qed.

Theorem r_assertD :
Expand Down Expand Up @@ -2690,7 +2690,7 @@ Proof.
unfold SDistr_bind. rewrite dlet_null.
reflexivity.
+ intros [? ?] [? ?]. rewrite dnullE.
rewrite order.Order.POrderTheory.ltxx. discriminate.
rewrite Order.POrderTheory.ltxx. discriminate.
Qed.

Lemma rswap_assertD_cmd_eq :
Expand Down Expand Up @@ -2762,7 +2762,7 @@ Proof.
unfold SDistr_bind. rewrite dlet_null.
reflexivity.
+ intros [? ?] [? ?]. rewrite dnullE.
rewrite order.Order.POrderTheory.ltxx. discriminate.
rewrite Order.POrderTheory.ltxx. discriminate.
Qed.

Lemma r_bind_assertD_sym :
Expand Down Expand Up @@ -2812,7 +2812,7 @@ Proof.
end.
2:{
rewrite e in hh. simpl in hh.
rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
rewrite Order.POrderTheory.ltxx in hh. discriminate.
}
move: e => /eqP e. inversion e.
subst. reflexivity.
Expand Down Expand Up @@ -2885,7 +2885,7 @@ Proof.
end.
2:{
rewrite e in hh. simpl in hh.
rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
rewrite Order.POrderTheory.ltxx in hh. discriminate.
}
move: e => /eqP e. inversion e.
subst.
Expand Down Expand Up @@ -2929,7 +2929,7 @@ Proof.
end.
2:{
rewrite e in hh. simpl in hh.
rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
rewrite Order.POrderTheory.ltxx in hh. discriminate.
}
move: e => /eqP e. noconf e.
subst. f_equal.
Expand Down