From bf28d8f9bf531e15db8075273067274ccb8a2537 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2017 20:35:50 -0400 Subject: Add wneg_inj --- Bedrock/Word.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'Bedrock') diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 09bfc036b..ecdecee3c 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -1089,6 +1089,17 @@ Proof. f_equal. eapply IHa. destruct (wordToN a); destruct (wordToN (wtl b0)); simpl in *; try congruence. Qed. +Lemma wneg_involutive : forall sz (a : word sz), + wneg (wneg a) = a. +Proof. + intros; eapply Ropp_opp; [ exact _ | apply wring_eq_ext | apply wring ]. +Qed. +Lemma wneg_inj : forall sz (a b : word sz), + wneg a = wneg b -> a = b. +Proof. + intros sz a b H. + cut (wneg (wneg a) = wneg (wneg b)); [ rewrite !wneg_involutive | ]; congruence. +Qed. Lemma unique_inverse : forall sz (a b1 b2 : word sz), a ^+ b1 = wzero _ -> a ^+ b2 = wzero _ -> -- cgit v1.2.3