diff options
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 335ebf26..0bd4707d 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -239,6 +239,22 @@ f_equal. auto using just_list_length. Qed. +Fixpoint member_Z_list (x : Z) (l : list Z) : bool := +match l with +| [] => false +| h::t => if x =? h then true else member_Z_list x t +end. + +Lemma member_Z_list_In {x l} : member_Z_list x l = true <-> In x l. +induction l. +* simpl. split. congruence. tauto. +* simpl. destruct (x =? a) eqn:H. + + rewrite Z.eqb_eq in H. subst. tauto. + + rewrite Z.eqb_neq in H. split. + - intro Heq. right. apply IHl. assumption. + - intros [bad | good]. congruence. apply IHl. assumption. +Qed. + (*** Bits *) Inductive bitU := B0 | B1 | BU. |