(* * Seplog is an implementation of separation logic (an extension of Hoare * logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the * Coq proof assistant (version 8, http://coq.inria.fr) together with a * sample verification of the heap manager of the Topsy operating system * (version 2, http://www.topsy.net). More information is available at * http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog. * * Copyright (c) 2005 Reynald Affeldt and Nicolas Marti * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA *) Require Import EqNat. Require Import Bool. Require Import ZArith. Require Import List. Require Import Classical. (* lemmas on booleans and integers *) Lemma beq_dif_false : forall n m, n <> m -> beq_nat n m = false. double induction n m; try tauto. simpl; intuition. Qed. Lemma beq_nat_false : forall a b, beq_nat a b = false -> a <> b. double induction a b; simpl; auto. intro X; discriminate X. Qed. Lemma beq_nat_true: forall x y, beq_nat x y = true -> x=y. double induction x y. intros; auto. intros. simpl in H0. inversion H0. intros. simpl in H0. inversion H0. intros. simpl in H1. generalize (H0 n H1); intro. rewrite H2. auto. Qed. Lemma beq_nat_classic : forall a b, (beq_nat a b)=true \/ (beq_nat a b)=false. double induction a b; auto. intros. generalize (H n0 H0); intro. simpl. auto. Qed. Lemma negb_false_is_true : forall x, negb x = false -> x = true. intro; case x; simpl; auto. Qed. Lemma negb_true_is_false : forall x, negb x = true -> x = false. intro; case x; simpl; auto. Qed. (* lemmas on integers *) Lemma Zeq_bool_classic: forall x y, Zeq_bool x y = true \/ Zeq_bool x y = false. intros. elim Zeq_bool. left; auto. right; auto. Qed. Lemma Zeq_bool_refl : forall x, (Zeq_bool x x)=true. intro; induction x. ring. unfold Zeq_bool. rewrite (Zcompare_refl (Zpos p)). auto. unfold Zeq_bool. rewrite (Zcompare_refl (Zneg p)). auto. Qed. Lemma Zeq_bool_false : forall x y, (Zeq_bool x y)=false <-> x<>y. do 2 intro. split. generalize (Ztrichotomy_inf x y); intro X; inversion_clear X. inversion_clear H. omega. rewrite H0. rewrite Zeq_bool_refl. intro X; discriminate X. omega. generalize (Ztrichotomy_inf x y); intro X; inversion_clear X. inversion_clear H. unfold Zeq_bool. inversion H0. rewrite H1. auto. rewrite H0. intro X; generalize (X (refl_equal y)); contradiction. inversion H. unfold Zeq_bool. rewrite H1. auto. Qed. Lemma Zeq_bool_true : forall x y, (Zeq_bool x y)=true -> x=y. unfold Zeq_bool. intros x y. generalize (Ztrichotomy_inf x y); intro. inversion_clear H. inversion_clear H0. inversion H. rewrite H1. intro X; discriminate X. elim H; auto. inversion H0. rewrite H1. intro X; discriminate X. Qed. Lemma Z_of_nat_Zpos_P_of_succ_nat : forall (n:nat), Z_of_nat (n + 1) = Zpos (P_of_succ_nat n). intro. unfold Z_of_nat. destruct n. simpl. auto. simpl. generalize (nat_of_P_o_P_of_succ_nat_eq_succ n); intro. assert ((n + 1)%nat = (S n)). omega. rewrite H0. rewrite <-H. rewrite P_of_succ_nat_o_nat_of_P_eq_succ. auto. Qed. Lemma Z_of_nat_inj : forall x y, Z_of_nat x = Z_of_nat y -> x = y. induction x. induction y; auto. simpl; intro X; discriminate X. induction y. simpl; intro X; discriminate X. intros. simpl in H. injection H; intro. rewrite <-nat_of_P_o_P_of_succ_nat_eq_succ. rewrite <-nat_of_P_o_P_of_succ_nat_eq_succ. rewrite H0. auto. Qed. Lemma Z_of_nat_inj': (forall x y, x = y -> Z_of_nat x = Z_of_nat y). auto. Qed. (* lemmas about lists *) Lemma length_app : forall (A:Set) (l:(list A)) l', (length (l++l'))=(plus (length l) (length l')). induction l. simpl; auto. simpl. intro l'; rewrite (IHl l'); auto. Qed. Lemma incl_nil : forall (A:Set) (h:(list A)), incl h nil -> h=nil. induction h; auto. simpl; intros. red in H. assert (In a nil); [apply H; simpl; auto | idtac]. simpl in H0; contradiction. Qed. Definition inter (A:Set) h1 h2 h := forall x:A, In x h1 /\ In x h2 <-> In x h. Implicit Arguments inter. Lemma inter_nil: forall (A:Set) l, @inter A l nil nil. unfold inter; unfold In. tauto. Qed. Implicit Arguments inter_nil. Lemma inter_weak : forall (A:Set) x L K M, @inter A K L M -> ~ In x K -> inter K (x :: L) M. intros. unfold inter. split; intros. elim (classic (x = x0)); intros. subst x0. generalize (H0 (proj1 H1)); contradiction. assert (In x0 L). inversion_clear H1. inversion H4. contradiction. auto. generalize (H x0); intuition; tauto. generalize (H x0); intro X; inversion_clear X. split; intuition. Qed. Implicit Arguments inter_weak. Lemma inter_sym: forall (A:Set) h h' h'', @inter A h h' h'' -> inter h' h h''. intros. red. intros. generalize (H x). tauto. Qed. Implicit Arguments inter_sym. Lemma inter_nil_subset : forall (A:Set) (l:(list A)) l', (inter l l' nil) -> forall l'', (incl l'' l) -> (inter l'' l' nil). intros. red. intros. split. intros. inversion_clear H1. red in H. generalize (H x); intro. inversion_clear H1. apply H4. split; auto. contradiction. Qed. Lemma inter_app : forall (A:Set) (l k m:(list A)), (inter (l++k) m nil) -> (inter l m nil) /\ (inter k m nil). intros. red in H. split. split; intros. assert (In x (l++k)). apply in_or_app. intuition. generalize (H x); tauto. contradiction. split; intros. assert (In x (l++k)). apply in_or_app. intuition. generalize (H x); tauto. contradiction. Qed. Lemma inter_stren : forall (A:Set) (hd1:A) tl1 l2, inter (hd1::tl1) l2 nil -> inter tl1 l2 nil. intros. red; split; intros. red in H. generalize (H x); intro. inversion_clear H1. apply H2; split. simpl; intuition. intuition. simpl in H0; tauto. Qed. Implicit Arguments inter_stren. Lemma list_split : forall (A:Set) (l:list A) x, In x l -> exists l1, exists l2, l = l1 ++ (x::nil) ++ l2. induction l. simpl. intuition. intros. simpl. simpl in H. inversion_clear H. subst a. exists (@nil A). exists l. auto. generalize (IHl _ H0). simpl. intros. inversion_clear H. inversion_clear H1. exists (a::x0); exists x1. simpl. rewrite H. auto. Qed. (* permutations and accompanying lemmas *) Set Implicit Arguments. Inductive permut (A:Set) : (list A) -> (list A) -> Prop := permut_refl: forall h, permut h h | permut_cons: forall a l0 l1, permut l0 l1 -> permut (a::l0) (a::l1) | permut_append: forall a l, permut (a::l) (l ++ a::nil) | permut_trans: forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. Lemma permut_sym : forall (A:Set) (h1 h2 : (list A)), permut h1 h2 -> permut h2 h1. intros. induction H. apply permut_refl. apply permut_cons. auto. generalize a; clear a. induction l. simpl. intro. apply permut_refl. simpl. intros. assert (permut (a::l ++ a0::nil) (a::a0::l)). apply permut_cons; auto. apply permut_trans with (a::a0::l); auto. apply permut_trans with (a0::(l ++ (a::nil))). apply permut_append with (a:=a) (l:=(a0::l)). apply permut_cons. apply IHl. apply permut_trans with l1; auto. Qed. Lemma permut_nil' : forall (A:Set) (k k':(list A)), permut k k' -> k'=nil -> k=nil. do 4 intro. induction H; auto. intro X; discriminate X. intro X. destruct l. discriminate X. discriminate X. Qed. Lemma permut_nil : forall (A:Set) (k:(list A)), permut k nil -> k=nil. intros. eapply permut_nil'. apply H. auto. Qed. Lemma In_permut : forall (A:Set) (h h':(list A)), permut h' h -> forall x, In x h -> In x h'. do 4 intro. induction H. auto. intros. simpl; simpl in H0. inversion_clear H0; auto. simpl. intros. generalize (in_app_or _ _ _ H); intros. inversion_clear H0; auto. simpl in H1. inversion_clear H1; auto. contradiction. auto. Qed. Lemma permut_head : forall (A:Set) h (a b:A), permut (a::b::h) (b::a::h). intros. apply permut_trans with ((a::h) ++ b::nil). simpl. apply permut_cons. apply permut_append. apply permut_sym. apply permut_append with (l:=a::h) (a:=b). Qed. Lemma rotate_is_permut : forall (A:Set) k (a:A), (permut (a::k) (k++a::nil)). induction k. simpl; intros; apply permut_refl. intros. simpl. apply permut_trans with (a::a0::k). apply permut_head. apply permut_cons. auto. Qed. Lemma permut_inter : forall (A:Set) (k m:(list A)), permut k m -> forall n p, inter n m p -> inter n k p. do 4 intro. induction H. auto. intros. red. intro. generalize (H0 x); intro X; inversion_clear X. split; intros. apply H1. inversion_clear H3. split; auto. simpl in H5. inversion_clear H5. subst x. simpl; auto. simpl. right. apply In_permut with l0; auto. apply permut_sym; auto. generalize (H2 H3); intro X; inversion_clear X. split; auto. simpl in H5; inversion_clear H5. subst x. simpl; auto. simpl; right. apply In_permut with l1; auto. intros. red; intro. generalize (H x); intro X; inversion_clear X. split; intros. apply H0. inversion_clear H2. split; auto. simpl in H4; inversion_clear H4. subst x. apply In_permut with (a::l). apply permut_sym. apply rotate_is_permut. simpl; auto. apply in_or_app; auto. generalize (H1 H2); intro X; inversion_clear X. generalize (in_app_or _ _ _ H4); intro X; inversion_clear X. simpl; auto. simpl in H5; inversion_clear H5. subst x; simpl; auto. contradiction. auto. Qed. Ltac Permut n := match goal with | |- (permut ?X1 ?X1) => apply permut_refl | |- (permut (?X1 :: ?X2) (?X1 :: ?X3)) => let newn := eval compute in (length X2) in (apply permut_cons; Permut newn) | |- (permut (?X1 :: ?X2) ?X3) => match eval compute in n with | 1 => fail | _ => let l0' := constr:(X2 ++ X1 :: nil) in (apply (@permut_trans _ (X1 :: X2) l0' X3); [ apply permut_append | compute; Permut (pred n) ]) end end. Ltac PermutProve := match goal with | |- (permut ?X1 ?X2) => match eval compute in (length X1 = length X2) with | (?X1 = ?X1) => Permut X1 end end. Lemma permut_inv_head : forall (A:Set) (L : (list A)) (c d : A), permut (c :: d :: L) (d :: c :: L). intros. apply permut_trans with (l1 := (c :: L) ++ d :: nil). simpl. apply permut_cons. apply permut_append. apply permut_sym. apply permut_append with (l := c :: L) (a := d). Qed. Lemma permut_app_com : forall (A:Set) (L K:(list A)), permut (L ++ K) (K ++ L). intro. induction L. intro. simpl. rewrite <- app_nil_end. apply permut_refl. intro. generalize (IHL (a :: K)); intro. simpl. simpl in H. apply permut_trans with (l1 := a :: K ++ L). apply permut_cons. apply IHL. induction K. simpl. apply permut_refl. simpl. apply permut_trans with (l1 := a0 :: a :: K ++ L). apply permut_inv_head. apply permut_cons. apply IHK. generalize (IHL (a :: K)); intro. simpl in H0. auto. Qed. Unset Implicit Arguments. Definition length_rev : forall (A:Set) (l:(list A)), length (rev l) = length l. induction l; auto. simpl. rewrite length_app. simpl. rewrite IHl. rewrite <-plus_n_Sm. assert (forall n:nat, (n + O)%nat = n). induction n; auto. rewrite (H (length l)). auto. Defined. Lemma list_last : forall (A:Set) (lst:list A), (length lst > O)%nat -> exists lst', exists a, lst = lst' ++ a::nil. induction lst. simpl. intros. inversion H. intros. destruct lst. exists (@nil A). exists a. auto. assert ( (length (a0::lst) > 0)%nat ). simpl. omega. generalize (IHlst H0); intro. inversion_clear H1. inversion_clear H2. exists (a::x). exists x0. simpl. rewrite H1. auto. Qed.