diff options
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 02c5d07f..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]. *) @@ -1325,3 +1360,9 @@ Lemma nlist_forall2_imply: Proof. induction 1; simpl; intros; constructor; auto. Qed. + +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. |