Remove ListNth's and Show's dependence on omega.

Author: Gregory Malecha

theories/Data/ListNth.v

@@ -1,5 +1,4 @@
 Require Import Coq.Lists.List.
-Require Import Coq.omega.Omega.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -11,16 +10,19 @@ Section parametric.
     n < length A ->
     nth_error (A ++ B) n = nth_error A n.
   Proof.
-    induction A; destruct n; simpl; intros; try omega; auto.
-    eapply IHA. omega.
+    induction A; destruct n; simpl; intros; auto.
+    { inversion H. }
+    { inversion H. }
+    { eapply IHA. apply Lt.lt_S_n; assumption. }
   Qed.
 
   Lemma nth_error_app_R : forall (A B : list T) n,
     length A <= n ->
     nth_error (A ++ B) n = nth_error B (n - length A).
   Proof.
-    induction A; destruct n; simpl; intros; try omega; auto.
-    apply IHA. omega.
+    induction A; destruct n; simpl; intros; auto.
+    + inversion H.
+    + apply IHA. apply Le.le_S_n; assumption.
   Qed.
 
   Lemma nth_error_weaken : forall ls' (ls : list T) n v,
@@ -41,32 +43,36 @@ Section parametric.
     nth_error ls n = None.
   Proof.
     clear. induction ls; destruct n; simpl; intros; auto.
-    exfalso; omega. rewrite IHls; auto. omega.
+    + inversion H.
+    + apply IHls. apply Le.le_S_n; assumption.
   Qed.
 
   Lemma nth_error_length : forall (ls ls' : list T) n,
     nth_error (ls ++ ls') (n + length ls) = nth_error ls' n.
   Proof.
     induction ls; simpl; intros.
     rewrite Plus.plus_0_r. auto.
-    cutrewrite (n + S (length ls) = S n + length ls); [ | omega ]. simpl. auto.
+    rewrite <- Plus.plus_Snm_nSm.
+    simpl. eapply IHls.
   Qed.
 
   Theorem nth_error_length_ge : forall T (ls : list T) n,
     nth_error ls n = None -> length ls <= n.
   Proof.
-    induction ls; destruct n; simpl in *; auto; simpl in *; try omega.
-    inversion 1. intro. apply IHls in H. omega.
+    induction ls; destruct n; simpl in *; auto; simpl in *.
+    + intro. apply Le.le_0_n.
+    + inversion 1.
+    + intros. eapply Le.le_n_S. auto.
   Qed.
 
   Lemma nth_error_length_lt : forall {T} (ls : list T) n val,
     nth_error ls n = Some val -> n < length ls.
   Proof.
     induction ls; destruct n; simpl; intros; auto.
-    { inversion H. }
-    { inversion H. }
-    { omega. }
-    { apply Lt.lt_n_S. eauto. }
+    + inversion H.
+    + inversion H.
+    + apply Lt.lt_0_Sn.
+    + apply Lt.lt_n_S. eauto.
   Qed.
 
 

theories/Data/Positive.v

@@ -1,4 +1,4 @@
-Require Import BinPos.
+Require Import Coq.PArith.BinPos.
 Require Import ExtLib.Core.RelDec.
 
 Set Implicit Arguments.
@@ -54,4 +54,4 @@ Proof.
   intuition; [ apply Pos.le_ge | apply Pos.ge_le ]; auto.
 Qed.
 
-Export BinPos.
+Export Coq.PArith.BinPos.

theories/Programming/Show.v

@@ -1,7 +1,7 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Program.Wf.
-Require Import Omega.
-
+Require Import Coq.PArith.BinPos.
+Require Import Coq.ZArith.ZArith.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Programming.Injection.
@@ -13,7 +13,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition showM : Type := 
+Definition showM : Type :=
   forall m, Injection ascii m -> Monoid m -> m.
 
 Class ShowScheme (T : Type) : Type :=
@@ -28,7 +28,7 @@ Global Instance ShowScheme_string : ShowScheme string :=
 
 Global Instance ShowScheme_string_compose : ShowScheme (string -> string) :=
 { show_mon := Monoid_compose string
-; show_inj := String 
+; show_inj := String
 }.
 
 Definition runShow {T} {M : ShowScheme T} (m : showM) : T :=
@@ -39,7 +39,7 @@ Class Show T := show : T -> showM.
 Definition to_string {T} {M : Show T} (v : T) : string :=
   runShow (show v) ""%string.
 
-Definition empty : showM := 
+Definition empty : showM :=
   fun _ _ m => monoid_unit m.
 Definition cat (a b : showM) : showM :=
   fun _ i m => monoid_plus m (a _ i m) (b _ i m).
@@ -63,7 +63,7 @@ End ShowNotation.
 
 Definition indent (indent : showM) (v : showM) : showM :=
   let nl := Ascii.ascii_of_nat 10 in
-    fun _ inj mon => 
+    fun _ inj mon =>
       v _ (fun a => if eq_dec a nl
          then monoid_plus mon (inj a) (indent _ inj mon)
          else inj a) mon.
@@ -91,15 +91,17 @@ Program Fixpoint nat_show (n:nat) {measure n} : showM :=
     (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
 Next Obligation.
   assert (NPeano.div n 10 < n) ; eauto.
-  eapply NPeano.Nat.div_lt ; omega.
+  eapply NPeano.Nat.div_lt.
+  inversion H; apply Lt.lt_O_Sn.
+  repeat constructor.
 Defined.
 Global Instance nat_Show : Show nat := { show := nat_show }.
 
-Global Instance Show_pos : Show positive :=
+Global Instance Show_positive : Show positive :=
   fun x => nat_show (Pos.to_nat x).
 
 Global Instance Show_Z : Show Z :=
-  fun x => 
+  fun x =>
     match x with
       | Z0 => "0"%char
       | Zpos p => show p
@@ -120,7 +122,7 @@ Section sepBy.
   Context {F : Foldable T showM}.
 
   Definition sepBy (sep : showM) (ls : T) : showM :=
-    match 
+    match
       fold (fun s acc =>
         match acc with
           | None => Some s
@@ -138,7 +140,7 @@ Section sepBy_f.
   Variable (f : E -> showM).
 
   Definition sepBy_f (sep : showM) (ls : T) : showM :=
-    match 
+    match
       fold (fun s acc =>
         match acc with
           | None => Some (f s)
@@ -148,7 +150,7 @@ Section sepBy_f.
       | None => empty
       | Some s => s
     end.
-End sepBy_f. 
+End sepBy_f.
 
 Definition wrap (before after : showM) (x : showM) : showM :=
   before << x << after.
@@ -192,5 +194,5 @@ Fixpoint iter_show (ss : list showM) : showM :=
 (*
 Examples:
 Eval compute in (runShow (show (42,"foo"%string)) : string).
-Eval compute in (runShow (show (inl true : bool+string)) 
+Eval compute in (runShow (show (inl true : bool+string))
 *)