Commit 8eba8490 by MARCHE Claude

linked list reversal: replaced the old version by the new one

parent 58366e69
 (* In-place linked list reversal. (** {1 In-place linked list reversal } Version designed for the MPRI lecture http://www.lri.fr/~marche/MPRI-2-36-1/ Version designed for the {h MPRI lecture ``Proof of Programs''} This is an improved version of {h this one}: it does not use any Coq proofs, but lemma functions instead. *) theory ListReverse module Disjoint use export int.Int use export list.List function head (l: list 'a) : 'a axiom head_cons: forall x:'a, l:list 'a. head (Cons x l) = x function tail (l: list 'a) : list 'a axiom tail_cons: forall x:'a, l:list 'a. tail (Cons x l) = l use export list.Mem use export list.Append use export list.Length use export list.Reverse predicate disjoint (l1:list 'a) (l2:list 'a) = forall x:'a. not (mem x l1 /\ mem x l2) ... ... @@ -28,70 +30,151 @@ theory ListReverse | Cons x r -> not (mem x r) /\ no_repet r end use export list.Append use export list.Reverse let rec ghost mem_decomp (x: 'a) (l: list 'a) : (list 'a, list 'a) requires { mem x l } variant { l } returns { (l1,l2) -> l = l1 ++ Cons x l2 } = match l with | Nil -> absurd | Cons h t -> if h = x then (Nil,t) else let (r1,r2) = mem_decomp x t in (Cons h r1,r2) end end module InPlaceRev use import ListReverse use import Disjoint use import map.Map use import ref.Ref type loc function null:loc val acc(field: ref (map loc 'a)) (l:loc) : 'a requires { l <> null } reads { field } ensures { result = get !field l } val upd(field: ref (map loc 'a)) (l:loc) (v:'a):unit requires { l <> null } writes { field } ensures { !field = set (old !field) l v } inductive list_seg loc (map loc loc) (list loc) loc = | list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p | list_seg_cons: forall p q:loc, next:map loc loc, l:list loc. p <> null /\ list_seg (get next p) next l q -> list_seg p next (Cons p l) q lemma list_seg_frame: forall next1 next2:map loc loc, p q v: loc, pM:list loc. list_seg p next1 pM null /\ next2 = set next1 q v /\ not (mem q pM) -> list_seg p next2 pM null let rec lemma list_seg_frame_ext (next1 next2:map loc loc) (p q r v: loc) (pM:list loc) requires { list_seg p next1 pM r } requires { next2 = set next1 q v } requires { not (mem q pM) } variant { pM } ensures { list_seg p next2 pM r } = match pM with | Nil -> () | Cons h t -> assert { p = h }; list_seg_frame_ext next1 next2 (get next1 p) q r v t end lemma list_seg_functional: forall next:map loc loc, l1 l2:list loc, p: loc. list_seg p next l1 null /\ list_seg p next l2 null -> l1 = l2 let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc) requires { list_seg p next l1 null } requires { list_seg p next l2 null } variant { l1 } ensures { l1 = l2 } = match l1,l2 with | Nil, Nil -> () | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p) | _ -> absurd end lemma list_seg_sublistl: forall next:map loc loc, l1 l2:list loc, p q: loc. list_seg p next (l1++Cons q l2) null -> list_seg q next (Cons q l2) null let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc) requires { list_seg p next (l1 ++ Cons q l2) null } variant { l1 } ensures { list_seg q next (Cons q l2) null } = match l1 with | Nil -> () | Cons _ r -> list_seg_sublistl next r l2 (get next p) q end lemma list_seg_no_repet: forall next:map loc loc, pM:list loc, p: loc. list_seg p next pM null -> no_repet pM let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc) requires { list_seg p next pM null } variant { pM } ensures { no_repet pM } = match pM with | Nil -> () | Cons h t -> if mem h t then (* absurd case *) let (l1,l2) = mem_decomp h t in list_seg_sublistl next (Cons h l1) l2 p h; list_seg_functional next pM (Cons h l2) p; assert { length pM > length (Cons h l2) } else list_seg_no_repet next (get next p) t end use import ref.Ref let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc) requires { list_seg p next pM q } requires { list_seg q next qM r } variant { pM } ensures { list_seg p next (pM ++ qM) r } = match pM with | Nil -> () | Cons _ t -> list_seg_append next (get next p) q r t qM end val next : ref (map loc loc) let in_place_reverse (l:loc) (ghost lM:list loc) : loc requires { list_seg l !next lM null } ensures { list_seg result !next (reverse lM) null } = 'Init: let p = ref l in let ghost pM = ref lM in let r = ref null in let ghost rM = ref (Nil : list loc) in while !p <> null do let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc requires { list_seg l1 !next l1M null } requires { list_seg l2 !next l2M null } requires { disjoint l1M l2M } ensures { list_seg result !next (l1M ++ l2M) null } = if l1 = null then l2 else let p = ref l1 in let ghost pM = ref l1M in let ghost l1pM = ref (Nil : list loc) in while acc next !p <> null do invariant { !p <> null } invariant { list_seg l1 !next !l1pM !p } invariant { list_seg !p !next !pM null } invariant { list_seg !r !next !rM null } invariant { disjoint !pM !rM } invariant { (reverse !pM) ++ !rM = reverse lM } invariant { !l1pM ++ !pM = l1M } invariant { disjoint !l1pM !pM } variant { !pM } let n = get !next !p in next := set !next !p !r; assert { list_seg !r !next !rM null }; r := !p; p := n; rM := Cons (head !pM) !rM; pM := tail !pM match !pM with | Nil -> absurd | Cons _ t -> l1pM := !l1pM ++ Cons !p Nil; pM := t end; p := acc next !p done; !r upd next !p l2; assert { list_seg l1 !next !l1pM !p }; assert { list_seg !p !next (Cons !p Nil) l2 }; assert { list_seg l2 !next l2M null }; l1 end (* Local Variables: compile-command: "why3 ide linked_list_rev.mlw" End: *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. Parameter head: forall {a:Type} {a_WT:WhyType a}, (list a) -> a. Axiom head_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((head (Cons x l)) = x). Parameter tail: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a). Axiom tail_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((tail (Cons x l)) = l). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. (* Why3 assumption *) Definition disjoint {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)): Prop := forall (x:a), ~ ((mem x l1) /\ (mem x l2)). (* Why3 assumption *) Fixpoint no_repet {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Prop := match l with | Nil => True | (Cons x r) => (~ (mem x r)) /\ (no_repet r) end. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). (* Why3 assumption *) Fixpoint reverse {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil :(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil :(list a)))) end. Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length (reverse l)) = (length l)). Axiom loc : Type. Parameter loc_WhyType : WhyType loc. Existing Instance loc_WhyType. Parameter null: loc. (* Why3 assumption *) Inductive list_seg : loc -> (map.Map.map loc loc) -> (list loc) -> loc -> Prop := | list_seg_nil : forall (p:loc) (next:(map.Map.map loc loc)), (list_seg p next (Nil :(list loc)) p) | list_seg_cons : forall (p:loc) (q:loc) (next:(map.Map.map loc loc)) (l:(list loc)), ((~ (p = null)) /\ (list_seg (map.Map.get next p) next l q)) -> (list_seg p next (Cons p l) q). (* Why3 goal *) Theorem list_seg_frame : forall (next1:(map.Map.map loc loc)) (next2:(map.Map.map loc loc)) (p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\ ((next2 = (map.Map.set next1 q v)) /\ ~ (mem q pM))) -> (list_seg p next2 pM null). Proof. intros until pM. generalize p; clear p. elim pM. (* case pM = Nil *) intros p (h1&h2&h3). inversion h1; subst; clear h1. constructor. (* case pM = Cons a l *) intros a l Hind p (h1&h2&h3). inversion h1; subst; clear h1. destruct H4. constructor; split; auto. simpl in h3. rewrite Map.Select_neq; auto. apply Hind; split; auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. Parameter head: forall {a:Type} {a_WT:WhyType a}, (list a) -> a. Axiom head_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((head (Cons x l)) = x). Parameter tail: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a). Axiom tail_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((tail (Cons x l)) = l). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. (* Why3 assumption *) Definition disjoint {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)): Prop := forall (x:a), ~ ((mem x l1) /\ (mem x l2)). (* Why3 assumption *) Fixpoint no_repet {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Prop := match l with | Nil => True | (Cons x r) => (~ (mem x r)) /\ (no_repet r) end. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). (* Why3 assumption *) Fixpoint reverse {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: (list a) := match l with | Nil => (Nil :(list a)) | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil :(list a)))) end. Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) l2) = (infix_plpl (reverse l1) (Cons x l2))). Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((reverse (reverse l)) = l). Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length (reverse l)) = (length l)). Axiom loc : Type. Parameter loc_WhyType : WhyType loc. Existing Instance loc_WhyType. Parameter null: loc. (* Why3 assumption *) Inductive list_seg : loc -> (map.Map.map loc loc) -> (list loc) -> loc -> Prop := | list_seg_nil : forall (p:loc) (next:(map.Map.map loc loc)), (list_seg p next (Nil :(list loc)) p) | list_seg_cons : forall (p:loc) (q:loc) (next:(map.Map.map loc loc)) (l:(list loc)), ((~ (p = null)) /\ (list_seg (map.Map.get next p) next l q)) -> (list_seg p next (Cons p l) q). Axiom list_seg_frame : forall (next1:(map.Map.map loc loc)) (next2:(map.Map.map loc loc)) (p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\ ((next2 = (map.Map.set next1 q v)) /\ ~ (mem q pM))) -> (list_seg p next2 pM null). (* Why3 goal *) Theorem list_seg_functional : forall (next:(map.Map.map loc loc)) (l1:(list loc)) (l2:(list loc)) (p:loc), ((list_seg p next l1 null) /\ (list_seg p next l2 null)) -> (l1 = l2). Proof. induction l1. intros l2 p (h1,h2). inversion h1; subst; clear h1. inversion h2; subst; clear h2; intuition. intros l2 p (h1,h2). inversion h1; subst; clear h1. inversion h2; subst; clear h2; intuition. apply f_equal. apply IHl1 with (p := Map.get next a); auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require list.List. Require list.Length. Require list.Mem. Require map.Map. Require list.Append. Require list.Reverse. (* Why3 assumption *) Definition unit := unit. Parameter head: forall {a:Type} {a_WT:WhyType a}, (list a) -> a. Axiom head_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((head (cons x l)) = x). Parameter tail: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a). Axiom tail_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), ((tail (cons x l)) = l). (* Why3 assumption *) Definition disjoint {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list a)): Prop := forall (x:a), ~ ((list.Mem.mem x l1) /\ (list.Mem.mem x l2)). (* Why3 assumption *) Fixpoint no_repet {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Prop := match l with | nil => True | (cons x r) => (~ (list.Mem.mem x r)) /\ (no_repet r) end. Axiom loc : Type. Parameter loc_WhyType : WhyType loc. Existing Instance loc_WhyType. Parameter null: loc. (* Why3 assumption *) Inductive list_seg : loc -> (@map.Map.map loc loc_WhyType loc loc_WhyType) -> (list loc) -> loc -> Prop := | list_seg_nil : forall (p:loc) (next:(@map.Map.map loc loc_WhyType loc loc_WhyType)), (list_seg p next nil p) | list_seg_cons : forall (p:loc) (q:loc) (next:(@map.Map.map loc loc_WhyType loc loc_WhyType)) (l:(list loc)), ((~ (p = null)) /\ (list_seg (map.Map.get next p) next l q)) -> (list_seg p next (cons p l) q). Axiom list_seg_frame : forall (next1:(@map.Map.map loc loc_WhyType loc loc_WhyType)) (next2:(@map.Map.map loc loc_WhyType loc loc_WhyType)) (p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\ ((next2 = (map.Map.set next1 q v)) /\ ~ (list.Mem.mem q pM))) -> (list_seg p next2 pM null).