Commit fd9919f2 by Jean-Christophe Filliatre

### permutation property: more lemmas and updated proofs (in progress)

parent 1e29247f
 ... ... @@ -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 ... ...
This diff is collapsed.
 ... ... @@ -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 ... ...
This diff is collapsed.
 ... ... @@ -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 ... ...
 (* 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 *)
 ... ... @@ -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 *) ... ...
This diff is collapsed.
 ... ... @@ -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 ... ...
 (* 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