selection_sort.mlw_Quicksort_WP_parameter selection_sort_2.v 6.53 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
(* 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 label : Type.

Parameter at1: forall (a:Type), a -> label  -> 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), (l <= 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)))).

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).

Theorem WP_parameter_selection_sort : forall (a:Z), forall (a1:(map Z Z)),
  let a2 := (mk_array a a1) in ((0%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
  Z)), forall (i:Z), ((0%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) ->
  (((sorted_sub a3 0%Z i) /\ ((permut (mk_array a a3) a2) /\ forall (k1:Z)
  (k2:Z), ((((0%Z <= k1)%Z /\ (k1 <  i)%Z) /\ (i <= k2)%Z) /\ (k2 <  a)%Z) ->
  ((get a3 k1) <= (get a3 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 a3
  min) <= (get a3 k))%Z) -> ((~ (min = i)) -> ((((0%Z <= min)%Z /\
  (min <  a)%Z) /\ ((0%Z <= i)%Z /\ (i <  a)%Z)) -> forall (a4:(map Z Z)),
  (exchange a4 a3 min i) -> (permut (mk_array a a4) a2)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
unfold permut; simpl; intuition.
apply permut_trans with a3; auto.
apply permut_exchange with min i; auto.
unfold permut in H1.
intuition.
Qed.
(* DO NOT EDIT BELOW *)