diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Notations.v | 28 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 8 |
2 files changed, 32 insertions, 4 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 3aa80406b..b23fe37ac 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -17,8 +17,36 @@ Reserved Notation "x ^ 2" (at level 30, format "x ^ 2"). Reserved Notation "x ^ 3" (at level 30, format "x ^ 3"). Reserved Infix "mod" (at level 40, no associativity). Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50). +Reserved Notation "@ 'is_eq_dec' T R" (at level 10, T at level 8, R at level 8). Reserved Infix "<<" (at level 30, no associativity). Reserved Infix ">>" (at level 30, no associativity). Reserved Infix "&" (at level 50). Reserved Infix "∣" (at level 50). Reserved Infix "~=" (at level 70). +Reserved Infix "==" (at level 70, no associativity). +Reserved Notation "a !== b" (at level 70, no associativity). +Reserved Notation "$$ v" (at level 40). +Reserved Notation "% A" (at level 20, right associativity). +Reserved Notation "$ A" (at level 20, right associativity). +Reserved Notation "A :[ B ]:" (at level 20, right associativity). +Reserved Notation "# A" (at level 20, right associativity). +Reserved Notation "A :+: B" (at level 60, right associativity). +Reserved Notation "A :+c: B" (at level 60, right associativity). +Reserved Notation "A :-: B" (at level 60, right associativity). +Reserved Notation "A :&: B" (at level 45, right associativity). +Reserved Notation "A :^: B" (at level 45, right associativity). +Reserved Notation "A :>>: B" (at level 60, right associativity). +Reserved Notation "A :<<: B" (at level 60, right associativity). +Reserved Notation "A :*: B" (at level 55, right associativity). +(*Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity).*) (* breaks everything *) +Reserved Notation "F :**: e" (at level 70, right associativity). +Reserved Notation "E :->: F" (at level 70, right associativity). +Reserved Notation "A :|: B" (at level 65, left associativity). +Reserved Notation "n ::: A :():" (at level 65, left associativity). +Reserved Notation "& x" (at level 30). +Reserved Notation "** x" (at level 30). +Reserved Notation "A <- X ; B" (at level 70, right associativity). +Reserved Notation "'plet' x := y 'in' z" (at level 60). +Reserved Notation "u [ i ]" (at level 30). +Reserved Notation "v [[ i ]]" (at level 30). +Reserved Notation "u {{ i }}" (at level 30). diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 939ada461..ab844e9ad 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -214,7 +214,7 @@ Module Z. rewrite Z.mul_comm in c_id. apply Zdivide_intro in c_id. apply prime_divisors in c_id; auto. - destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. + destruct c_id; [omega | destruct H; [omega | destruct H; auto] ]. pose proof (prime_ge_2 p prime_p); omega. Qed. @@ -828,9 +828,9 @@ Module Z. | _ => lia | _ => progress subst | [ H : ?n * ?m < 0 |- _ ] - => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]] + => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [ [??]|[??] ] | [ H : ?n / ?m < 0 |- _ ] - => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?] + => apply (proj1 (lt_div_0 n m)) in H; destruct H as [ [ [??]|[??] ] ? ] | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] => assert (0 <= x^y) by zero_bounds; lia | [ H : (?x^?y) < 0 |- _ ] @@ -841,7 +841,7 @@ Module Z. assert (x^y = 0) by lia; clear H H' | [ H : _^_ = 0 |- _ ] - => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]] + => apply Z.pow_eq_0_iff in H; destruct H as [ ?|[??] ] | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] => assert (x = 0) by lia; clear H H' | [ |- ?x <= ?y ] => is_evar x; reflexivity |