From 1cdcec9f4be7dd94a1ea7a3dcd98add33a2378d8 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 14 Oct 2016 16:41:32 +0200 Subject: Some proofs for the Int63 glue --- src/versions/standard/Int63/Int63Axioms_standard.v | 112 +++++++++++++++++++-- 1 file changed, 104 insertions(+), 8 deletions(-) (limited to 'src/versions') diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v index 7e89ef6..bbc353a 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/versions/standard/Int63/Int63Axioms_standard.v @@ -42,18 +42,30 @@ Local Open Scope Z_scope. (* Bijection : int63 <-> Bvector size *) -Lemma to_Z_inj : forall x y, [|x|] = [|y|] -> x = y. +Theorem to_Z_inj : forall x y, [|x|] = [|y|] -> x = y. Proof Ring31.Int31_canonic. -Lemma of_to_Z : forall x, of_Z ([|x|]) = x. +Theorem of_to_Z : forall x, of_Z ([|x|]) = x. Proof. exact phi_inv_phi. Qed. (* Comparisons *) -Axiom eqb_refl : forall x, (x == x)%int = true. +Theorem eqb_refl x : (x == x)%int = true. +Proof. now rewrite Ring31.eqb31_eq. Qed. -Axiom ltb_spec : forall x y, (x < y)%int = true <-> [|x|] < [|y|]. +Theorem ltb_spec x y : (x < y)%int = true <-> [|x|] < [|y|]. +Proof. + unfold ltb. rewrite spec_compare, <- Z.compare_lt_iff. + change (phi x ?= phi y) with ([|x|] ?= [|y|]). + case ([|x|] ?= [|y|]); intuition; discriminate. +Qed. + +Theorem leb_spec x y : (x <= y)%int = true <-> [|x|] <= [|y|]. +Proof. + unfold leb. rewrite spec_compare, <- Z.compare_le_iff. + change (phi x ?= phi y) with ([|x|] ?= [|y|]). + case ([|x|] ?= [|y|]); intuition; discriminate. +Qed. -Axiom leb_spec : forall x y, (x <= y)%int = true <-> [|x|] <= [|y|]. (** Specification of logical operations *) Lemma lsl_spec_alt p : @@ -69,7 +81,7 @@ Proof. * exact Z.le_0_1. Qed. -Lemma lsl_spec x p : [| x << p |] = ([|x|] * 2^[|p|]) mod wB. +Theorem lsl_spec x p : [| x << p |] = ([|x|] * 2^[|p|]) mod wB. Proof. unfold lsl. rewrite addmuldiv31_equiv, lsl_spec_alt, Nat2Z.inj_abs_nat, Z.abs_eq. @@ -77,6 +89,7 @@ Proof. - now destruct (phi_bounded p). Qed. + Lemma div_greater (p x:int) (H:Z.of_nat Int31.size <= [|p|]) : [|x|] / 2 ^ [|p|] = 0. Proof. apply Z.div_small. destruct (phi_bounded x) as [H1 H2]. split; auto. @@ -84,7 +97,7 @@ Proof. exact Z.lt_0_2. Qed. -Lemma lsr_spec x p : [|x >> p|] = [|x|] / 2 ^ [|p|]. +Theorem lsr_spec x p : [|x >> p|] = [|x|] / 2 ^ [|p|]. Proof. unfold lsr. case_eq (p < 31%int31)%int; intro Heq. - assert (H : [|31%int31 - p|] = 31 - [|p|]). @@ -104,10 +117,93 @@ Proof. Qed. +Lemma bit_testbit x i : bit x i = Z.testbit [|x|] [|i|]. +Admitted. +(* Proof. *) +(* case_eq [|i|]. *) +(* - simpl. change 0 with [|0|]. intro Heq. apply Ring31.Int31_canonic in Heq. subst i. *) +(* unfold bit. *) + + +Lemma Z_pos_xO_pow i x (Hi:0 <= i) : Z.pos x < 2 ^ i <-> Z.pos x~0 < 2 ^ (i+1). +Proof. rewrite Pos2Z.inj_xO, Z.pow_add_r; auto using Z.le_0_1; lia. Qed. + +Lemma Z_pos_xI_pow i x (Hi:0 <= i) : Z.pos x < 2 ^ i <-> Z.pos x~1 < 2 ^ (i+1). +Proof. rewrite Pos2Z.inj_xI, Z.pow_add_r; auto using Z.le_0_1; lia. Qed. + +Lemma pow_nonneg i (Hi : 1 <= 2 ^ i) : 0 <= i. +Proof. + destruct (Z.le_gt_cases 0 i); auto. + rewrite (Z.pow_neg_r _ _ H) in Hi. lia. +Qed. + +Lemma pow_pos i (Hi : 1 < 2 ^ i) : 0 < i. +Proof. + destruct (Z.lt_trichotomy 0 i) as [H|[H|H]]; auto. + - subst i. lia. + - rewrite (Z.pow_neg_r _ _ H) in Hi. lia. +Qed. + +Lemma pos_land_bounded : forall x y i, + Z.pos x < 2 ^ i -> Z.pos y < 2 ^ i -> Z.of_N (Pos.land x y) < 2 ^ i. +Proof. + induction x as [x IHx|x IHx| ]; intros [y|y| ] i; auto. + - simpl. intro H. + assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~1)); auto; lia). + generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- !Z_pos_xI_pow; auto. intros H1 H2. + assert (H3:=IHx _ _ H1 H2). + unfold Pos.Nsucc_double. case_eq (Pos.land x y). + * intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia. + * intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xI_pow; auto. + replace (i - 1 + 1) with i by ring. clear. lia. + - simpl. intro H. + assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~1)); auto; lia). + generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- Z_pos_xI_pow, <- Z_pos_xO_pow; auto. intros H1 H2. + assert (H3:=IHx _ _ H1 H2). + unfold Pos.Ndouble. case_eq (Pos.land x y). + * intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia. + * intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto. + replace (i - 1 + 1) with i by ring. clear. lia. + - simpl. intro H. + assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~0)); auto; lia). + generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- Z_pos_xI_pow, <- Z_pos_xO_pow; auto. intros H1 H2. + assert (H3:=IHx _ _ H1 H2). + unfold Pos.Ndouble. case_eq (Pos.land x y). + * intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia. + * intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto. + replace (i - 1 + 1) with i by ring. clear. lia. + - simpl. intro H. + assert (H4:0 <= i - 1) by (assert (H4:0 < i); try lia; apply pow_pos; apply (Z.le_lt_trans _ (Z.pos x~0)); auto; lia). + generalize H. replace i with ((i-1)+1) at 1 2 by ring. rewrite <- !Z_pos_xO_pow; auto. intros H1 H2. + assert (H3:=IHx _ _ H1 H2). + unfold Pos.Ndouble. case_eq (Pos.land x y). + * intros _. eapply Z.le_lt_trans; [ |exact H]. clear. lia. + * intros p Hp. revert H3. rewrite Hp, N2Z.inj_pos, Z_pos_xO_pow; auto. + replace (i - 1 + 1) with i by ring. clear. lia. + - simpl. intros H _. apply (Z.le_lt_trans _ (Z.pos x~0)); lia. + - simpl. intros H _. apply (Z.le_lt_trans _ 1); lia. +Qed. + +Lemma Z_land_bounded i : forall x y, + 0 <= x < 2 ^ i -> 0 <= y < 2 ^ i -> 0 <= Z.land x y < 2 ^ i. +Proof. + intros [ |p|p] [ |q|q]; auto. + - intros [_ H1] [_ H2]. simpl. split. + * apply N2Z.is_nonneg. + * now apply pos_land_bounded. +Admitted. +Theorem land_spec x y i : bit (x land y) i = bit x i && bit y i. +Proof. + rewrite !bit_testbit. change (x land y) with (land31 x y). unfold land31. + rewrite phi_phi_inv. rewrite Zmod_small. + - apply Z.land_spec. + - split. + * rewrite Z.land_nonneg. left. now destruct (phi_bounded x). + * now destruct (Z_land_bounded _ _ _ (phi_bounded x) (phi_bounded y)). +Qed. -Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i. Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i. -- cgit