Finished admits for canonicalization proofs.

1 files changed, 76 insertions, 19 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 1b7cfafdc..536566312 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -385,34 +385,91 @@ Qed.
       omega.
   Qed.
 
-(* prove that known nonnegative numbers are nonnegative *)
+(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
 Ltac zero_bounds' :=
   repeat match goal with
   | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
-  | [ |- 0 <= _ - _] => apply Zle_minus_le_0
+  | [ |- 0 <= _ - _] => apply Z.le_0_sub
   | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
   | [ |- 0 <= _ / _] => apply Z.div_pos
-  | [ |- 0 < _ + _] => apply Z.add_pos_nonneg
-  (* TODO : this apply is not good: it can make a true goal false. Actually,
-  * we would want this tactic to explore two branches:
-  * - apply Z.add_pos_nonneg and continue
-  * - apply Z.add_nonneg_pos and continue
-  * Keep whichever one solves all subgoals. If neither does, don't apply. *)
-
-  | [ |- 0 < _ - _] => apply Zlt_minus_lt_0
+  | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
+  | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
+  | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
+                       try solve [apply Z.add_nonneg_pos; zero_bounds']
+  | [ |- 0 < _ - _] => apply Z.lt_0_sub
   | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
   | [ |- 0 < _ / _] => apply Z.div_str_pos
+  | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
   end; try omega; try prime_bound; auto.
 
 Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
 
-  Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
-  Proof.
-    apply natlike_ind.
-    + unfold Z.ones. simpl; omega.
-    + intros.
-      rewrite Z_ones_succ by assumption.
-      zero_bounds.
-      apply Z.pow_nonneg; omega.
-  Qed.
+Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
+Proof.
+  apply natlike_ind.
+  + unfold Z.ones. simpl; omega.
+  + intros.
+    rewrite Z_ones_succ by assumption.
+    zero_bounds.
+Qed.
+
+Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
+Proof.
+  intros.
+  unfold Z.ones.
+  rewrite Z.shiftl_1_l.
+  apply Z.lt_succ_lt_pred.
+  apply Z.pow_gt_1; omega.
+Qed.
+
+Lemma N_le_1_l : forall p, (1 <= N.pos p)%N.
+Proof.
+  destruct p; cbv; congruence.
+Qed.
+
+Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
+Proof.
+  induction a; destruct b; intros; try solve [cbv; congruence];
+    simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
+    try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
+    rewrite land_eq in *; unfold N.le, N.compare in *;
+    rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
+    try assumption.
+  destruct (p ?=a)%positive; cbv; congruence.
+Qed.
 
+Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
+  Z.land a b <= a.
+Proof.
+  intros.
+  destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
+  cbv [Z.land].
+  rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
+  auto using Pos_land_upper_bound_l.
+Qed.
+
+Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) ->
+  Z.land a b <= b.
+Proof.
+  intros.
+  rewrite Z.land_comm.
+  auto using Z_land_upper_bound_l.
+Qed.
+
+Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
+  In x l -> x <= fold_right Z.max low l.
+Proof.
+  induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
+  simpl.
+  destruct (in_inv In_list); subst.
+  + apply Z.le_max_l.
+  + etransitivity.
+    - apply IHl; auto; intuition.
+    - apply Z.le_max_r.
+Qed.
+
+Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
+Proof.
+  induction l; intros; try reflexivity.
+  etransitivity; [ apply IHl | apply Z.le_max_r ].
+Qed.