(* * 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, 2006 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. Require Import Max. (* lemmas on beq_nat and negb *) 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. discriminate. discriminate. Qed. Lemma beq_nat_classic : forall a b, beq_nat a b = true \/ beq_nat a b =false. double induction a b; intros; simpl; auto. Qed. Lemma beq_nat_com: forall n m, beq_nat n m = beq_nat m n. double induction n m; simpl; auto. Qed. Lemma negb_false_is_true : forall x, negb x = false -> x = true. destruct x; auto. Qed. Lemma negb_true_is_false : forall x, negb x = true -> x = false. destruct x; auto. Qed. (* lemmas on Z *) Lemma Zeq_bool_classic : forall x y, Zeq_bool x y = true \/ Zeq_bool x y = false. intros; elim Zeq_bool; auto. Qed. Lemma Zeq_bool_refl : forall x, Zeq_bool x x = true. intros. unfold Zeq_bool. rewrite Zcompare_refl. auto. Qed. Lemma Zeq_bool_sym : forall x y, Zeq_bool x y = Zeq_bool y x. intros. unfold Zeq_bool. generalize (Ztrichotomy_inf x y); intro X; inversion_clear X. inversion_clear H. generalize (Ztrichotomy_inf y x); intro X; inversion_clear X. inversion_clear H. rewrite H0; rewrite H1; auto. subst x. generalize (Zlt_irrefl y); tauto. rewrite H0; rewrite H; auto. subst y. reflexivity. generalize (Ztrichotomy_inf y x); intro X; inversion_clear X. inversion_clear H0. rewrite H; rewrite H1; auto. subst y. generalize (Zlt_irrefl x); tauto. rewrite H0; rewrite H; 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. rewrite H. intro; discriminate. auto. rewrite H0. intro; discriminate. Qed. Lemma Zeq_bool_false : forall x y, Zeq_bool x y = false <-> x <> y. split; intros. generalize (Ztrichotomy_inf x y); intro X; inversion_clear X. inversion_clear H0. omega. subst x. rewrite Zeq_bool_refl in H; discriminate. omega. apply not_true_is_false. intro; apply H. apply Zeq_bool_true. assumption. Qed. Lemma Zeq_bool_false' : forall x y, Zeq_bool x y = false -> x <> y. intros. generalize (Zeq_bool_false x y); tauto. Qed. Lemma Zgt_bool_true : forall a b, Zgt_bool a b = true -> (a > b)%Z. intros. generalize (Z_gt_le_dec a b); intro X; inversion_clear X; auto. unfold Zgt_bool in H. red in H0. destruct (a ?= b)%Z; try discriminate||tauto. Qed. Lemma Zgt_bool_false: forall a b, Zgt_bool a b = false -> (a <= b)%Z. intros. generalize (Z_gt_le_dec a b); intro X; inversion_clear X; auto. unfold Zgt_bool in H. red in H0. destruct (a ?= b)%Z; try discriminate||tauto. Qed. Lemma Zle_neq_lt : forall n m, (n <= m)%Z -> (n <> m)%Z -> (n < m)%Z. intros. omega. Qed. Lemma Z_of_nat_Zpos_P_of_succ_nat : forall n, 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. Lemma Z_of_nat_le_inj': forall x y, x <= y -> (Z_of_nat x <= Z_of_nat y)%Z. intros. omega. Qed. Lemma Z_of_nat_le_inj: forall x y, (Z_of_nat x <= Z_of_nat y)%Z -> x <= y. intros. omega. Qed. Lemma Z_of_nat_lt_inj': forall x y, x < y -> (Z_of_nat x < Z_of_nat y)%Z. intros. omega. Qed. Lemma Z_of_nat_lt_inj: forall x y, (Z_of_nat x < Z_of_nat y)%Z -> x < y. intros. omega. Qed. Lemma Z_of_nat_ge_inj': forall x y, x >= y -> (Z_of_nat x >= Z_of_nat y)%Z. intros. omega. Qed. Lemma Z_of_nat_ge_inj: forall x y, (Z_of_nat x >= Z_of_nat y)%Z -> x >= y. intros. omega. Qed. Lemma Z_of_nat_gt_inj': forall x y, x > y -> (Z_of_nat x > Z_of_nat y)%Z. intros. omega. Qed. Lemma Z_of_nat_gt_inj: forall x y, (Z_of_nat x > Z_of_nat y)%Z -> x > y. intros. omega. Qed. Lemma nat_of_Z: forall z, (z >= 0)%Z -> exists n, z = Z_of_nat n. destruct z. intros. exists 0. auto. intros. exists (nat_of_P p). eapply Zpos_eq_Z_of_nat_o_nat_of_P. intros. generalize (Zlt_neg_0 p). intros. contradiction. Qed. (* lemmas about lists *) Lemma length_app : forall (A:Set) (l:list A) l', length (l++l') = 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 h1 h2, @inter A h h1 h2 -> inter h1 h h2. 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 S_to_plus_one. ring. Qed. Lemma list_last : forall (A:Set) (lst:list A), length lst > O -> 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 ). simpl. omega. generalize (IHlst H0); intro. inversion_clear H1. inversion_clear H2. exists (a::x). exists x0. simpl. rewrite H1. auto. Qed. (* * lemmas on nat *) Lemma mult_minus_distr_r : forall n m p, n >= m -> (n - m) * p = n * p - m * p. intuition. Qed. Lemma mult_minus_distr_l : forall n m p, m >= p -> n * (m - p) = n * m - n * p. intros. assert (n * (m - p) = (m - p) * n). intuition. rewrite H0. rewrite mult_minus_distr_r. intuition. intuition. Qed. (* * lemmas on max *) Lemma max_lemma1: forall x1 x2 x3, x1 >= x2 -> max x1 x3 >= max x2 x3. intros. generalize (max_dec x1 x3); intro X; inversion_clear X. generalize (max_dec x2 x3); intro X; inversion_clear X. rewrite H0; rewrite H1. auto. rewrite H0; rewrite H1. generalize (le_max_r x1 x3); intros. rewrite H0 in H2. omega. generalize (max_dec x2 x3); intro X; inversion_clear X. rewrite H0; rewrite H1. generalize (le_max_l x1 x3); intros. rewrite H0 in H2. omega. rewrite H0; rewrite H1. omega. Qed. Lemma max_lemma2: forall x1 x2 x3, x1 > max x2 x3 -> x1 > x2 /\ x1 > x3. intros. generalize (max_dec x2 x3); intro X; inversion_clear X. split. omega. generalize (le_max_r x2 x3); intros. omega. split. generalize (le_max_l x2 x3); intros. omega. omega. Qed. Lemma max_lemma3: forall x1 x2 x3, x1 > x2 /\ x1 > x3 -> x1 > max x2 x3. intros. inversion_clear H. generalize (max_dec x2 x3); intro X; inversion_clear X. omega. omega. Qed. Lemma max_lemma4: forall x y, max x y >= x. intros. generalize (le_max_l x y); auto. Qed. Lemma max_lemma5: forall x y z, z >= x -> max z y >= x. intros. generalize (le_max_l z y); omega. Qed. Lemma max_lemma6: forall x y z, z >= x -> max y z >= x. intros. generalize (le_max_r y z); omega. Qed. (* * definition of inequalities over naturals in bool (instead of Prop) *) Fixpoint nat_lt (n m:nat) {struct n} : bool := match n with 0 => match m with 0 => false | S m' => true end | S n' => match m with 0 => false | S m' => nat_lt n' m' end end. Definition nat_le (n m:nat) : bool := orb (beq_nat n m) (nat_lt n m). Fixpoint nat_gt (n m:nat) {struct n} : bool := match n with 0 => false | S n' => match m with 0 => true | S m' => nat_gt n' m' end end. Definition nat_ge (n m:nat) : bool := orb (beq_nat n m) (nat_gt n m). Lemma nat_lt_true: forall n m, nat_lt n m = true -> n < m. double induction n m. simpl; intro X; inversion X. intros. omega. simpl. intros. inversion H0. simpl; intros. cut (n1 < n0). omega. apply (H0 n0 H1). Qed. Lemma nat_lt_true': forall n m, n < m -> nat_lt n m = true. double induction n m. intro X; inversion X. intros. simpl. auto. simpl. intros. inversion H0. simpl; intros. assert (n1 < n0). omega. eapply H0; auto. Qed. Lemma nat_lt_false: forall n m, nat_lt n m = false -> n >= m. double induction n m. intuition. simpl; intros. inversion H0. simpl; intros. intuition. simpl; intros. cut (n1 >= n0). omega. apply H0; auto. Qed. Lemma nat_lt_false': forall n m, n >= m -> nat_lt n m = false. double induction n m. simpl; auto. simpl; intros. inversion H0. simpl; auto. simpl; intros. apply H0; omega. Qed. Lemma nat_lt_assym: forall n m, nat_lt n m = true -> nat_lt m n= false. intros. generalize (nat_lt_true _ _ H); intro. apply nat_lt_false'. intuition. Qed. Lemma nat_lt_irrefl: forall n , nat_lt n n = false. induction n. simpl; auto. simpl. auto. Qed. Lemma nat_lt_trans: forall n m p, nat_lt n m = true -> nat_lt m p = true -> nat_lt n p = true. intros. eapply nat_lt_true'. generalize (nat_lt_true _ _ H); intro. generalize (nat_lt_true _ _ H0); intro. intuition. Qed. Lemma nat_lt_classic: forall n m, nat_lt n m = true \/ nat_lt n m = false. intros. elim nat_lt; [left; auto | right; auto]. Qed. Ltac Contrad_lt := intros; Hyp_lt_clean; match goal with | id: ?a = ?b |- _ => subst a; Contrad_lt | id: ?a < ?a |- _ => generalize (lt_irrefl a); tauto | id1: ?b < ?a, id': ?a < ?b |- _ => generalize (lt_asym a b); tauto | id1: ?b < ?a, id': ?a < ?b' |- _ => generalize (lt_trans b a b' id1 id'); clear id'; intros; Contrad_lt | |- _ => tauto end with Hyp_lt_clean := match goal with | id: ?a = ?a |- _ => clear id; Hyp_lt_clean | id: ?a < ?b, id': ?a < ?b |- _ => clear id; Hyp_lt_clean | |- _ => idtac end.