diff --git a/examples/programs/flag.mlw b/examples/programs/flag.mlw index 9101b1791f87b43a5f3a93a14e6107f92373d128..2aac29187fdb1801ff98e35d719997f48e61b1e1 100644 --- a/examples/programs/flag.mlw +++ b/examples/programs/flag.mlw @@ -19,7 +19,7 @@ module Flag a[i] <- a[j]; a[j] <- v end - { exchange a (old a) i j } + { exchange (old a) a i j } let dutch_flag (a:array color) (n:int) = { 0 <= n /\ length a = n } @@ -33,7 +33,7 @@ module Flag monochrome a !b !i White /\ monochrome a !r n Red /\ length a = n /\ - permut_sub a (at a 'Init) 0 n } + permut_sub (at a 'Init) a 0 n } variant { !r - !i } match a[!i] with | Blue -> @@ -51,7 +51,7 @@ module Flag monochrome a 0 b Blue /\ monochrome a b r White /\ monochrome a r n Red) - /\ permut a (old a) } + /\ permut (old a) a } end diff --git a/examples/programs/flag/why3session.xml b/examples/programs/flag/why3session.xml index 9e5d70e13a831dc3a39712f15f49f42e9ac5526c..6b52c87c9797e93ce24134b5a9cdfb2bb68b363b 100644 --- a/examples/programs/flag/why3session.xml +++ b/examples/programs/flag/why3session.xml @@ -1,266 +1,325 @@ - - - + + + + + + + + + + + - + - - - - - - - - - - - - - + + + - - - - - - + - + - + - + - + - - - - - + - + - + - + - + - + - - - - - - - - - - - + - - - - - - + - + - + - + - + - + - - - - - - - - + + + + + + + + + + + - + - + - + - + + + + - + + + + - + - + - - - + + + + + + + + + - + + + + + + - - - - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + - + + + + + + + + + + - + + + + + + - + - + - + - + - + + + + + + + - + - + + + + + + + - + - + + + + + + + - + - + + + + - + - + - + - + - + - + - + - + - + - + - + + + + diff --git a/examples/programs/insertion_sort.mlw b/examples/programs/insertion_sort.mlw index c3dc62628263a354e387f4c5782243a295239275..01a7391db35c8a536b53bccf970878c9e511a5ad 100644 --- a/examples/programs/insertion_sort.mlw +++ b/examples/programs/insertion_sort.mlw @@ -15,25 +15,25 @@ module InsertionSort 'L: for i = 1 to length a - 1 do (* a[0..i[ is sorted; now insert a[i] *) - invariant { sorted_sub a 0 i /\ permut a (at a 'L) } + invariant { sorted_sub a 0 i /\ permut (at a 'L) a } let v = a[i] in let j = ref i in while !j > 0 && a[!j - 1] > v do invariant { - 0 <= !j <= i /\ permut a[!j <- v] (at a 'L) /\ + 0 <= !j <= i /\ permut (at a 'L) a[!j <- v] /\ (forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2]) /\ (forall k: int. !j+1 <= k <= i -> v < a[k]) } variant { !j } 'L1: a[!j] <- a[!j - 1]; - assert { exchange a[!j-1 <- v] (at a 'L1)[!j <- v] (!j - 1) !j}; + assert { exchange (at a 'L1)[!j <- v] a[!j-1 <- v] (!j - 1) !j}; j := !j - 1 done; assert { forall k: int. 0 <= k < !j -> a[k] <= v }; a[!j] <- v done - { sorted a /\ permut a (old a) } + { sorted a /\ permut (old a) a } end diff --git a/examples/programs/insertion_sort/why3session.xml b/examples/programs/insertion_sort/why3session.xml index 4906b134486f2201597a1085c980dbbb91d8987a..6fe7d42f2a9bed50d8af1927ca81d6baa06e73f9 100644 --- a/examples/programs/insertion_sort/why3session.xml +++ b/examples/programs/insertion_sort/why3session.xml @@ -1,172 +1,215 @@ - - - - - + + + + + + + + + + + + + - + - - - - - - + - + - + - + - + - - - + + + + + + + - + - + - - + + + + + + + + + + + + - - - + + + - - - + + + - + - + - - - + + + + + + - - - + - + - + - + + + + + + + + + - - - + + + - - - + + + - + - + + + + - - - - - - - - + + + + - + - + + + + - + - + + + + - - - + + + + + + - + - + + + + - + - + + + + - + - + + + + - + - + + + + - - - - - - - - - - - - - + + + + + + + - + - + - - - + + + + + + - + - + diff --git a/examples/programs/quicksort.mlw b/examples/programs/quicksort.mlw index 968de8a928d00b66870732bccca6c3f0780673d7..4e200eb5dca32f0b21a41c2c683d966251cb47d1 100644 --- a/examples/programs/quicksort.mlw +++ b/examples/programs/quicksort.mlw @@ -19,7 +19,7 @@ module Quicksort let v = t[i] in t[i] <- t[j]; t[j] <- v - { exchange t (old t) i j } + { exchange (old t) t i j } let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l } = { 0 <= l /\ r < length t } @@ -29,7 +29,7 @@ module Quicksort 'L: for i = l + 1 to r do invariant { (forall j:int. l < j <= !m -> t[j] < v) /\ (forall j:int. !m < j < i -> t[j] >= v) /\ - permut_sub t (at t 'L) l (r+1) /\ + permut_sub (at t 'L) t l (r+1) /\ t[l] = v /\ l <= !m < i } if t[i] < v then begin m := !m + 1; swap t i !m end done; @@ -37,12 +37,12 @@ module Quicksort quick_rec t l (!m - 1); quick_rec t (!m + 1) r end - { sorted_sub t l (r+1) /\ permut_sub t (old t) l (r+1) } + { sorted_sub t l (r+1) /\ permut_sub (old t) t l (r+1) } let quicksort (t : array int) = { } quick_rec t 0 (length t - 1) - { sorted t /\ permut t (old t) } + { sorted t /\ permut (old t) t } end diff --git a/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v b/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v new file mode 100644 index 0000000000000000000000000000000000000000..a0cfb30fe8ebfd84d739ec75c9a457ffd922ce54 --- /dev/null +++ b/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v @@ -0,0 +1,190 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Definition unit := unit. + +Parameter mark : Type. + +Parameter at1: forall (a:Type), a -> mark -> a. + +Implicit Arguments at1. + +Parameter old: forall (a:Type), a -> a. + +Implicit Arguments old. + +Inductive ref (a:Type) := + | mk_ref : a -> ref a. +Implicit Arguments mk_ref. + +Definition contents (a:Type)(u:(ref a)): a := + match u with + | mk_ref contents1 => contents1 + end. +Implicit Arguments contents. + +Parameter map : forall (a:Type) (b:Type), Type. + +Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. + +Implicit Arguments get. + +Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). + +Implicit Arguments set. + +Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) + a2) = b1). + +Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) + a2) = (get m a2)). + +Parameter const: forall (b:Type) (a:Type), b -> (map a b). + +Set Contextual Implicit. +Implicit Arguments const. +Unset Contextual Implicit. + +Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( + b1):(map a b)) a1) = b1). + +Inductive array (a:Type) := + | mk_array : Z -> (map Z a) -> array a. +Implicit Arguments mk_array. + +Definition elts (a:Type)(u:(array a)): (map Z a) := + match u with + | mk_array _ elts1 => elts1 + end. +Implicit Arguments elts. + +Definition length (a:Type)(u:(array a)): Z := + match u with + | mk_array length1 _ => length1 + end. +Implicit Arguments length. + +Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). +Implicit Arguments get1. + +Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := + match a1 with + | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) + end. +Implicit Arguments set1. + +Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), + (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a + i2))%Z. + +Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a) + l u). + +Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)). + +Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z) + (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). +Implicit Arguments map_eq_sub. + +Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z) + (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\ + forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))). +Implicit Arguments exchange. + +Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z) + (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j). + +Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) + | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l + u) -> (permut_sub a1 a3 l u)) + | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) + (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ + (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). +Implicit Arguments permut_sub. + +Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z + a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ + (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). + +Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ + (u <= i)%Z) -> ((get a2 i) = (get a1 i)). + +Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ + (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2 + i) = (get a1 j)). + +Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z) + (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Implicit Arguments exchange1. + +Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Implicit Arguments permut_sub1. + +Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z + (length a1)). +Implicit Arguments permut. + +Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) -> + (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ + (j < (length a1))%Z) -> (permut a1 a2)))). + +Axiom permut_sym1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)), + (permut a1 a2) -> (permut a2 a1). + +Axiom permut_trans1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). + +Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). +Implicit Arguments array_eq_sub. + +Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). +Implicit Arguments array_eq. + +Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u). + +Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)), (array_eq a1 a2) -> (permut a1 a2). + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Theorem WP_parameter_quick_rec : forall (t:Z), forall (l:Z), forall (r:Z), + forall (t1:(map Z Z)), ((0%Z <= l)%Z /\ (r < t)%Z) -> ((l < r)%Z -> + (((0%Z <= l)%Z /\ (l < t)%Z) -> let result := (get t1 l) in + (((l + 1%Z)%Z <= r)%Z -> forall (m:Z), forall (t2:(map Z Z)), forall (i:Z), + (((l + 1%Z)%Z <= i)%Z /\ (i <= r)%Z) -> (((forall (j:Z), ((l < j)%Z /\ + (j <= m)%Z) -> ((get t2 j) < result)%Z) /\ ((forall (j:Z), ((m < j)%Z /\ + (j < i)%Z) -> (result <= (get t2 j))%Z) /\ ((permut_sub t1 t2 l + (r + 1%Z)%Z) /\ (((get t2 l) = result) /\ ((l <= m)%Z /\ (m < i)%Z))))) -> + (((0%Z <= i)%Z /\ (i < t)%Z) -> (((get t2 i) < result)%Z -> + forall (m1:Z), (m1 = (m + 1%Z)%Z) -> ((((0%Z <= i)%Z /\ (i < t)%Z) /\ + ((0%Z <= m1)%Z /\ (m1 < t)%Z)) -> forall (t3:(map Z Z)), (exchange t2 t3 i + m1) -> (permut_sub t1 t3 l (r + 1%Z)%Z)))))))). +(* YOU MAY EDIT THE PROOF BELOW *) +intuition. +intuition. +apply permut_trans with t2; auto. +apply permut_exchange with i m1; try omega. +auto. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v b/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v index 4d6da50c8eeac9be89797f3d991bbecabdbc2c6c..81d34ff5b51685fb2b8b3a6a2daeb71abfaaeb04 100644 --- a/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v +++ b/examples/programs/quicksort/quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v @@ -6,11 +6,11 @@ Definition unit := unit. Parameter mark : Type. -Parameter at1: forall (a:Type), a -> mark -> a. +Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. -Parameter old: forall (a:Type), a -> a. +Parameter old: forall (a:Type), a -> a. Implicit Arguments old. @@ -26,11 +26,11 @@ Implicit Arguments contents. Parameter map : forall (a:Type) (b:Type), Type. -Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. +Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Implicit Arguments get. -Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). +Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Implicit Arguments set. @@ -42,7 +42,7 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). -Parameter const: forall (b:Type) (a:Type), b -> (map a b). +Parameter const: forall (b:Type) (a:Type), b -> (map a b). Set Contextual Implicit. Implicit Arguments const. @@ -142,6 +142,12 @@ Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)) (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))). +Axiom permut_sym1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)), + (permut a1 a2) -> (permut a2 a1). + +Axiom permut_trans1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). + Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). Implicit Arguments array_eq_sub. @@ -156,24 +162,28 @@ Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + Theorem WP_parameter_quick_rec : forall (t:Z), forall (l:Z), forall (r:Z), forall (t1:(map Z Z)), ((0%Z <= l)%Z /\ (r < t)%Z) -> ((l < r)%Z -> (((0%Z <= l)%Z /\ (l < t)%Z) -> let result := (get t1 l) in (((l + 1%Z)%Z <= r)%Z -> forall (m:Z), forall (t2:(map Z Z)), ((forall (j:Z), ((l < j)%Z /\ (j <= m)%Z) -> ((get t2 j) < result)%Z) /\ ((forall (j:Z), ((m < j)%Z /\ (j < (r + 1%Z)%Z)%Z) -> (result <= (get t2 - j))%Z) /\ ((permut_sub t2 t1 l (r + 1%Z)%Z) /\ (((get t2 l) = result) /\ + j))%Z) /\ ((permut_sub t1 t2 l (r + 1%Z)%Z) /\ (((get t2 l) = result) /\ ((l <= m)%Z /\ (m < (r + 1%Z)%Z)%Z))))) -> ((((0%Z <= l)%Z /\ (l < t)%Z) /\ ((0%Z <= m)%Z /\ (m < t)%Z)) -> forall (t3:(map Z Z)), - (exchange t3 t2 l m) -> ((((0%Z <= ((1%Z + r)%Z - l)%Z)%Z /\ + (exchange t2 t3 l m) -> ((((0%Z <= ((1%Z + r)%Z - l)%Z)%Z /\ (((1%Z + (m - 1%Z)%Z)%Z - l)%Z < ((1%Z + r)%Z - l)%Z)%Z) /\ ((0%Z <= l)%Z /\ ((m - 1%Z)%Z < t)%Z)) -> forall (t4:(map Z Z)), - ((sorted_sub t4 l ((m - 1%Z)%Z + 1%Z)%Z) /\ (permut_sub t4 t3 l + ((sorted_sub t4 l ((m - 1%Z)%Z + 1%Z)%Z) /\ (permut_sub t3 t4 l ((m - 1%Z)%Z + 1%Z)%Z)) -> ((((0%Z <= ((1%Z + r)%Z - l)%Z)%Z /\ (((1%Z + r)%Z - (m + 1%Z)%Z)%Z < ((1%Z + r)%Z - l)%Z)%Z) /\ ((0%Z <= (m + 1%Z)%Z)%Z /\ (r < t)%Z)) -> forall (t5:(map Z Z)), - ((sorted_sub t5 (m + 1%Z)%Z (r + 1%Z)%Z) /\ (permut_sub t5 t4 (m + 1%Z)%Z - (r + 1%Z)%Z)) -> ((sorted_sub t5 l (r + 1%Z)%Z) /\ (permut_sub t5 t1 l + ((sorted_sub t5 (m + 1%Z)%Z (r + 1%Z)%Z) /\ (permut_sub t4 t5 (m + 1%Z)%Z + (r + 1%Z)%Z)) -> ((sorted_sub t5 l (r + 1%Z)%Z) /\ (permut_sub t1 t5 l (r + 1%Z)%Z)))))))). (* YOU MAY EDIT THE PROOF BELOW *) intros n l r t1. @@ -189,25 +199,27 @@ assert (h: (l <= i1 < m \/ m <= i1 <= r)%Z) by omega. destruct h. (* l <= i1 < m *) assert (eq: get t4 i1 = get t5 i1). apply permut_eq with (m+1)%Z (r+1)%Z; auto. +apply permut_sym; auto. omega. rewrite <- eq; clear eq. assert (vi1: (get t4 i1 < v)%Z). assert (exists i3:Z, l <= i3 < m-1+1 /\ get t4 i1 = get t3 i3)%Z. apply permut_exists. -apply permut_sym; auto. +auto. omega. destruct H1 as (i3, (hi3, eq3)). rewrite eq3; clear eq3. assert (case: (i3 = l \/ l < i3)%Z) by omega. destruct case. subst i3. -destruct exch as (h,_). rewrite h. +destruct exch as (_,(h,_)). rewrite h. apply inv1; omega. -destruct exch as (_,(_,h)). rewrite h; try omega. +destruct exch as (_,(_,h)). rewrite <- h; try omega. apply inv1; omega. assert (h: (l <= i2 < m \/ m <= i2 <= r)%Z) by omega. destruct h. (* l <= i2 < m *) assert (eq: get t4 i2 = get t5 i2). apply permut_eq with (m+1)%Z (r+1)%Z; auto. +apply permut_sym; auto. omega. rewrite <- eq; clear eq. apply lsorted; omega. @@ -223,21 +235,24 @@ omega. red in exch; intuition. transitivity (get t4 m). apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. apply permut_eq with (m+1)%Z (r+1)%Z; auto. +apply permut_sym; auto. omega. (* m < i2 *) assert (exists i3:Z, m+1 <= i3 < r+1 /\ get t5 i2 = get t4 i3)%Z. apply permut_exists. -apply permut_sym; auto. +auto. omega. destruct H3 as (i3, (hi3, eq3)). rewrite eq3; clear eq3. replace (get t4 i3) with (get t3 i3). -destruct exch as (_,(_,hex)). rewrite hex. +destruct exch as (_,(_,hex)). rewrite <- hex. apply inv2; omega. omega. apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. omega. @@ -252,21 +267,24 @@ omega. red in exch; intuition. transitivity (get t4 m). apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. apply permut_eq with (m+1)%Z (r+1)%Z; auto. +apply permut_sym; auto. omega. (* m < i1 *) assert (exists i3:Z, m+1 <= i3 < r+1 /\ get t5 i1 = get t4 i3)%Z. apply permut_exists. -apply permut_sym; auto. +auto. omega. destruct H2 as (i3, (hi3, eq3)). rewrite eq3; clear eq3. replace (get t4 i3) with (get t3 i3). -destruct exch as (_,(_,hex)). rewrite hex. +destruct exch as (_,(_,hex)). rewrite <-hex. apply inv2; omega. omega. apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. assert (h: (l <= i2 < m \/ m <= i2 <= r)%Z) by omega. destruct h. @@ -283,12 +301,12 @@ assert (h: (i1 = m \/ m < i1)%Z) by omega. destruct h. subst i1. assert (exists i3:Z, m+1 <= i3 < r+1 /\ get t5 i2 = get t4 i3)%Z. apply permut_exists. -apply permut_sym; auto. +auto. omega. destruct H3 as (i3, (hi3, eq3)). rewrite eq3; clear eq3. replace (get t4 i3) with (get t3 i3). -destruct exch as (ex1,(ex2,hex)). rewrite hex. +destruct exch as (ex1,(ex2,hex)). rewrite <- hex. replace (get t5 m) with v. apply inv2; omega. replace (get t5 m) with (get t3 m). @@ -296,25 +314,28 @@ replace (get t3 m) with (get t2 l). omega. transitivity (get t4 m). apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. apply permut_eq with (m+1)%Z (r+1)%Z; auto. +apply permut_sym; auto. omega. omega. apply permut_eq with l (m-1+1)%Z; auto. +apply permut_sym; auto. omega. (* m < i1 *) apply rsorted; try omega. (* permut *) apply permut_trans with t4. -apply permut_weakening with (m+1)%Z (r+1)%Z; auto. -omega. apply permut_trans with t3. -apply permut_weakening with l (m-1+1)%Z; auto. -omega. apply permut_trans with t2; auto. apply permut_exchange with l m; auto. omega. +apply permut_weakening with l (m-1+1)%Z; auto. +omega. +apply permut_weakening with (m+1)%Z (r+1)%Z; auto. +omega. Qed. (* DO NOT EDIT BELOW *) diff --git a/examples/programs/quicksort/why3session.xml b/examples/programs/quicksort/why3session.xml index 1c090afc5224b68f4fa2396c810d05bf13f38181..483756f36792a4558bd8d6e68d2b981e31993eb6 100644 --- a/examples/programs/quicksort/why3session.xml +++ b/examples/programs/quicksort/why3session.xml @@ -1,181 +1,198 @@ + + + + + + + + - + - + - + - + - + - + - + - + - + - + - - - + + + - - + + - + - + - + - + - + - + - + - + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - + + + - + - + - + - + - + - - - - - - - + + - - - - - + - + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + diff --git a/examples/programs/selection_sort.mlw b/examples/programs/selection_sort.mlw index 587cde8a6e3bdc7eae9c76043f72998a0e0d015b..3011696a917ad446a04e797a9d06e1541e56ba6d 100644 --- a/examples/programs/selection_sort.mlw +++ b/examples/programs/selection_sort.mlw @@ -15,7 +15,7 @@ module SelectionSort let v = a[i] in a[i] <- a[j]; a[j] <- v - { exchange a (old a) i j } + { exchange (old a) a i j } let selection_sort (a: array int) = { } @@ -23,7 +23,7 @@ module SelectionSort for i = 0 to length a - 1 do (* a[0..i[ is sorted; now find minimum of a[i..n[ *) invariant - { sorted_sub a 0 i /\ permut a (at a 'L) /\ + { sorted_sub a 0 i /\ permut (at a 'L) a /\ forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] } let min = ref i in for j = i + 1 to length a - 1 do @@ -33,9 +33,9 @@ module SelectionSort done; 'L1: if !min <> i then swap a !min i; - assert { permut a (at a 'L1) } + assert { permut (at a 'L1) a } done - { sorted a /\ permut a (old a) } + { sorted a /\ permut (old a) a } end diff --git a/examples/programs/selection_sort/selection_sort_WP_SelectionSort_WP_parameter_selection_sort_1.v b/examples/programs/selection_sort/selection_sort_WP_SelectionSort_WP_parameter_selection_sort_1.v new file mode 100644 index 0000000000000000000000000000000000000000..619278b6fc14fb9e1cba23d701d43ad8eb6667e4 --- /dev/null +++ b/examples/programs/selection_sort/selection_sort_WP_SelectionSort_WP_parameter_selection_sort_1.v @@ -0,0 +1,189 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Definition unit := unit. + +Parameter mark : Type. + +Parameter at1: forall (a:Type), a -> mark -> a. + +Implicit Arguments at1. + +Parameter old: forall (a:Type), a -> a. + +Implicit Arguments old. + +Inductive ref (a:Type) := + | mk_ref : a -> ref a. +Implicit Arguments mk_ref. + +Definition contents (a:Type)(u:(ref a)): a := + match u with + | mk_ref contents1 => contents1 + end. +Implicit Arguments contents. + +Parameter map : forall (a:Type) (b:Type), Type. + +Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. + +Implicit Arguments get. + +Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). + +Implicit Arguments set. + +Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) + a2) = b1). + +Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) + a2) = (get m a2)). + +Parameter const: forall (b:Type) (a:Type), b -> (map a b). + +Set Contextual Implicit. +Implicit Arguments const. +Unset Contextual Implicit. + +Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( + b1):(map a b)) a1) = b1). + +Inductive array (a:Type) := + | mk_array : Z -> (map Z a) -> array a. +Implicit Arguments mk_array. + +Definition elts (a:Type)(u:(array a)): (map Z a) := + match u with + | mk_array _ elts1 => elts1 + end. +Implicit Arguments elts. + +Definition length (a:Type)(u:(array a)): Z := + match u with + | mk_array length1 _ => length1 + end. +Implicit Arguments length. + +Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). +Implicit Arguments get1. + +Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := + match a1 with + | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) + end. +Implicit Arguments set1. + +Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), + (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a + i2))%Z. + +Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a) + l u). + +Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)). + +Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z) + (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). +Implicit Arguments map_eq_sub. + +Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z) + (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\ + forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))). +Implicit Arguments exchange. + +Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z) + (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j). + +Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) + | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l + u) -> (permut_sub a1 a3 l u)) + | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) + (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ + (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). +Implicit Arguments permut_sub. + +Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z + a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ + (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). + +Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ + (u <= i)%Z) -> ((get a2 i) = (get a1 i)). + +Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ + (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2 + i) = (get a1 j)). + +Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z) + (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Implicit Arguments exchange1. + +Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Implicit Arguments permut_sub1. + +Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z + (length a1)). +Implicit Arguments permut. + +Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) -> + (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ + (j < (length a1))%Z) -> (permut a1 a2)))). + +Axiom permut_refl1 : forall (a:Type), forall (a1:(array a)), (permut a1 a1). + +Axiom permut_sym1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)), + (permut a1 a2) -> (permut a2 a1). + +Axiom permut_trans1 : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). + +Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). +Implicit Arguments array_eq_sub. + +Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). +Implicit Arguments array_eq. + +Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u). + +Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)), (array_eq a1 a2) -> (permut a1 a2). + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Theorem WP_parameter_selection_sort : forall (a:Z), forall (a1:(map Z Z)), + (0%Z <= (a - 1%Z)%Z)%Z -> forall (a2:(map Z Z)), let a3 := (mk_array a + a2) in forall (i:Z), ((0%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) -> + (((sorted_sub a2 0%Z i) /\ ((permut (mk_array a a1) a3) /\ forall (k1:Z) + (k2:Z), ((((0%Z <= k1)%Z /\ (k1 < i)%Z) /\ (i <= k2)%Z) /\ (k2 < a)%Z) -> + ((get a2 k1) <= (get a2 k2))%Z)) -> (((i + 1%Z)%Z <= (a - 1%Z)%Z)%Z -> + forall (min:Z), (((i <= min)%Z /\ (min < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\ + forall (k:Z), ((i <= k)%Z /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) -> ((get a2 + min) <= (get a2 k))%Z) -> ((~ (min = i)) -> ((((0%Z <= min)%Z /\ + (min < a)%Z) /\ ((0%Z <= i)%Z /\ (i < a)%Z)) -> forall (a4:(map Z Z)), + (exchange a2 a4 min i) -> (permut a3 (mk_array a a4)))))). +(* YOU MAY EDIT THE PROOF BELOW *) +intuition. +intuition. +apply exchange_permut with min i; auto. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/selection_sort/why3session.xml b/examples/programs/selection_sort/why3session.xml index 690b1bcbc6ff0c33566ffb1759af837e3d8a3bde..e70a2131dc9cdb0ad5830a64339e63f049bab66d 100644 --- a/examples/programs/selection_sort/why3session.xml +++ b/examples/programs/selection_sort/why3session.xml @@ -1,132 +1,140 @@ + + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + + + - + - + - - - + + + - + - + - + - + - + - + + + + + + - + - + diff --git a/modules/array.mlw b/modules/array.mlw index bcbdc36628faae3dcb4c215e8f506e9693ab53fd..813453197d1089dd80d8724d9307d352a05ee0a2 100644 --- a/modules/array.mlw +++ b/modules/array.mlw @@ -149,11 +149,19 @@ module ArrayPermut a1.length = a2.length /\ M.permut_sub a1.elts a2.elts 0 a1.length lemma exchange_permut: - forall a1 a2: array 'a, i j: int. + forall a1 a2: array 'a, i j: int [exchange a1 a2 i j]. exchange a1 a2 i j -> a1.length = a2.length -> 0 <= i < a1.length -> 0 <= j < a1.length -> permut a1 a2 + lemma permut_sym: + forall a1 a2: array 'a. + permut a1 a2 -> permut a2 a1 + + lemma permut_trans: + forall a1 a2 a3: array 'a. + permut a1 a2 -> permut a2 a3 -> permut a1 a3 + use import module ArrayEq lemma array_eq_sub_permut: