Commit e79e9a4f by Jean-Christophe Filliatre

### fixed inconsistencies in theory MapPermut/ArrayPermut

```predicates permut over maps and arrays are given new semantics, as follows:
- MapPermut: permut m1 m2 l u means that m1[l..u[ is a permutation of
m2[l..u[ and values outside the interval [l..u[ are *ignored*.
- ArrayPermut: permut_sub a1 a2 l u means that a1[l..u[ is a permutation
of a2[l..u[ and other meaningful values are *identical*.
- ArrayPermut: another predicate map_permut_sub has the same semantics as
MapPermut.permut_sub, that is values outside of the interval [l..u[
are ignored```
parent 1e83ae78
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require map.MapPermut. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a). Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a := match v with | (mk_ref x) => x end. (* Why3 assumption *) Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a. Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Existing Instance array_WhyType. Implicit Arguments mk_array [[a] [a_WT]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map Z _ a a_WT) := match v with | (mk_array x x1) => x1 end. (* Why3 assumption *) Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z := match v with | (mk_array x x1) => x end. (* Why3 assumption *) Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a := (map.Map.get (elts a1) i). (* Why3 assumption *) Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z) (v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i v)). (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) := (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2) 0%Z (length a1)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= i)%Z /\ (i < (length a1))%Z) /\ (((0%Z <= j)%Z /\ (j < (length a1))%Z) /\ (((get a1 i) = (get a2 j)) /\ (((get a1 j) = (get a2 i)) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k < (length a1))%Z) -> ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (array_eq_sub a1 a2 0%Z l) /\ ((map_permut_sub a1 a2 l u) /\ (array_eq_sub a2 a2 u (length a1))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). (* Why3 goal *) Theorem WP_parameter_partition : forall (a:Z) (a1:(@map.Map.map Z _ Z _)) (m:Z) (n:Z), ((0%Z <= a)%Z /\ ((0%Z <= m)%Z /\ ((m < n)%Z /\ (n < a)%Z))) -> (((0%Z <= m)%Z /\ ((m < n)%Z /\ (n < a)%Z)) -> forall (o:Z) (j:Z) (i:Z) (a2:(@map.Map.map Z _ Z _)), ((0%Z <= a)%Z /\ (((m <= j)%Z /\ ((j < i)%Z /\ (i <= n)%Z)) /\ ((permut_sub (mk_array a a1) (mk_array a a2) m (n + 1%Z)%Z) /\ ((forall (r:Z), ((m <= r)%Z /\ (r <= j)%Z) -> ((map.Map.get a2 r) <= o)%Z) /\ ((forall (r:Z), ((j < r)%Z /\ (r < i)%Z) -> ((map.Map.get a2 r) = o)) /\ forall (r:Z), ((i <= r)%Z /\ (r <= n)%Z) -> (o <= (map.Map.get a2 r))%Z))))) -> exists x:Z, (forall (r:Z), ((m <= r)%Z /\ (r <= j)%Z) -> ((map.Map.get a2 r) <= x)%Z) /\ ((forall (r:Z), ((j < r)%Z /\ (r < i)%Z) -> ((map.Map.get a2 r) = x)) /\ forall (r:Z), ((i <= r)%Z /\ (r <= n)%Z) -> (x <= (map.Map.get a2 r))%Z)). intros a a1 m n (h1,(h2,(h3,h4))) (h5,(h6,h7)) o j i a2 (h8,((h9,(h10,h11)),(h12,(h13,(h14,h15))))). exists o; auto. Qed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -55,25 +55,56 @@ Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z) Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) := (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2) 0%Z (length a1)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j). (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= i)%Z /\ (i < (length a1))%Z) /\ (((0%Z <= j)%Z /\ (j < (length a1))%Z) /\ (((get a1 i) = (get a2 j)) /\ (((get a1 j) = (get a2 i)) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k < (length a1))%Z) -> ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u). (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ ((map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((map.MapPermut.permut_sub (elts a1) (elts a2) l u) /\ (map_eq_sub (elts a2) (elts a2) u (length a1)))))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange 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)))). a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). ... ... @@ -82,28 +113,18 @@ Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). Axiom elt : Type. Parameter elt_WhyType : WhyType elt. Existing Instance elt_WhyType. ... ... @@ -152,9 +173,13 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ (map.Map.get a4 o1) v)) -> let o2 := (j - 1%Z)%Z in (((0%Z <= o2)%Z /\ (o2 < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(@map.Map.map Z _ elt elt_WhyType)), ((0%Z <= a)%Z /\ (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((map.MapPermut.exchange (map.Map.set a4 j v) (map.Map.set a5 (j - 1%Z)%Z v) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). o2)))) -> ((exchange (mk_array a (map.Map.set a4 j v)) (mk_array a (map.Map.set a5 (j - 1%Z)%Z v)) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). (* Why3 intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. *) intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. ... ...
 ... ... @@ -68,25 +68,56 @@ Definition sorted_sub1 (a:(@array Z _)) (l:Z) (u:Z): Prop := (sorted_sub Definition sorted (a:(@array Z _)): Prop := (sorted_sub (elts a) 0%Z (length a)). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2) 0%Z (length a1)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := (map.MapPermut.exchange (elts a1) (elts a2) i j). (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= i)%Z /\ (i < (length a1))%Z) /\ (((0%Z <= j)%Z /\ (j < (length a1))%Z) /\ (((get a1 i) = (get a2 j)) /\ (((get a1 j) = (get a2 i)) /\ forall (k:Z), ((0%Z <= k)%Z /\ (k < (length a1))%Z) -> ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map.MapPermut.permut_sub (elts a1) (elts a2) l u). (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ ((map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((map.MapPermut.permut_sub (elts a1) (elts a2) l u) /\ (map_eq_sub (elts a2) (elts a2) u (length a1)))))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange 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)))). a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). ... ... @@ -95,28 +126,18 @@ Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). Import MapPermut. (* Why3 goal *) ... ... @@ -135,10 +156,13 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ ((0%Z <= o1)%Z /\ (o1 < a)%Z)) -> ((v < (map.Map.get a4 o1))%Z -> let o2 := (j - 1%Z)%Z in (((0%Z <= o2)%Z /\ (o2 < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(@map.Map.map Z _ Z _)), ((0%Z <= a)%Z /\ (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((map.MapPermut.exchange (map.Map.set a4 j v) (map.Map.set a5 (j - 1%Z)%Z v) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((exchange (mk_array a (map.Map.set a4 j v)) (mk_array a (map.Map.set a5 (j - 1%Z)%Z v)) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). (* Why3 intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. *) intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. ... ... @@ -153,9 +177,8 @@ apply permut_trans with (elts (set (mk_array a a4) j (Map.get a3 i))); auto. subst j1. unfold permut in h12. intuition. apply permut_exchange with (j-1)%Z j. simpl; omega. simpl; omega. generalize (exchange_permut _ _ _ _ h26). unfold permut; simpl; intuition. subst j1; assumption. Qed.
This diff is collapsed.
 ... ... @@ -151,6 +151,7 @@ module InsertionSortParam a[!j] <- a[b]; a[b] <- t; assert { exchange (at a 'L) a (!j-1) !j }; assert { sorted_sub p a.elts (!j-1) (i+1) }; decr j done done ... ...
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -6,36 +6,16 @@ Require int.Int. Require map.Map. (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (i:Z) (j:Z): Prop := ((map.Map.get a1 i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2 k))). (* Why3 goal *) Lemma exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)), forall (i:Z) (j:Z), (exchange a1 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i j). Proof. intros a a_WT a1 i j. split. now rewrite Map.Select_eq. split. destruct (Z_eq_dec i j) as [H|H]. rewrite H. now rewrite Map.Select_eq. rewrite Map.Select_neq by now apply sym_not_eq. now rewrite Map.Select_eq. intros k (Hk1,Hk2). now rewrite 2!Map.Select_neq by now apply sym_not_eq. Qed. Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := | permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a1 l u) | permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (map_eq_sub a1 a2 l u) -> ((@permut_sub _ _) a1 a2 l u) | permut_sym : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a2 l u) -> ((@permut_sub _ _) a2 a1 l u) ... ... @@ -45,44 +25,32 @@ Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> ((@permut_sub _ _) a1 a3 l u)) | permut_exchange : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), 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))). (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (((map.Map.get a1 i) = (map.Map.get a2 j)) -> (((map.Map.get a1 j) = (map.Map.get a2 i)) -> ((forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) -> ((~ (k = i)) -> ((~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2 k))))) -> ((@permut_sub _ _) a1 a2 l u))))). (* Why3 goal *) Lemma permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), 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)). Proof. intros a a_WT a1 a2 l1 r1 l2 r2 ((h1,h2),h3) h4. induction h4. constructor. constructor. now apply IHh4. constructor 3 with a2. now apply IHh4_1. now apply IHh4_2. constructor 4 with (3 := H1). omega. omega. Qed. (* Why3 goal *) Lemma permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 i) = (map.Map.get a1 i)). Proof. intros a a_WT a1 a2 l u h1 i h2. induction h1. apply eq_refl. now apply sym_eq, IHh1. etransitivity. now apply IHh1_2. now apply IHh1_1. apply sym_eq. apply H1. omega. Lemma permut_exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (permut_sub a1 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l u)). intros a a_WT a1 l u i j (h1,h2) (h3,h4). apply permut_exchange with i j; auto. assert (h: i=j \/ i<>j) by omega. destruct h. subst. rewrite Map.Select_eq; auto. rewrite Map.Select_eq; auto. assert (h: i=j \/ i<>j) by omega. destruct h. subst. rewrite Map.Select_eq; auto. rewrite Map.Select_neq; auto. rewrite Map.Select_eq; auto. intros. rewrite Map.Select_neq; auto. rewrite Map.Select_neq; auto. Qed. (* Why3 goal *) ... ... @@ -99,7 +67,9 @@ assert ((exists j, (l <= j < u)%Z /\ Map.get a2 i = Map.get a1 j) /\ revert i Hi. induction h1. intros i Hi. now split ; exists i ; split. red in H. split ; exists i ; intuition. rewrite <- H; auto. intros i Hi. destruct (IHh1 i Hi) as ((j&H1&H2),(k&H3&H4)). split. ... ... @@ -123,17 +93,17 @@ split ; exists j ; split ; try easy ; rewrite Hki ; apply H1. intuition. destruct (Z_eq_dec k j) as [Hkj|Hkj]. split ; exists i ; split ; try easy ; rewrite Hkj ; apply sym_eq, H1. apply sym_eq; intuition. split ; exists k ; split ; try easy. now apply sym_eq, H1 ; split. now apply H1 ; split. now apply sym_eq, H3 ; intuition. now apply H3 ; intuition. Qed.
 ... ... @@ -129,15 +129,16 @@ end module ArrayEq use import int.Int use import Array use import map.MapEq as M use import map.MapEq predicate array_eq_sub (a1 a2: array 'a) (l u: int) = a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\ map_eq_sub a1.elts a2.elts l u predicate array_eq (a1 a2: array 'a) = a1.length = a2.length /\ array_eq_sub a1 a2 0 a1.length a1.length = a2.length /\ map_eq_sub a1.elts a2.elts 0 (length a1) end ... ... @@ -148,21 +149,43 @@ module ArrayPermut use import int.Int use import Array use import map.MapPermut as M use import map.MapEq use import ArrayEq predicate exchange (a1 a2: array 'a) (i j: int) = M.exchange a1.elts a2.elts i j a1.length = a2.length /\ 0 <= i < a1.length /\ 0 <= j < a1.length /\ a1[i] = a2[j] /\ a1[j] = a2[i] /\ (forall k:int. 0 <= k < a1.length -> k <> i -> k <> j -> a1[k] = a2[k]) (** [exchange a1 a2 i j] means that arrays [a1] and [a2] only differ by the swapping of elements at indices [i] and [j] *) predicate map_permut_sub (a1 a2: array 'a) (l u: int) = a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\ M.permut_sub a1.elts a2.elts l u (** [map_permut_sub a1 a2 l u] is true when the segment [a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]. Values outside of the interval (l..u-1) are ignored. *) predicate permut_sub (a1 a2: array 'a) (l u: int) =