examples/WP_revisited/blocking_semantics5/blocking_semantics5_WP_progress_5.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require BuiltIn.
   5 Require bool.Bool.
   6 Require int.Int.
   7 Require map.Map.
   8 Require list.List.
   9 Require list.Length.
  10 Require list.Mem.
  11 Require list.Append.
  12
  13 (* Why3 assumption *)
  14 Inductive datatype :=
  15   | TYunit : datatype
  16   | TYint : datatype
  17   | TYbool : datatype.
  18 Axiom datatype_WhyType : WhyType datatype.
  19 Existing Instance datatype_WhyType.
  20
  21 (* Why3 assumption *)
  22 Inductive value :=
  23   | Vvoid : value
  24   | Vint : Z -> value
  25   | Vbool : bool -> value.
  26 Axiom value_WhyType : WhyType value.
  27 Existing Instance value_WhyType.
  28
  29 (* Why3 assumption *)
  30 Inductive operator :=
  31   | Oplus : operator
  32   | Ominus : operator
  33   | Omult : operator
  34   | Ole : operator.
  35 Axiom operator_WhyType : WhyType operator.
  36 Existing Instance operator_WhyType.
  37
  38 Axiom mident : Type.
  39 Parameter mident_WhyType : WhyType mident.
  40 Existing Instance mident_WhyType.
  41
  42 Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
  43   ~ (m1 = m2).
  44
  45 Axiom ident : Type.
  46 Parameter ident_WhyType : WhyType ident.
  47 Existing Instance ident_WhyType.
  48
  49 Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
  50
  51 (* Why3 assumption *)
  52 Inductive term :=
  53   | Tvalue : value -> term
  54   | Tvar : ident -> term
  55   | Tderef : mident -> term
  56   | Tbin : term -> operator -> term -> term.
  57 Axiom term_WhyType : WhyType term.
  58 Existing Instance term_WhyType.
  59
  60 (* Why3 assumption *)
  61 Inductive fmla :=
  62   | Fterm : term -> fmla
  63   | Fand : fmla -> fmla -> fmla
  64   | Fnot : fmla -> fmla
  65   | Fimplies : fmla -> fmla -> fmla
  66   | Flet : ident -> term -> fmla -> fmla
  67   | Fforall : ident -> datatype -> fmla -> fmla.
  68 Axiom fmla_WhyType : WhyType fmla.
  69 Existing Instance fmla_WhyType.
  70
  71 (* Why3 assumption *)
  72 Inductive stmt :=
  73   | Sskip : stmt
  74   | Sassign : mident -> term -> stmt
  75   | Sseq : stmt -> stmt -> stmt
  76   | Sif : term -> stmt -> stmt -> stmt
  77   | Sassert : fmla -> stmt
  78   | Swhile : term -> fmla -> stmt -> stmt.
  79 Axiom stmt_WhyType : WhyType stmt.
  80 Existing Instance stmt_WhyType.
  81
  82 Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
  83
  84 (* Why3 assumption *)
  85 Definition env := (map.Map.map mident value).
  86
  87 (* Why3 assumption *)
  88 Definition stack := (list (ident* value)%type).
  89
  90 Parameter get_stack: ident -> (list (ident* value)%type) -> value.
  91
  92 Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
  93   match pi with
  94   | Init.Datatypes.nil => ((get_stack i pi) = Vvoid)
  95   | (Init.Datatypes.cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\
  96       ((~ (x = i)) -> ((get_stack i pi) = (get_stack i r)))
  97   end.
  98
  99 Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
 100   value)%type)), ((get_stack x (Init.Datatypes.cons (x, v) r)) = v).
 101
 102 Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
 103   value)%type)), (~ (x = i)) -> ((get_stack i (Init.Datatypes.cons (x,
 104   v) r)) = (get_stack i r)).
 105
 106 Parameter eval_bin: value -> operator -> value -> value.
 107
 108 Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
 109   y) with
 110   | ((Vint x1), (Vint y1)) =>
 111       match op with
 112       | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
 113       | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
 114       | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
 115       | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
 116           ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
 117       end
 118   | (_, _) => ((eval_bin x op y) = Vvoid)
 119   end.
 120
 121 (* Why3 assumption *)
 122 Fixpoint eval_term (sigma:(map.Map.map mident value)) (pi:(list (ident*
 123   value)%type)) (t:term) {struct t}: value :=
 124   match t with
 125   | (Tvalue v) => v
 126   | (Tvar id) => (get_stack id pi)
 127   | (Tderef id) => (map.Map.get sigma id)
 128   | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
 129       pi t2))
 130   end.
 131
 132 (* Why3 assumption *)
 133 Fixpoint eval_fmla (sigma:(map.Map.map mident value)) (pi:(list (ident*
 134   value)%type)) (f:fmla) {struct f}: Prop :=
 135   match f with
 136   | (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
 137   | (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
 138   | (Fnot f1) => ~ (eval_fmla sigma pi f1)
 139   | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
 140   | (Flet x t f1) => (eval_fmla sigma (Init.Datatypes.cons (x,
 141       (eval_term sigma pi t)) pi) f1)
 142   | (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma
 143       (Init.Datatypes.cons (x, (Vint n)) pi) f1)
 144   | (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma
 145       (Init.Datatypes.cons (x, (Vbool b)) pi) f1)
 146   | (Fforall x TYunit f1) => (eval_fmla sigma (Init.Datatypes.cons (x,
 147       Vvoid) pi) f1)
 148   end.
 149
 150 (* Why3 assumption *)
 151 Definition valid_fmla (p:fmla): Prop := forall (sigma:(map.Map.map mident
 152   value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
 153
 154 (* Why3 assumption *)
 155 Inductive one_step: (map.Map.map mident value) -> (list (ident*
 156   value)%type) -> stmt -> (map.Map.map mident value) -> (list (ident*
 157   value)%type) -> stmt -> Prop :=
 158   | one_step_assign : forall (sigma:(map.Map.map mident value))
 159       (sigma':(map.Map.map mident value)) (pi:(list (ident* value)%type))
 160       (x:mident) (t:term), (sigma' = (map.Map.set sigma x (eval_term sigma pi
 161       t))) -> (one_step sigma pi (Sassign x t) sigma' pi Sskip)
 162   | one_step_seq_noskip : forall (sigma:(map.Map.map mident value))
 163       (sigma':(map.Map.map mident value)) (pi:(list (ident* value)%type))
 164       (pi':(list (ident* value)%type)) (s1:stmt) (s1':stmt) (s2:stmt),
 165       (one_step sigma pi s1 sigma' pi' s1') -> (one_step sigma pi (Sseq s1
 166       s2) sigma' pi' (Sseq s1' s2))
 167   | one_step_seq_skip : forall (sigma:(map.Map.map mident value))
 168       (pi:(list (ident* value)%type)) (s:stmt), (one_step sigma pi
 169       (Sseq Sskip s) sigma pi s)
 170   | one_step_if_true : forall (sigma:(map.Map.map mident value))
 171       (pi:(list (ident* value)%type)) (t:term) (s1:stmt) (s2:stmt),
 172       ((eval_term sigma pi t) = (Vbool true)) -> (one_step sigma pi (Sif t s1
 173       s2) sigma pi s1)
 174   | one_step_if_false : forall (sigma:(map.Map.map mident value))
 175       (pi:(list (ident* value)%type)) (t:term) (s1:stmt) (s2:stmt),
 176       ((eval_term sigma pi t) = (Vbool false)) -> (one_step sigma pi (Sif t
 177       s1 s2) sigma pi s2)
 178   | one_step_assert : forall (sigma:(map.Map.map mident value))
 179       (pi:(list (ident* value)%type)) (f:fmla), (eval_fmla sigma pi f) ->
 180       (one_step sigma pi (Sassert f) sigma pi Sskip)
 181   | one_step_while_true : forall (sigma:(map.Map.map mident value))
 182       (pi:(list (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
 183       ((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
 184       cond) = (Vbool true))) -> (one_step sigma pi (Swhile cond inv body)
 185       sigma pi (Sseq body (Swhile cond inv body)))
 186   | one_step_while_false : forall (sigma:(map.Map.map mident value))
 187       (pi:(list (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
 188       ((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
 189       cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
 190       sigma pi Sskip).
 191
 192 (* Why3 assumption *)
 193 Inductive many_steps: (map.Map.map mident value) -> (list (ident*
 194   value)%type) -> stmt -> (map.Map.map mident value) -> (list (ident*
 195   value)%type) -> stmt -> Z -> Prop :=
 196   | many_steps_refl : forall (sigma:(map.Map.map mident value))
 197       (pi:(list (ident* value)%type)) (s:stmt), (many_steps sigma pi s sigma
 198       pi s 0%Z)
 199   | many_steps_trans : forall (sigma1:(map.Map.map mident value))
 200       (sigma2:(map.Map.map mident value)) (sigma3:(map.Map.map mident value))
 201       (pi1:(list (ident* value)%type)) (pi2:(list (ident* value)%type))
 202       (pi3:(list (ident* value)%type)) (s1:stmt) (s2:stmt) (s3:stmt) (n:Z),
 203       (one_step sigma1 pi1 s1 sigma2 pi2 s2) -> ((many_steps sigma2 pi2 s2
 204       sigma3 pi3 s3 n) -> (many_steps sigma1 pi1 s1 sigma3 pi3 s3
 205       (n + 1%Z)%Z)).
 206
 207 Axiom steps_non_neg : forall (sigma1:(map.Map.map mident value))
 208   (sigma2:(map.Map.map mident value)) (pi1:(list (ident* value)%type))
 209   (pi2:(list (ident* value)%type)) (s1:stmt) (s2:stmt) (n:Z), (many_steps
 210   sigma1 pi1 s1 sigma2 pi2 s2 n) -> (0%Z <= n)%Z.
 211
 212 (* Why3 assumption *)
 213 Definition reductible (sigma:(map.Map.map mident value)) (pi:(list (ident*
 214   value)%type)) (s:stmt): Prop := exists sigma':(map.Map.map mident value),
 215   exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
 216   sigma' pi' s').
 217
 218 (* Why3 assumption *)
 219 Definition type_value (v:value): datatype :=
 220   match v with
 221   | Vvoid => TYunit
 222   | (Vint _) => TYint
 223   | (Vbool _) => TYbool
 224   end.
 225
 226 (* Why3 assumption *)
 227 Inductive type_operator: operator -> datatype -> datatype -> datatype ->
 228   Prop :=
 229   | Type_plus : (type_operator Oplus TYint TYint TYint)
 230   | Type_minus : (type_operator Ominus TYint TYint TYint)
 231   | Type_mult : (type_operator Omult TYint TYint TYint)
 232   | Type_le : (type_operator Ole TYint TYint TYbool).
 233
 234 (* Why3 assumption *)
 235 Definition type_stack := (list (ident* datatype)%type).
 236
 237 Parameter get_vartype: ident -> (list (ident* datatype)%type) -> datatype.
 238
 239 Axiom get_vartype_def : forall (i:ident) (pi:(list (ident* datatype)%type)),
 240   match pi with
 241   | Init.Datatypes.nil => ((get_vartype i pi) = TYunit)
 242   | (Init.Datatypes.cons (x, ty) r) => ((x = i) -> ((get_vartype i
 243       pi) = ty)) /\ ((~ (x = i)) -> ((get_vartype i pi) = (get_vartype i r)))
 244   end.
 245
 246 (* Why3 assumption *)
 247 Definition type_env := (map.Map.map mident datatype).
 248
 249 (* Why3 assumption *)
 250 Inductive type_term: (map.Map.map mident datatype) -> (list (ident*
 251   datatype)%type) -> term -> datatype -> Prop :=
 252   | Type_value : forall (sigma:(map.Map.map mident datatype))
 253       (pi:(list (ident* datatype)%type)) (v:value), (type_term sigma pi
 254       (Tvalue v) (type_value v))
 255   | Type_var : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 256       datatype)%type)) (v:ident) (ty:datatype), ((get_vartype v pi) = ty) ->
 257       (type_term sigma pi (Tvar v) ty)
 258   | Type_deref : forall (sigma:(map.Map.map mident datatype))
 259       (pi:(list (ident* datatype)%type)) (v:mident) (ty:datatype),
 260       ((map.Map.get sigma v) = ty) -> (type_term sigma pi (Tderef v) ty)
 261   | Type_bin : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 262       datatype)%type)) (t1:term) (t2:term) (op:operator) (ty1:datatype)
 263       (ty2:datatype) (ty:datatype), ((type_term sigma pi t1 ty1) /\
 264       ((type_term sigma pi t2 ty2) /\ (type_operator op ty1 ty2 ty))) ->
 265       (type_term sigma pi (Tbin t1 op t2) ty).
 266
 267 (* Why3 assumption *)
 268 Inductive type_fmla: (map.Map.map mident datatype) -> (list (ident*
 269   datatype)%type) -> fmla -> Prop :=
 270   | Type_term : forall (sigma:(map.Map.map mident datatype))
 271       (pi:(list (ident* datatype)%type)) (t:term), (type_term sigma pi t
 272       TYbool) -> (type_fmla sigma pi (Fterm t))
 273   | Type_conj : forall (sigma:(map.Map.map mident datatype))
 274       (pi:(list (ident* datatype)%type)) (f1:fmla) (f2:fmla), ((type_fmla
 275       sigma pi f1) /\ (type_fmla sigma pi f2)) -> (type_fmla sigma pi
 276       (Fand f1 f2))
 277   | Type_neg : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 278       datatype)%type)) (f:fmla), (type_fmla sigma pi f) -> (type_fmla sigma
 279       pi (Fnot f))
 280   | Type_implies : forall (sigma:(map.Map.map mident datatype))
 281       (pi:(list (ident* datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla
 282       sigma pi f1) -> ((type_fmla sigma pi f2) -> (type_fmla sigma pi
 283       (Fimplies f1 f2)))
 284   | Type_let : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 285       datatype)%type)) (x:ident) (t:term) (f:fmla) (ty:datatype), (type_term
 286       sigma pi t ty) -> ((type_fmla sigma (Init.Datatypes.cons (x, ty) pi)
 287       f) -> (type_fmla sigma pi (Flet x t f)))
 288   | Type_forall : forall (sigma:(map.Map.map mident datatype))
 289       (pi:(list (ident* datatype)%type)) (x:ident) (f:fmla) (ty:datatype),
 290       (type_fmla sigma (Init.Datatypes.cons (x, ty) pi) f) -> (type_fmla
 291       sigma pi (Fforall x ty f)).
 292
 293 (* Why3 assumption *)
 294 Inductive type_stmt: (map.Map.map mident datatype) -> (list (ident*
 295   datatype)%type) -> stmt -> Prop :=
 296   | Type_skip : forall (sigma:(map.Map.map mident datatype))
 297       (pi:(list (ident* datatype)%type)), (type_stmt sigma pi Sskip)
 298   | Type_seq : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 299       datatype)%type)) (s1:stmt) (s2:stmt), (type_stmt sigma pi s1) ->
 300       ((type_stmt sigma pi s2) -> (type_stmt sigma pi (Sseq s1 s2)))
 301   | Type_assigns : forall (sigma:(map.Map.map mident datatype))
 302       (pi:(list (ident* datatype)%type)) (x:mident) (t:term) (ty:datatype),
 303       ((map.Map.get sigma x) = ty) -> ((type_term sigma pi t ty) ->
 304       (type_stmt sigma pi (Sassign x t)))
 305   | Type_if : forall (sigma:(map.Map.map mident datatype)) (pi:(list (ident*
 306       datatype)%type)) (t:term) (s1:stmt) (s2:stmt), (type_term sigma pi t
 307       TYbool) -> ((type_stmt sigma pi s1) -> ((type_stmt sigma pi s2) ->
 308       (type_stmt sigma pi (Sif t s1 s2))))
 309   | Type_assert : forall (sigma:(map.Map.map mident datatype))
 310       (pi:(list (ident* datatype)%type)) (p:fmla), (type_fmla sigma pi p) ->
 311       (type_stmt sigma pi (Sassert p))
 312   | Type_while : forall (sigma:(map.Map.map mident datatype))
 313       (pi:(list (ident* datatype)%type)) (cond:term) (body:stmt) (inv:fmla),
 314       (type_fmla sigma pi inv) -> ((type_term sigma pi cond TYbool) ->
 315       ((type_stmt sigma pi body) -> (type_stmt sigma pi (Swhile cond inv
 316       body)))).
 317
 318 (* Why3 assumption *)
 319 Definition compatible_env (sigma:(map.Map.map mident value))
 320   (sigmat:(map.Map.map mident datatype)) (pi:(list (ident* value)%type))
 321   (pit:(list (ident* datatype)%type)): Prop := (forall (id:mident),
 322   ((type_value (map.Map.get sigma id)) = (map.Map.get sigmat id))) /\
 323   forall (id:ident), ((type_value (get_stack id pi)) = (get_vartype id pit)).
 324
 325 Axiom type_inversion : forall (v:value),
 326   match (type_value v) with
 327   | TYbool => exists b:bool, (v = (Vbool b))
 328   | TYint => exists n:Z, (v = (Vint n))
 329   | TYunit => (v = Vvoid)
 330   end.
 331
 332 Axiom eval_type_term : forall (t:term) (sigma:(map.Map.map mident value))
 333   (pi:(list (ident* value)%type)) (sigmat:(map.Map.map mident datatype))
 334   (pit:(list (ident* datatype)%type)) (ty:datatype), (compatible_env sigma
 335   sigmat pi pit) -> ((type_term sigmat pit t ty) ->
 336   ((type_value (eval_term sigma pi t)) = ty)).
 337
 338 Axiom type_preservation : forall (s1:stmt) (s2:stmt) (sigma1:(map.Map.map
 339   mident value)) (sigma2:(map.Map.map mident value)) (pi1:(list (ident*
 340   value)%type)) (pi2:(list (ident* value)%type)) (sigmat:(map.Map.map mident
 341   datatype)) (pit:(list (ident* datatype)%type)), ((type_stmt sigmat pit
 342   s1) /\ ((compatible_env sigma1 sigmat pi1 pit) /\ (one_step sigma1 pi1 s1
 343   sigma2 pi2 s2))) -> ((type_stmt sigmat pit s2) /\ (compatible_env sigma2
 344   sigmat pi2 pit)).
 345
 346 Axiom Cons_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:a)
 347   (l1:(list a)) (l2:(list a)),
 348   ((Init.Datatypes.cons a1 (Init.Datatypes.app l1 l2)) = (Init.Datatypes.app (Init.Datatypes.cons a1 l1) l2)).
 349
 350 Axiom Append_nil_l : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
 351   ((Init.Datatypes.app Init.Datatypes.nil l) = l).
 352
 353 Parameter msubst_term: term -> mident -> ident -> term.
 354
 355 Axiom msubst_term_def : forall (t:term) (x:mident) (v:ident),
 356   match t with
 357   | ((Tvalue _)|(Tvar _)) => ((msubst_term t x v) = t)
 358   | (Tderef y) => ((x = y) -> ((msubst_term t x v) = (Tvar v))) /\
 359       ((~ (x = y)) -> ((msubst_term t x v) = t))
 360   | (Tbin t1 op t2) => ((msubst_term t x v) = (Tbin (msubst_term t1 x v) op
 361       (msubst_term t2 x v)))
 362   end.
 363
 364 (* Why3 assumption *)
 365 Fixpoint msubst (f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
 366   match f with
 367   | (Fterm e) => (Fterm (msubst_term e x v))
 368   | (Fand f1 f2) => (Fand (msubst f1 x v) (msubst f2 x v))
 369   | (Fnot f1) => (Fnot (msubst f1 x v))
 370   | (Fimplies f1 f2) => (Fimplies (msubst f1 x v) (msubst f2 x v))
 371   | (Flet y t f1) => (Flet y (msubst_term t x v) (msubst f1 x v))
 372   | (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
 373   end.
 374
 375 (* Why3 assumption *)
 376 Fixpoint fresh_in_term (id:ident) (t:term) {struct t}: Prop :=
 377   match t with
 378   | ((Tvalue _)|(Tderef _)) => True
 379   | (Tvar i) => ~ (id = i)
 380   | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
 381   end.
 382
 383 (* Why3 assumption *)
 384 Fixpoint fresh_in_fmla (id:ident) (f:fmla) {struct f}: Prop :=
 385   match f with
 386   | (Fterm e) => (fresh_in_term id e)
 387   | ((Fand f1 f2)|(Fimplies f1 f2)) => (fresh_in_fmla id f1) /\
 388       (fresh_in_fmla id f2)
 389   | (Fnot f1) => (fresh_in_fmla id f1)
 390   | (Flet y t f1) => (~ (id = y)) /\ ((fresh_in_term id t) /\ (fresh_in_fmla
 391       id f1))
 392   | (Fforall y _ f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
 393   end.
 394
 395 Axiom eval_msubst_term : forall (e:term) (sigma:(map.Map.map mident value))
 396   (pi:(list (ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v
 397   e) -> ((eval_term sigma pi (msubst_term e x
 398   v)) = (eval_term (map.Map.set sigma x (get_stack v pi)) pi e)).
 399
 400 Axiom eval_msubst : forall (f:fmla) (sigma:(map.Map.map mident value))
 401   (pi:(list (ident* value)%type)) (x:mident) (v:ident), (fresh_in_fmla v
 402   f) -> ((eval_fmla sigma pi (msubst f x v)) <-> (eval_fmla
 403   (map.Map.set sigma x (get_stack v pi)) pi f)).
 404
 405 Axiom eval_swap_term : forall (t:term) (sigma:(map.Map.map mident value))
 406   (pi:(list (ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
 407   (id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_term sigma
 408   (Init.Datatypes.app l (Init.Datatypes.cons (id1, v1) (Init.Datatypes.cons (
 409   id2, v2) pi))) t) = (eval_term sigma
 410   (Init.Datatypes.app l (Init.Datatypes.cons (id2, v2) (Init.Datatypes.cons (
 411   id1, v1) pi))) t)).
 412
 413 Axiom eval_swap_gen : forall (f:fmla) (sigma:(map.Map.map mident value))
 414   (pi:(list (ident* value)%type)) (l:(list (ident* value)%type)) (id1:ident)
 415   (id2:ident) (v1:value) (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma
 416   (Init.Datatypes.app l (Init.Datatypes.cons (id1, v1) (Init.Datatypes.cons (
 417   id2, v2) pi))) f) <-> (eval_fmla sigma
 418   (Init.Datatypes.app l (Init.Datatypes.cons (id2, v2) (Init.Datatypes.cons (
 419   id1, v1) pi))) f)).
 420
 421 Axiom eval_swap : forall (f:fmla) (sigma:(map.Map.map mident value))
 422   (pi:(list (ident* value)%type)) (id1:ident) (id2:ident) (v1:value)
 423   (v2:value), (~ (id1 = id2)) -> ((eval_fmla sigma (Init.Datatypes.cons (id1,
 424   v1) (Init.Datatypes.cons (id2, v2) pi)) f) <-> (eval_fmla sigma
 425   (Init.Datatypes.cons (id2, v2) (Init.Datatypes.cons (id1, v1) pi)) f)).
 426
 427 Axiom eval_term_change_free : forall (t:term) (sigma:(map.Map.map mident
 428   value)) (pi:(list (ident* value)%type)) (id:ident) (v:value),
 429   (fresh_in_term id t) -> ((eval_term sigma (Init.Datatypes.cons (id, v) pi)
 430   t) = (eval_term sigma pi t)).
 431
 432 Axiom eval_change_free : forall (f:fmla) (sigma:(map.Map.map mident value))
 433   (pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_fmla id
 434   f) -> ((eval_fmla sigma (Init.Datatypes.cons (id, v) pi) f) <-> (eval_fmla
 435   sigma pi f)).
 436
 437 Parameter fresh_from: fmla -> ident.
 438
 439 Axiom fresh_from_fmla : forall (f:fmla), (fresh_in_fmla (fresh_from f) f).
 440
 441 Parameter abstract_effects: stmt -> fmla -> fmla.
 442
 443 Axiom abstract_effects_specialize : forall (sigma:(map.Map.map mident value))
 444   (pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
 445   (abstract_effects s f)) -> (eval_fmla sigma pi f).
 446
 447 Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
 448   (sigma:(map.Map.map mident value)) (pi:(list (ident* value)%type)),
 449   ((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
 450   (abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
 451   q))).
 452
 453 Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
 454   (valid_fmla (Fimplies p q)) -> forall (sigma:(map.Map.map mident value))
 455   (pi:(list (ident* value)%type)), (eval_fmla sigma pi (abstract_effects s
 456   p)) -> (eval_fmla sigma pi (abstract_effects s q)).
 457
 458 (* Why3 assumption *)
 459 Fixpoint wp (s:stmt) (q:fmla) {struct s}: fmla :=
 460   match s with
 461   | Sskip => q
 462   | (Sassert f) => (Fand f (Fimplies f q))
 463   | (Sseq s1 s2) => (wp s1 (wp s2 q))
 464   | (Sassign x t) => let id := (fresh_from q) in (Flet id t (msubst q x id))
 465   | (Sif t s1 s2) => (Fand (Fimplies (Fterm t) (wp s1 q))
 466       (Fimplies (Fnot (Fterm t)) (wp s2 q)))
 467   | (Swhile cond inv body) => (Fand inv (abstract_effects body
 468       (Fand (Fimplies (Fand (Fterm cond) inv) (wp body inv))
 469       (Fimplies (Fand (Fnot (Fterm cond)) inv) q))))
 470   end.
 471
 472 Axiom abstract_effects_writes : forall (sigma:(map.Map.map mident value))
 473   (pi:(list (ident* value)%type)) (body:stmt) (cond:term) (inv:fmla)
 474   (q:fmla), let f := (abstract_effects body
 475   (Fand (Fimplies (Fand (Fterm cond) inv) (wp body inv))
 476   (Fimplies (Fand (Fnot (Fterm cond)) inv) q))) in ((eval_fmla sigma pi f) ->
 477   (eval_fmla sigma pi (wp body f))).
 478
 479 Axiom monotonicity : forall (s:stmt) (p:fmla) (q:fmla), (valid_fmla
 480   (Fimplies p q)) -> (valid_fmla (Fimplies (wp s p) (wp s q))).
 481
 482 Axiom distrib_conj : forall (s:stmt) (sigma:(map.Map.map mident value))
 483   (pi:(list (ident* value)%type)) (p:fmla) (q:fmla), ((eval_fmla sigma pi
 484   (wp s p)) /\ (eval_fmla sigma pi (wp s q))) -> (eval_fmla sigma pi (wp s
 485   (Fand p q))).
 486
 487 Axiom wp_preserved_by_reduction : forall (sigma:(map.Map.map mident value))
 488   (sigma':(map.Map.map mident value)) (pi:(list (ident* value)%type))
 489   (pi':(list (ident* value)%type)) (s:stmt) (s':stmt), (one_step sigma pi s
 490   sigma' pi' s') -> forall (q:fmla), (eval_fmla sigma pi (wp s q)) ->
 491   (eval_fmla sigma' pi' (wp s' q)).
 492
 493 (* Why3 goal *)
 494 Theorem progress : forall (s:stmt), forall (x:term) (x1:fmla) (x2:stmt),
 495   (s = (Swhile x x1 x2)) -> ((forall (sigma:(map.Map.map mident value))
 496   (pi:(list (ident* value)%type)) (sigmat:(map.Map.map mident datatype))
 497   (pit:(list (ident* datatype)%type)) (q:fmla), (compatible_env sigma sigmat
 498   pi pit) -> ((type_stmt sigmat pit x2) -> ((eval_fmla sigma pi (wp x2 q)) ->
 499   ((~ (x2 = Sskip)) -> (reductible sigma pi x2))))) ->
 500   forall (sigma:(map.Map.map mident value)) (pi:(list (ident* value)%type))
 501   (sigmat:(map.Map.map mident datatype)) (pit:(list (ident* datatype)%type))
 502   (q:fmla), (compatible_env sigma sigmat pi pit) -> ((type_stmt sigmat pit
 503   s) -> ((eval_fmla sigma pi (wp s q)) -> ((~ (s = Sskip)) -> (reductible
 504   sigma pi s))))).
 505 (* Why3 intros s x x1 x2 h1 h2 sigma pi sigmat pit q h3 h4 h5 h6. *)
 506 intros s x x1 x2 H_;rewrite H_ in *.
 507 simpl.
 508 intros H sigma pi sigmat pit q H1 H2 (H3 & H4) H5.
 509 inversion H2; subst; clear H2.
 510 unfold reductible.
 511 apply eval_type_term with (sigma := sigma) (pi := pi) in H11 ; auto.
 512 assert (eval_term sigma pi x = Vbool true \/
 513         eval_term sigma pi x = Vbool false).
 514 generalize (type_inversion (eval_term sigma pi x)).
 515 destruct (eval_term sigma pi x); simpl;  try discriminate.
 516 destruct b; auto.
 517 destruct H0.
 518 do 3 eexists.
 519 apply one_step_while_true; auto.
 520 do 3 eexists.
 521 apply one_step_while_false; auto.
 522 Qed.
 523