Commit 4169ecd0 authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

fix some more examples

parent dd402124
......@@ -310,7 +310,7 @@ Qed.
Lemma bf_from_Z_shiftl_1 it (n : Z):
0 n
1 n = bf_to_Z (bf_cons (range_of n 1) (bf_val 1) bf_nil) it.
1 n = bf_to_Z (bf_cons (range_of n 1) (bf_mask 1) bf_nil) it.
Proof.
rewrite /bf_to_Z/=/bitwise.rc.bf_cons/bitwise.rc.bf_nil => ?.
bitblast.
......@@ -370,4 +370,3 @@ Global Instance max_int_u64_le_lt x :
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
......@@ -219,6 +219,8 @@ Global Instance simpl_bool_to_Z_0 (b : bool) : SimplBothRel (=) 0 (bool_to_Z b)
Proof. split; destruct b; naive_solver. Qed.
Global Instance simpl_bool_to_Z_1 (b : bool) : SimplBothRel (=) 1 (bool_to_Z b) (b = true).
Proof. split; destruct b; naive_solver. Qed.
Global Instance simpl_Z_to_bool_ones_1 (b : bool) : SimplBothRel (=) (Z.ones 1) (Z_of_bool b) (b = true).
Proof. split; destruct b; naive_solver. Qed.
(* Using a SimplBothRel does not work since [x ≠ y] (i.e., [not (x = y)]) does
not unify with [?R ?x ?y] (Coq's unification is too limited here). This can be
......
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