Val_cmp* -> Val.mxcmp*

1 files changed, 35 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]. *)