Library Stack
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)
Require Import List.
Require Import Arith.
Require Import Min.
Require Import Classical.
Section definitions.
Set Implicit Arguments.
Variable A: Type.
Definition stack := list.
Definition empty (s : stack A) : bool :=
match s with
| nil => true
| _ => false
end.
Definition singleton (a : A) : stack A :=
a::nil.
Definition peek (s : stack A) : option A :=
match s with
| nil => None
| a::t => Some a
end.
Definition peekd (s : stack A) (d : A) : A :=
match s with
| nil => d
| a::t => a
end.
Definition push (a : A) (s : stack A) : stack A :=
a :: s.
Definition pop (s : stack A) : stack A :=
match s with
| nil => nil
| a::t => t
end.
Definition apply_top (f : A -> A) (s : stack A) : stack A :=
match s with
| nil => nil
| a :: t => f a :: t
end.
Definition replace_top (a : A) (s : stack A) : stack A :=
match s with
| nil => nil
| h :: t => a :: t
end.
Fixpoint truncate (n : nat) (s : stack A) : stack A :=
match nat_compare n (length s) with
| Lt =>
match s with
| _ :: t => truncate n t
| _ => nil
end
| _ => s
end.
Definition level (s t : stack A) : stack A * stack A :=
match nat_compare (length s) (length t) with
| Lt => (s , truncate (length s) t)
| Eq => (s, t)
| Gt => (truncate (length t) s, t)
end.
End definitions.
Notation "│ s │" := (length s).
Notation "[]" := (nil).
Section proofs.
Set I
mplicit Arguments.
Variable A B : Type.
Lemma nat_compare_n_Sn : forall n,
nat_compare n (S n) = Lt.
Proof.
intuition.
rewrite <- nat_compare_lt.
auto.
Qed.
Lemma nat_compare_Sn_n : forall n,
nat_compare (S n) n = Gt.
Proof.
intuition.
rewrite <- nat_compare_gt.
auto.
Qed.
Lemma nat_compare_Eq:
forall n m,
nat_compare n m = Eq <-> n = m.
Proof.
induction n.
split; intros.
apply nat_compare_eq; trivial.
unfold nat_compare.
destruct m; trivial.
discriminate H.
intros.
split.
intros.
apply nat_compare_eq; trivial.
intros.
destruct m.
discriminate H.
inversion H.
generalize H1; intro.
apply IHn in H1.
unfold nat_compare.
subst.
destruct m; trivial.
Qed.
Lemma nat_compare_n_n:
forall n,
nat_compare n n = Eq.
Proof.
intros.
rewrite nat_compare_Eq.
trivial.
Qed.
Lemma lt_gt: forall n m, n < m <-> m > n. Proof. split; trivial. Qed.
Lemma le_ge: forall n m , n <= m <-> m>=n. Proof. split;trivial. Qed.
Lemma nat_compare_lt_gt_sym:
forall n m, nat_compare n m = Lt <-> nat_compare m n = Gt.
Proof.
intros;split;intros.
apply nat_compare_lt in H.
rewrite lt_gt in H.
rewrite <- nat_compare_gt;trivial.
apply nat_compare_gt in H.
rewrite <- lt_gt in H.
rewrite <- nat_compare_lt;trivial.
Qed.
Lemma nat_compare_eq_sym:
forall n m, nat_compare n m = Eq <-> nat_compare m n = Eq.
Proof.
intros;split;intros;rewrite nat_compare_Eq;rewrite nat_compare_Eq in H;symmetry;trivial.
Qed.
Lemma truncate_1:
forall n (s : stack A),
n <= length s ->
n = length ( truncate n s).
Proof.
intros.
unfold truncate in |- *.
induction s.
simpl in *.
assert (n = 0) by complete auto with arith.
destruct nat_compare; trivial.
case_eq (nat_compare n (length (a :: s))); intro.
apply nat_compare_Eq in H0; trivial.
apply IHs.
clear IHs.
apply nat_compare_lt in H0.
unfold length in H0.
auto with *.
apply nat_compare_gt in H0.
apply le_not_lt in H.
elim H.
trivial.
Qed.
Lemma truncate_nil:
forall (s : stack A),
truncate 0 s = nil.
Proof.
intros.
induction s.
unfold truncate.
unfold nat_compare;trivial.
unfold truncate.
replace (nat_compare 0 (length (a::s))) with Lt by trivial.
trivial.
Qed.
Lemma map_truncate:
forall (f : A -> B) n (s : stack A),
map f (truncate n s) = truncate n (map f s).
Proof.
intros.
induction s.
unfold truncate in |- *.
simpl in |- *.
unfold map in |- *.
destruct nat_compare; trivial.
unfold truncate in |- *.
case_eq (nat_compare n (length (map f (a :: s)))); intro.
generalize H; intro.
rewrite map_length in H0.
unfold map at 2 in |- *.
unfold map in H.
rewrite H in |- *.
rewrite H0 in |- *.
trivial.
generalize H; intro.
rewrite map_length in H0.
unfold map at 2 in |- *.
unfold map in H.
rewrite H in |- *.
rewrite H0 in |- *.
assumption.
generalize H; intro.
rewrite map_length in H0.
unfold map at 2 in |- *.
unfold map in H.
rewrite H in |- *.
rewrite H0 in |- *.
trivial.
Qed.
Lemma level_eq:
forall (s t : stack A),
(s, t) = level s t
<->
length s = length t.
Proof.
intros.
split; intro.
unfold level in H.
case_eq (nat_compare (length s) (length t)); intro.
apply nat_compare_Eq in H0; trivial.
rewrite H0 in H.
inversion H.
apply truncate_1.
apply nat_compare_lt in H0.
auto with *.
rewrite H0 in H.
inversion H.
symmetry in |- *.
apply truncate_1.
apply nat_compare_gt in H0.
progress auto with *.
unfold level in |- *.
replace (nat_compare (length s) (length t)) with Eq ; trivial.
symmetry in |- *; rewrite nat_compare_Eq in |- *; trivial.
Qed.
Lemma level_le:
forall (s t : stack A),
(s, truncate (length s) t) = level s t
<->
length s <= length t.
Proof.
split;intros.
unfold level in H.
case_eq (nat_compare (length s) (length t));intros.
apply nat_compare_Eq in H0.
rewrite H0.
trivial.
apply nat_compare_lt in H0.
auto with *.
assert (truncate (length s) t = t).
unfold truncate.
destruct t.
destruct nat_compare;trivial.
rewrite H0.
trivial.
rewrite H1 in H.
rewrite H0 in H.
inversion H.
generalize truncate_1.
intro.
specialize H2 with (length t) s.
apply nat_compare_lt_gt_sym in H0.
apply nat_compare_lt in H0.
assert ((length t) <= (length s)).
auto with *.
apply H2 in H4.
rewrite <- H4.
trivial.
unfold level.
case_eq(nat_compare (length s) (length t));intros.
unfold truncate.
destruct t.
destruct nat_compare;trivial.
rewrite H0;trivial.
trivial.
apply nat_compare_le in H.
elim H;trivial.
Qed.
Lemma level_ge:
forall (s t : stack A),
(truncate (length t) s, t) = level s t
<->
length t <= length s.
Proof.
split;intros.
unfold level in H.
case_eq (nat_compare (length t) (length s));intros.
apply nat_compare_Eq in H0.
rewrite H0.
trivial.
apply nat_compare_lt in H0.
auto with *.
assert (truncate (length t) s = s).
unfold truncate.
destruct s.
simpl.
destruct (nat_compare (length t) 0);trivial.
rewrite H0.
trivial.
rewrite H1 in H.
apply nat_compare_lt_gt_sym in H0.
rewrite H0 in H.
inversion H.
generalize truncate_1.
intro.
specialize H2 with (length s) t.
apply nat_compare_lt_gt_sym in H0.
apply nat_compare_gt in H0.
assert ((length s) <= (length t)).
auto with *.
apply H2 in H4.
rewrite <- H4.
trivial.
unfold level.
case_eq(nat_compare (length s) (length t));intros.
unfold truncate.
destruct s.
simpl.
destruct (nat_compare (length t) 0);trivial.
apply nat_compare_eq_sym in H0.
rewrite H0;trivial.
apply nat_compare_ge in H.
elim H;trivial.
trivial.
Qed.
Lemma level_1:
forall (s s' t t' : stack A),
(s', t') = level s t ->
length s' = length t'.
Proof.
intros.
unfold level in H.
case_eq (nat_compare (length s) (length t));intros;rewrite H0 in H.
apply nat_compare_Eq in H0.
inversion H.
trivial.
inversion H;subst.
apply truncate_1.
apply nat_compare_lt in H0.
auto with *.
inversion H;subst.
symmetry.
apply truncate_1.
apply nat_compare_gt in H0.
auto with *.
Qed.
Lemma truncate_pop:
forall n (s : stack A),
length s = (S n) ->
truncate n s = pop s.
Proof.
intros.
unfold truncate in |- *.
destruct s.
destruct nat_compare; trivial.
rewrite H in |- *.
rewrite nat_compare_n_Sn in |- *.
unfold pop in |- *.
assert (length s = n).
unfold length in H.
apply eq_add_S.
trivial.
destruct s.
destruct nat_compare; trivial.
rewrite H0 in |- *.
replace (nat_compare n n) with Eq .
trivial.
symmetry.
rewrite nat_compare_Eq.
trivial.
Qed.
Lemma truncate_same:
forall (s : stack A),
truncate (length s) s = s.
Proof.
intros.
unfold truncate.
destruct s.
destruct nat_compare;trivial.
rewrite nat_compare_n_n.
trivial.
Qed.
Lemma truncate_n_nil:
forall n,
truncate n nil = nil (A := A).
Proof.
intros. unfold truncate.
destruct nat_compare;trivial.
Qed.
Lemma truncate_truncate:
forall n m (s : stack A),
n <= m ->
truncate n s = truncate n (truncate m s).
Proof.
induction s.
intuition.
repeat rewrite truncate_n_nil;trivial.
intros.
generalize H.
intros.
apply IHs in H0.
unfold truncate.
case_eq (nat_compare m (length (a::s))).
case_eq (nat_compare n (length (a::s))).
trivial.
trivial.
trivial.
unfold truncate in H0.
rewrite <- H0.
clear H0.
intros.
case_eq (nat_compare n (length (a::s))).
intuition.
apply nat_compare_lt in H0.
apply nat_compare_Eq in H1.
subst.
apply le_not_lt in H.
elim H;trivial.
trivial.
intuition.
apply nat_compare_lt in H0.
apply nat_compare_gt in H1.
assert (m < n).
apply lt_gt in H1.
apply lt_trans with (length (a::s));trivial.
apply le_not_lt in H.
elim H;trivial.
trivial.
Qed.
End proofs.