From 655b67f9600b862447d7f0bcf271a41d50c2e32a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 8 Apr 2017 13:37:59 -0400 Subject: Add ZToInterp_eq_inj --- src/Compilers/Z/Syntax/Util.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Compilers') diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 3c35bdc9e..3e442b4d8 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -162,6 +162,24 @@ Proof. | rewrite wordToZ_ZToWord_wordToZ by omega * ]. Qed. +Lemma ZToInterp_eq_inj {a} x y + : @ZToInterp a x = @ZToInterp a y + <-> match a with + | TZ => x + | TWord lgsz => Z.max 0 x mod 2^Z.of_nat (2^lgsz) + end%Z + = match a with + | TZ => y + | TWord lgsz => Z.max 0 y mod 2^Z.of_nat (2^lgsz) + end%Z. +Proof. + rewrite <- !interpToZ_ZToInterp_mod. + destruct a; try reflexivity; simpl. + split; intro H; try congruence. + rewrite <- (ZToWord_wordToZ (FixedWordSizes.ZToWord x)), <- (ZToWord_wordToZ (FixedWordSizes.ZToWord y)). + congruence. +Qed. + Lemma make_const_correct : forall T v, interp_op Unit (Tbase T) (make_const T v) tt = v. Proof. destruct T; cbv -[FixedWordSizes.ZToWord FixedWordSizes.wordToZ FixedWordSizes.wordT]; -- cgit v1.2.3