Commit 36ed1a5c authored by Michael Sammler's avatar Michael Sammler
Browse files

solve land and lor sideconditions

parent 91e61a47
Pipeline #60258 passed with stage
in 13 minutes and 36 seconds
......@@ -942,6 +942,28 @@ Proof.
by apply: Z.pow_pos_nonneg.
Qed.
Lemma Z_lor_lt_pow_2 z1 z2 n:
(0 n
0 z1
0 z2
Z.lor z1 z2 < 2 ^ n z1 < 2 ^ n z2 < 2 ^ n)%Z.
Proof.
move => ???.
rewrite !Z_bounded_iff_bits_nonneg; [|try apply Z.lor_nonneg; lia..].
setoid_rewrite Z.lor_spec. setoid_rewrite orb_false_iff. naive_solver lia.
Qed.
Lemma Z_land_lt_pow_2 z1 z2 n:
(0 n
0 z1 < 2 ^ n 0 z2 < 2 ^ n
Z.land z1 z2 < 2 ^ n)%Z.
Proof.
move => ? Hor.
rewrite Z_bounded_iff_bits_nonneg; [|try apply Z.land_nonneg; lia..] => l ?.
rewrite Z.land_spec andb_false_iff.
move: Hor => [[?] | [?]]; rewrite Z_bounded_iff_bits_nonneg //; naive_solver.
Qed.
(* bits for `- n` *)
Lemma Z_bits_opp_z n i :
(0 i)%Z
......
......@@ -190,6 +190,17 @@ Proof. split; naive_solver lia. Qed.
Global Instance simpl_nat_sub_0 (n m : nat) : SimplBothRel (=) (m - 0)%nat n (n = m).
Proof. split; naive_solver lia. Qed.
Global Instance simpl_and_lor_lt_pow2 z1 z2 n `{!CanSolve (0 n 0 z1 0 z2)}:
SimplAnd (Z.lor z1 z2 < 2 ^ n) (λ T, z1 < 2 ^ n z2 < 2 ^ n T).
Proof. unfold CanSolve in * => ?. rewrite Z_lor_lt_pow_2; [ |lia..]. naive_solver. Qed.
Global Instance simpl_and_land_lt_pow2 z1 z2 n `{!TCDone (0 z2 < 2^n 0 n)} :
SimplAnd (Z.land z1 z2 < 2 ^ n) (λ T, T).
Proof.
unfold TCDone in * => ?. split; [|naive_solver] => ?. split; [|done].
apply Z_land_lt_pow_2; naive_solver lia.
Qed.
(* TODO: add a more general impl? *)
Global Instance simpl_eq_0 (n : nat) : SimplBothRel (=) (A := Z) n 0 (n = 0)%nat.
Proof. split; naive_solver lia. Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment