From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- lib/Coqlib.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'lib/Coqlib.v') 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]. *) -- cgit