Val_cmp* -> Val.mxcmp*

2 files changed, 50 insertions, 0 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 16d880fa..7a7261a3 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1053,6 +1053,41 @@ Proof.
   induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
 Qed.
 
+Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
+Proof.
+  induction l1; cbn; auto with coqlib.
+Qed.
+Hint Resolve is_tail_app: coqlib.
+
+Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
+Proof.
+  induction l1; cbn; auto with coqlib.
+  intros l2 l3 H; inversion H; eauto with coqlib.
+Qed.
+Hint Resolve is_tail_app_inv: coqlib.
+
+Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
+Proof.
+  intros; eauto with coqlib.
+Qed.
+
+Lemma is_tail_app_def A (l1 l2: list A):
+  is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
+Proof.
+  induction 1 as [|x l1 l2]; simpl.
+  - exists nil; simpl; auto.
+  - destruct IHis_tail as (l3 & EQ); rewrite EQ.
+    exists (x::l3); simpl; auto.
+Qed.
+
+Lemma is_tail_bound A (l1 l2: list A):
+  is_tail l1 l2 -> (length l1 <= length l2)%nat.
+Proof.
+  intros H; destruct (is_tail_app_def H) as (l3 & EQ).
+  subst; rewrite app_length.
+  omega.
+Qed.
+
 (** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and
   [P xi yi] holds for all [i]. *)
 
diff --git a/lib/IterList.v b/lib/IterList.v
index 49beb1c5..bde47068 100644
--- a/lib/IterList.v
+++ b/lib/IterList.v
@@ -94,3 +94,18 @@ Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_
 Proof.
   intros; rewrite list_length_z_nat, Nat2Z.id. auto.
 Qed.
+
+Lemma is_tail_list_nth_z A (l1 l2: list A):
+  is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
+Proof.
+  induction 1; simpl.
+  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
+  - assert (X: list_length_z (i :: c2) > list_length_z c1).
+    { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
+      exploit is_tail_bound; simpl; eauto.
+      omega. }
+    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
+    replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
+    rewrite list_length_z_cons.
+    omega.
+Qed.