Commit 230fb1b3 authored by Michael Sammler's avatar Michael Sammler
Browse files

rename Z_solvers.v -> Z_bitblast.v and use it in base.v

parent 1f985c29
Pipeline #50510 passed with stage
in 17 minutes and 37 seconds
From refinedc.lithium Require Import base.
From Coq.btauto Require Import Btauto.
From Coq Require Import ssreflect.
From stdpp Require Import prelude.
From Coq.btauto Require Export Btauto.
(* set globally in base.v *)
Local Set Keyed Unification.
Local Open Scope bool_scope.
Local Open Scope Z_scope.
......@@ -99,7 +103,7 @@ Ltac bitblast :=
(** tests **)
Goal x a k,
Goal x a k,
Z.land x (Z.land (Z.ones k) (Z.ones k) a) =
Z.land (Z.land (x a) (Z.ones k)) (Z.ones k) a.
by intros; bitblast. Abort.
......
......@@ -8,6 +8,7 @@ From iris.bi Require Import derived_laws.
Import interface.bi derived_laws.bi.
From iris.proofmode Require Import tactics.
From stdpp Require Import natmap.
From refinedc.lithium Require Import Z_bitblast.
Set Default Proof Using "Type".
Global Unset Program Cases.
......@@ -838,12 +839,9 @@ Lemma Z_shiftl_shiftr_0 a n :
Proof.
move => ? Hland.
rewrite -Z.ldiff_ones_r //.
apply Z.bits_inj_iff' => n' ?.
rewrite Z.ldiff_spec Z_ones_spec //. rewrite andb_comm.
case_bool_decide => //=. symmetry.
move/Z.bits_inj_iff' in Hland. move: (Hland n').
rewrite Z.bits_0 Z.land_spec Z_ones_spec//. case_bool_decide => //.
rewrite andb_true_r. naive_solver.
bitblast.
move/Z.bits_inj_iff' in Hland. move: (Hland i ltac:(done)).
by rewrite_testbit.
Qed.
Lemma Z_shiftl_distr_add a b c:
0 c
......
From refinedc.lithium Require Export infrastructure simpl_classes simpl_instances interpreter tactics_extend normalize solvers Z_solvers.
From refinedc.lithium Require Export infrastructure simpl_classes simpl_instances interpreter tactics_extend normalize solvers Z_bitblast.
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