Add coqprime that works with 8.5, bundle bedrock

This simplifes the build process, and also allows us to try to build
with 8.5.  We autodetect the version of Coq in the Makefile to decide
which version of coqprime to build.

1 files changed, 71 insertions, 0 deletions

diff --git a/Bedrock/Nomega.v b/Bedrock/Nomega.v
new file mode 100644
index 000000000..2535cd217
--- /dev/null
+++ b/Bedrock/Nomega.v
@@ -0,0 +1,71 @@
+(* Make [omega] work for [N] *)
+
+Require Import Coq.Arith.Arith Coq.omega.Omega Coq.NArith.NArith.
+
+Local Open Scope N_scope.
+
+Hint Rewrite Nplus_0_r nat_of_Nsucc nat_of_Nplus nat_of_Nminus
+  N_of_nat_of_N nat_of_N_of_nat
+  nat_of_P_o_P_of_succ_nat_eq_succ nat_of_P_succ_morphism : N.
+
+Theorem nat_of_N_eq : forall n m,
+  nat_of_N n = nat_of_N m
+  -> n = m.
+  intros ? ? H; apply (f_equal N_of_nat) in H;
+    autorewrite with N in *; assumption.
+Qed.
+
+Theorem Nneq_in : forall n m,
+  nat_of_N n <> nat_of_N m
+  -> n <> m.
+  congruence.
+Qed.
+
+Theorem Nneq_out : forall n m,
+  n <> m
+  -> nat_of_N n <> nat_of_N m.
+  intuition.
+  apply nat_of_N_eq in H0; tauto.
+Qed.
+
+Theorem Nlt_out : forall n m, n < m
+  -> (nat_of_N n < nat_of_N m)%nat.
+  unfold Nlt; intros.
+  rewrite nat_of_Ncompare in H.
+  apply nat_compare_Lt_lt; assumption.
+Qed.
+
+Theorem Nlt_in : forall n m, (nat_of_N n < nat_of_N m)%nat
+  -> n < m.
+  unfold Nlt; intros.
+  rewrite nat_of_Ncompare.
+  apply (proj1 (nat_compare_lt _ _)); assumption.
+Qed.
+
+Theorem Nge_out : forall n m, n >= m
+  -> (nat_of_N n >= nat_of_N m)%nat.
+  unfold Nge; intros.
+  rewrite nat_of_Ncompare in H.
+  apply nat_compare_ge; assumption.
+Qed.
+
+Theorem Nge_in : forall n m, (nat_of_N n >= nat_of_N m)%nat
+  -> n >= m.
+  unfold Nge; intros.
+  rewrite nat_of_Ncompare.
+  apply nat_compare_ge; assumption.
+Qed.
+
+Ltac nsimp H := simpl in H; repeat progress (autorewrite with N in H; simpl in H).
+
+Ltac pre_nomega :=
+  try (apply nat_of_N_eq || apply Nneq_in || apply Nlt_in || apply Nge_in); simpl;
+    repeat (progress autorewrite with N; simpl);
+    repeat match goal with
+             | [ H : _ <> _ |- _ ] => apply Nneq_out in H; nsimp H
+             | [ H : _ = _ -> False |- _ ] => apply Nneq_out in H; nsimp H
+             | [ H : _ |- _ ] => (apply (f_equal nat_of_N) in H
+               || apply Nlt_out in H || apply Nge_out in H); nsimp H
+           end.
+
+Ltac nomega := pre_nomega; omega || (unfold nat_of_P in *; simpl in *; omega).