Skip to content
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

Jump to bottom

adapt to MC#1256 #20

Merged
merged 1 commit into from
Aug 5, 2024
Merged

adapt to MC#1256 #20

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/stern/stern.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import BinPos.

Check warning on line 17 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key N to nat_scope

Check warning on line 17 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key Z to int_scope

Check warning on line 17 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key N to nat_scope

Check warning on line 17 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key Z to int_scope
Import GRing.Theory Num.Theory.
Import PrimeDecompAux.

Expand All @@ -24,8 +24,8 @@
Warning: Hiding binding of key Z to int_scope
*)

Delimit Scope int_scope with Z.

Check warning on line 27 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key Z to Z_scope

Check warning on line 27 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key Z to Z_scope
Delimit Scope nat_scope with N.

Check warning on line 28 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key N to N_scope

Check warning on line 28 in theories/stern/stern.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key N to N_scope


Module Stern.
Expand Down Expand Up @@ -956,7 +956,7 @@
rewrite -{2}(intrD _ 1%:Z) -intr_N floor_sum - intrM - intr_N.
rewrite -[in X in _ + X] mulNr (opprB (floorq x)).
rewrite {2} mulz2 (addrA 1) addrK -(addrA x) -opprD (addrC _ 1) - !(intrD _ 1%:Z).
by rewrite mulz2 mulz2 addrACA addrA addrNK.
by rewrite mulz2 mulz2 addrACA [X in X%:~R]addrA addrNK.
Qed.

(* ORIG
Expand Down Expand Up @@ -1018,7 +1018,7 @@
have ->: -t = (- (1 + (floorq x) * 2%N))%:Q.
rewrite /t /W opprD opprD intrD - intrM - mulrNz //=.
rewrite floor_sum intrD intr_N intrD intrM /t !doubleq -/W (addrACA W).
by rewrite -/a addrA [1 + _]addrA [X in X + a - x]addrA subrK subrr add0r.
by rewrite -/a [LHS]addrA [1 + _]addrA [(1 + _) + _]addrA subrK subrr add0r.
Qed.


Expand Down
Loading