Library ListHelpers
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Usefull TheoryList extensions:
- AllS_x_P
- Last and corresponding lemmas
- Suffix and corresponding lemmas
If AllS P l holds, predicate P holds for every element x in l.
Lemma AllS_x_P : forall A P l (x:A), AllS P l -> In x l -> P x.
Proof.
intros.
induction H.
simpl in H0.
elim H0.
elim H0.
intro eq_a_x.
rewrite <- eq_a_x; exact H.
assumption.
Qed.
End TheoryList.
Section In.
Variable A : Type.
Proof.
intros.
induction H.
simpl in H0.
elim H0.
elim H0.
intro eq_a_x.
rewrite <- eq_a_x; exact H.
assumption.
Qed.
End TheoryList.
Section In.
Variable A : Type.
If head l = Some x, x is element of l.
Lemma In_head : forall (x:A) l, head l = Some x -> In x l.
Proof.
intros.
induction l.
discriminate H.
simpl in H.
unfold In.
left.
inversion H.
reflexivity.
Qed.
Proof.
intros.
induction l.
discriminate H.
simpl in H.
unfold In.
left.
inversion H.
reflexivity.
Qed.
If l=y::nil, In x l -> x=y.
Lemma In_singleton : forall (x y:A),
In x (y::nil) -> x = y.
Proof.
intros.
case H; intuition.
Qed.
Lemma in_nth:
forall e (l : list A),
In e l -> forall d, exists n, nth n l d = e /\ (n < length l)%nat.
Proof.
induction l; intros.
inversion H.
simpl in H.
destruct H.
subst.
exists O.
simpl.
auto with *.
elim IHl with d.
intros.
exists (S x).
simpl.
intuition.
trivial.
Qed.
End In.
Section Last.
Variable A : Type.
In x (y::nil) -> x = y.
Proof.
intros.
case H; intuition.
Qed.
Lemma in_nth:
forall e (l : list A),
In e l -> forall d, exists n, nth n l d = e /\ (n < length l)%nat.
Proof.
induction l; intros.
inversion H.
simpl in H.
destruct H.
subst.
exists O.
simpl.
auto with *.
elim IHl with d.
intros.
exists (S x).
simpl.
intuition.
trivial.
Qed.
End In.
Section Last.
Variable A : Type.
Last x l <-> x is the last element of list l.
Inductive Last (x:A) : list A -> Prop :=
| Last_base : Last x (x::nil)
| Last_step : forall (y:A) (l:list A), Last x l -> Last x (y::l).
| Last_base : Last x (x::nil)
| Last_step : forall (y:A) (l:list A), Last x l -> Last x (y::l).
The empty list nil has no last element.
If l is non-empty, the last element x of (y::l) is also the last element of l.
Lemma Last_step_inv : forall (x:A) (l:list A),
l <> nil -> forall y, Last x (y::l) -> Last x l.
Proof.
intros.
inversion H0.
rewrite H3 in H; elim H; reflexivity.
assumption.
Qed.
l <> nil -> forall y, Last x (y::l) -> Last x l.
Proof.
intros.
inversion H0.
rewrite H3 in H; elim H; reflexivity.
assumption.
Qed.
The last element x of l2 is also the last element of (l1 ++ l2).
Lemma Last_app : forall (x:A) (l1 l2:list A), Last x l2 -> Last x (l1 ++ l2).
Proof.
intros.
induction l1.
simpl; assumption.
change ((a :: l1) ++ l2) with (a :: (l1 ++ l2)).
apply Last_step; assumption.
Qed.
Proof.
intros.
induction l1.
simpl; assumption.
change ((a :: l1) ++ l2) with (a :: (l1 ++ l2)).
apply Last_step; assumption.
Qed.
If l is non-empty, the last element x of (l1 ++ l2) is also the last element of l2.
Lemma Last_app_inv : forall (x:A) (l1 l2:list A),
l2 <> nil -> Last x (l1 ++ l2) -> Last x l2.
Proof.
intros.
induction l1.
simpl; assumption.
apply IHl1.
apply Last_step_inv with (y := a).
destruct l1; [assumption | intuition; discriminate H1].
assumption.
Qed.
l2 <> nil -> Last x (l1 ++ l2) -> Last x l2.
Proof.
intros.
induction l1.
simpl; assumption.
apply IHl1.
apply Last_step_inv with (y := a).
destruct l1; [assumption | intuition; discriminate H1].
assumption.
Qed.
The last element Last x l of list l is element of the list l.
Theorem Last_In : forall (x:A) (l:list A),
Last x l -> In x l.
Proof.
intros.
elim H.
unfold In.
left; reflexivity.
intros y l0 L_x_l0 In_x_l0.
unfold In.
auto.
Qed.
Last x l -> In x l.
Proof.
intros.
elim H.
unfold In.
left; reflexivity.
intros y l0 L_x_l0 In_x_l0.
unfold In.
auto.
Qed.
Retrieve the last element x of l.
The result is either x together with a proof that x is the last element of l,
or l is the empty list.
Definition lastS (l:list A) : {x:A | Last x l}+{l=nil}.
Proof.
induction l.
right; reflexivity.
case_eq l.
left.
exists a.
apply Last_base.
left.
inversion IHl.
destruct X.
exists x.
rewrite <- H.
apply Last_step; assumption.
rewrite H in H0.
discriminate H0.
Defined.
End Last.
Implicit Arguments Last [A].
Implicit Arguments lastS [A].
Section Suffix.
Variable A : Type.
Proof.
induction l.
right; reflexivity.
case_eq l.
left.
exists a.
apply Last_base.
left.
inversion IHl.
destruct X.
exists x.
rewrite <- H.
apply Last_step; assumption.
rewrite H in H0.
discriminate H0.
Defined.
End Last.
Implicit Arguments Last [A].
Implicit Arguments lastS [A].
Section Suffix.
Variable A : Type.
Suffix s l <-> the list s is a suffix of the list l.
nil is a suffix of every list l.
l is a suffix of itself.
Lemma Suffix_l_l : forall l:list A, Suffix l l.
Proof.
intro l.
exists (nil (A:=A)); intuition.
Qed.
Proof.
intro l.
exists (nil (A:=A)); intuition.
Qed.
If s is a suffix of l, s is also a suffix of every list (x::l).
Lemma Suffix_step : forall (x:A) (s l:list A), Suffix s l -> Suffix s (x::l).
Proof.
intros x s l Hsuff.
unfold Suffix in * |- *.
elim Hsuff.
intros p Heq.
exists (x::p).
rewrite <- Heq.
reflexivity.
Qed.
Proof.
intros x s l Hsuff.
unfold Suffix in * |- *.
elim Hsuff.
intros p Heq.
exists (x::p).
rewrite <- Heq.
reflexivity.
Qed.
If s is a suffix of a list l, every element x that is an element of s is also an element of l.
Lemma Suffix_In : forall s l:list A, Suffix s l -> (forall x:A, In x s -> In x l).
Proof.
intros s l Hsuff x Hs.
elim Hsuff.
intros p Heq.
rewrite <- Heq.
intuition.
Qed.
Proof.
intros s l Hsuff x Hs.
elim Hsuff.
intros p Heq.
rewrite <- Heq.
intuition.
Qed.
For any two elements x and y in a list l,
it holds that either y is in a suffix (x::s) or
x is in a suffix (y::s).
Lemma Suffix_x_y_or_y_x : forall (l:list A) (x y:A),
In x l -> In y l ->
(exists s, Suffix (x::s) l /\ In y (x::s)) \/
(exists s, Suffix (y::s) l /\ In x (y::s)).
Proof.
intros.
induction l.
inversion H.
case H; intro Hax.
left.
exists l.
split.
rewrite Hax.
apply Suffix_l_l.
rewrite <- Hax; assumption.
case H0; intro Hay.
right.
exists l.
split.
rewrite Hay.
apply Suffix_l_l.
rewrite <- Hay; assumption.
change (In x l) in Hax.
change (In y l) in Hay.
generalize (IHl Hax Hay); intro H1.
case H1; intro.
left.
elim H2; intros.
exists x0.
destruct H3.
split.
apply Suffix_step; assumption.
assumption.
right.
elim H2; intros.
exists x0.
destruct H3.
split.
apply Suffix_step; assumption.
assumption.
Qed.
End Suffix.
Implicit Arguments Suffix [A].
In x l -> In y l ->
(exists s, Suffix (x::s) l /\ In y (x::s)) \/
(exists s, Suffix (y::s) l /\ In x (y::s)).
Proof.
intros.
induction l.
inversion H.
case H; intro Hax.
left.
exists l.
split.
rewrite Hax.
apply Suffix_l_l.
rewrite <- Hax; assumption.
case H0; intro Hay.
right.
exists l.
split.
rewrite Hay.
apply Suffix_l_l.
rewrite <- Hay; assumption.
change (In x l) in Hax.
change (In y l) in Hay.
generalize (IHl Hax Hay); intro H1.
case H1; intro.
left.
elim H2; intros.
exists x0.
destruct H3.
split.
apply Suffix_step; assumption.
assumption.
right.
elim H2; intros.
exists x0.
destruct H3.
split.
apply Suffix_step; assumption.
assumption.
Qed.
End Suffix.
Implicit Arguments Suffix [A].