(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require map.Map.
Require bool.Bool.

(* Why3 assumption *)
Inductive datatype :=
  | Tint : datatype
  | Tbool : datatype.
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.

(* Why3 assumption *)
Inductive operator :=
  | Oplus : operator
  | Ominus : operator
  | Omult : operator
  | Ole : operator.
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.

(* Why3 assumption *)
Definition ident := Z.

(* Why3 assumption *)
Inductive term :=
  | Tconst : Z -> term
  | Tvar : Z -> term
  | Tderef : Z -> term
  | Tbin : term -> operator -> term -> term.
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.

(* Why3 assumption *)
Inductive fmla :=
  | Fterm : term -> fmla
  | Fand : fmla -> fmla -> fmla
  | Fnot : fmla -> fmla
  | Fimplies : fmla -> fmla -> fmla
  | Flet : Z -> term -> fmla -> fmla
  | Fforall : Z -> datatype -> fmla -> fmla.
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.

(* Why3 assumption *)
Inductive value :=
  | Vint : Z -> value
  | Vbool : bool -> value.
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.

(* Why3 assumption *)
Definition env := Z -> value.

Parameter eval_bin: value -> operator -> value -> value.

Axiom eval_bin_def :
  forall (x:value) (op:operator) (y:value),
  match (x, y) with
  | ((Vint x1), (Vint y1)) =>
      match op with
      | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
      | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
      | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
      | Ole =>
          ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
          (~ (x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool false)))
      end
  | (_, _) => ((eval_bin x op y) = (Vbool false))
  end.

(* Why3 assumption *)
Fixpoint eval_term (sigma:Z -> value) (pi:Z -> value)
  (t:term) {struct t}: value :=
  match t with
  | (Tconst n) => Vint n
  | (Tvar id) => pi id
  | (Tderef id) => sigma id
  | (Tbin t1 op t2) =>
      eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
  end.

(* Why3 assumption *)
Fixpoint eval_fmla (sigma:Z -> value) (pi:Z -> value)
  (f:fmla) {struct f}: Prop :=
  match f with
  | (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
  | (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
  | (Fnot f1) => ~ (eval_fmla sigma pi f1)
  | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> eval_fmla sigma pi f2
  | (Flet x t f1) =>
      eval_fmla sigma (map.Map.set pi x (eval_term sigma pi t)) f1
  | (Fforall x Tint f1) =>
      forall (n:Z), eval_fmla sigma (map.Map.set pi x (Vint n)) f1
  | (Fforall x Tbool f1) =>
      forall (b:bool), eval_fmla sigma (map.Map.set pi x (Vbool b)) f1
  end.

Parameter subst_term: term -> Z -> Z -> term.

Axiom subst_term_def :
  forall (e:term) (r:Z) (v:Z),
  match e with
  | (Tconst _) => ((subst_term e r v) = e)
  | (Tvar _) => ((subst_term e r v) = e)
  | (Tderef x) =>
      ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
      (~ (r = x) -> ((subst_term e r v) = e))
  | (Tbin e1 op e2) =>
      ((subst_term e r v) =
       (Tbin (subst_term e1 r v) op (subst_term e2 r v)))
  end.

(* Why3 assumption *)
Fixpoint fresh_in_term (id:Z) (t:term) {struct t}: Prop :=
  match t with
  | (Tconst _) => True
  | (Tvar v) => ~ (id = v)
  | (Tderef _) => True
  | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
  end.

Axiom eval_subst_term :
  forall (sigma:Z -> value) (pi:Z -> value) (e:term) (x:Z) (v:Z),
  (fresh_in_term v e) ->
  ((eval_term sigma pi (subst_term e x v)) =
   (eval_term (map.Map.set sigma x (pi v)) pi e)).

Axiom eval_term_change_free :
  forall (t:term) (sigma:Z -> value) (pi:Z -> value) (id:Z) (v:value),
  (fresh_in_term id t) ->
  ((eval_term sigma (map.Map.set pi id v) t) = (eval_term sigma pi t)).

(* Why3 assumption *)
Fixpoint fresh_in_fmla (id:Z) (f:fmla) {struct f}: Prop :=
  match f with
  | (Fterm e) => fresh_in_term id e
  | ((Fand f1 f2)|(Fimplies f1 f2)) =>
      (fresh_in_fmla id f1) /\ (fresh_in_fmla id f2)
  | (Fnot f1) => fresh_in_fmla id f1
  | (Flet y t f1) =>
      ~ (id = y) /\ ((fresh_in_term id t) /\ (fresh_in_fmla id f1))
  | (Fforall y _ f1) => ~ (id = y) /\ (fresh_in_fmla id f1)
  end.

(* Why3 assumption *)
Fixpoint subst (f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
  match f with
  | (Fterm e) => Fterm (subst_term e x v)
  | (Fand f1 f2) => Fand (subst f1 x v) (subst f2 x v)
  | (Fnot f1) => Fnot (subst f1 x v)
  | (Fimplies f1 f2) => Fimplies (subst f1 x v) (subst f2 x v)
  | (Flet y t f1) => Flet y (subst_term t x v) (subst f1 x v)
  | (Fforall y ty f1) => Fforall y ty (subst f1 x v)
  end.

Axiom eval_subst :
  forall (f:fmla) (sigma:Z -> value) (pi:Z -> value) (x:Z) (v:Z),
  (fresh_in_fmla v f) ->
  (eval_fmla sigma pi (subst f x v)) <->
  (eval_fmla (map.Map.set sigma x (pi v)) pi f).

Axiom eval_swap :
  forall (f:fmla) (sigma:Z -> value) (pi:Z -> value) (id1:Z) (id2:Z)
    (v1:value) (v2:value),
  ~ (id1 = id2) ->
  (eval_fmla sigma (map.Map.set (map.Map.set pi id1 v1) id2 v2) f) <->
  (eval_fmla sigma (map.Map.set (map.Map.set pi id2 v2) id1 v1) f).

Axiom eval_change_free :
  forall (f:fmla) (sigma:Z -> value) (pi:Z -> value) (id:Z) (v:value),
  (fresh_in_fmla id f) ->
  (eval_fmla sigma (map.Map.set pi id v) f) <-> (eval_fmla sigma pi f).

(* Why3 assumption *)
Inductive stmt :=
  | Sskip : stmt
  | Sassign : Z -> term -> stmt
  | Sseq : stmt -> stmt -> stmt
  | Sif : term -> stmt -> stmt -> stmt
  | Sassert : fmla -> stmt
  | Swhile : term -> fmla -> stmt -> stmt.
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.

Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).

(* Why3 assumption *)
Inductive one_step: (Z -> value) -> (Z -> value) -> stmt -> (Z -> value) ->
  (Z -> value) -> stmt -> Prop :=
  | one_step_assign :
      forall (sigma:Z -> value) (pi:Z -> value) (x:Z) (e:term),
      one_step sigma pi (Sassign x e)
      (map.Map.set sigma x (eval_term sigma pi e)) pi Sskip
  | one_step_seq :
      forall (sigma:Z -> value) (pi:Z -> value) (sigma':Z -> value)
        (pi':Z -> value) (i1:stmt) (i1':stmt) (i2:stmt),
      (one_step sigma pi i1 sigma' pi' i1') ->
      one_step sigma pi (Sseq i1 i2) sigma' pi' (Sseq i1' i2)
  | one_step_seq_skip :
      forall (sigma:Z -> value) (pi:Z -> value) (i:stmt),
      one_step sigma pi (Sseq Sskip i) sigma pi i
  | one_step_if_true :
      forall (sigma:Z -> value) (pi:Z -> value) (e:term) (i1:stmt) (i2:stmt),
      ((eval_term sigma pi e) = (Vbool true)) ->
      one_step sigma pi (Sif e i1 i2) sigma pi i1
  | one_step_if_false :
      forall (sigma:Z -> value) (pi:Z -> value) (e:term) (i1:stmt) (i2:stmt),
      ((eval_term sigma pi e) = (Vbool false)) ->
      one_step sigma pi (Sif e i1 i2) sigma pi i2
  | one_step_assert :
      forall (sigma:Z -> value) (pi:Z -> value) (f:fmla),
      (eval_fmla sigma pi f) -> one_step sigma pi (Sassert f) sigma pi Sskip
  | one_step_while_true :
      forall (sigma:Z -> value) (pi:Z -> value) (e:term) (inv:fmla) (i:stmt),
      (eval_fmla sigma pi inv) -> ((eval_term sigma pi e) = (Vbool true)) ->
      one_step sigma pi (Swhile e inv i) sigma pi (Sseq i (Swhile e inv i))
  | one_step_while_false :
      forall (sigma:Z -> value) (pi:Z -> value) (e:term) (inv:fmla) (i:stmt),
      (eval_fmla sigma pi inv) -> ((eval_term sigma pi e) = (Vbool false)) ->
      one_step sigma pi (Swhile e inv i) sigma pi Sskip.

(* Why3 assumption *)
Inductive many_steps: (Z -> value) -> (Z -> value) -> stmt -> (Z -> value) ->
  (Z -> value) -> stmt -> Z -> Prop :=
  | many_steps_refl :
      forall (sigma:Z -> value) (pi:Z -> value) (i:stmt),
      many_steps sigma pi i sigma pi i 0%Z
  | many_steps_trans :
      forall (sigma1:Z -> value) (pi1:Z -> value) (sigma2:Z -> value)
        (pi2:Z -> value) (sigma3:Z -> value) (pi3:Z -> value) (i1:stmt)
        (i2:stmt) (i3:stmt) (n:Z),
      (one_step sigma1 pi1 i1 sigma2 pi2 i2) ->
      (many_steps sigma2 pi2 i2 sigma3 pi3 i3 n) ->
      many_steps sigma1 pi1 i1 sigma3 pi3 i3 (n + 1%Z)%Z.

Axiom steps_non_neg :
  forall (sigma1:Z -> value) (pi1:Z -> value) (sigma2:Z -> value)
    (pi2:Z -> value) (i1:stmt) (i2:stmt) (n:Z),
  (many_steps sigma1 pi1 i1 sigma2 pi2 i2 n) -> (0%Z <= n)%Z.

Axiom many_steps_seq :
  forall (sigma1:Z -> value) (pi1:Z -> value) (sigma3:Z -> value)
    (pi3:Z -> value) (i1:stmt) (i2:stmt) (n:Z),
  (many_steps sigma1 pi1 (Sseq i1 i2) sigma3 pi3 Sskip n) ->
  exists sigma2:Z -> value, exists pi2:Z -> value, exists n1:Z, exists n2:
  Z,
  (many_steps sigma1 pi1 i1 sigma2 pi2 Sskip n1) /\
  ((many_steps sigma2 pi2 i2 sigma3 pi3 Sskip n2) /\
   (n = ((1%Z + n1)%Z + n2)%Z)).

(* Why3 assumption *)
Definition valid_fmla (p:fmla) : Prop :=
  forall (sigma:Z -> value) (pi:Z -> value), eval_fmla sigma pi p.

(* Why3 assumption *)
Definition valid_triple (p:fmla) (i:stmt) (q:fmla) : Prop :=
  forall (sigma:Z -> value) (pi:Z -> value), (eval_fmla sigma pi p) ->
  forall (sigma':Z -> value) (pi':Z -> value) (n:Z),
  (many_steps sigma pi i sigma' pi' Sskip n) -> eval_fmla sigma' pi' q.

Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.

Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.

Parameter infix_eqeq:
  forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> Prop.

Axiom infix_eqeq_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a),
  (infix_eqeq s1 s2) <-> forall (x:a), (mem x s1) <-> (mem x s2).

Axiom extensionality :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), (infix_eqeq s1 s2) -> (s1 = s2).

Parameter subset:
  forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> Prop.

Axiom subset_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a),
  (subset s1 s2) <-> forall (x:a), (mem x s1) -> mem x s2.

Axiom subset_refl :
  forall {a:Type} {a_WT:WhyType a}, forall (s:set a), subset s s.

Axiom subset_trans :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a) (s3:set a), (subset s1 s2) ->
  (subset s2 s3) -> subset s1 s3.

Parameter is_empty: forall {a:Type} {a_WT:WhyType a}, (set a) -> Prop.

Axiom is_empty_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s:set a), (is_empty s) <-> forall (x:a), ~ (mem x s).

Parameter empty: forall {a:Type} {a_WT:WhyType a}, set a.

Axiom empty_def : forall {a:Type} {a_WT:WhyType a}, is_empty (empty : set a).

Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> set a.

Axiom add_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (s:set a), forall (y:a),
  (mem y (add x s)) <-> ((y = x) \/ (mem y s)).

Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> set a.

Axiom remove_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (s:set a), forall (y:a),
  (mem y (remove x s)) <-> (~ (y = x) /\ (mem y s)).

Axiom add_remove :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (s:set a), (mem x s) -> ((add x (remove x s)) = s).

Axiom remove_add :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (s:set a), ((remove x (add x s)) = (remove x s)).

Axiom subset_remove :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a) (s:set a), subset (remove x s) s.

Parameter union:
  forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> set a.

Axiom union_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), forall (x:a),
  (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).

Parameter inter:
  forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> set a.

Axiom inter_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), forall (x:a),
  (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).

Parameter diff:
  forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> set a.

Axiom diff_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), forall (x:a),
  (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).

Axiom subset_diff :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), subset (diff s1 s2) s1.

Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.

Axiom choose_spec :
  forall {a:Type} {a_WT:WhyType a},
  forall (s:set a), ~ (is_empty s) -> mem (choose s) s.

Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.

Axiom cardinal_nonneg :
  forall {a:Type} {a_WT:WhyType a},
  forall (s:set a), (0%Z <= (cardinal s))%Z.

Axiom cardinal_empty :
  forall {a:Type} {a_WT:WhyType a},
  forall (s:set a), ((cardinal s) = 0%Z) <-> (is_empty s).

Axiom cardinal_add :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a), forall (s:set a), ~ (mem x s) ->
  ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).

Axiom cardinal_remove :
  forall {a:Type} {a_WT:WhyType a},
  forall (x:a), forall (s:set a), (mem x s) ->
  ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).

Axiom cardinal_subset :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), (subset s1 s2) ->
  ((cardinal s1) <= (cardinal s2))%Z.

Axiom subset_eq :
  forall {a:Type} {a_WT:WhyType a},
  forall (s1:set a) (s2:set a), (subset s1 s2) ->
  ((cardinal s1) = (cardinal s2)) -> infix_eqeq s1 s2.

Axiom cardinal1 :
  forall {a:Type} {a_WT:WhyType a},
  forall (s:set a), ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) ->
  (x = (choose s)).

(* Why3 assumption *)
Definition assigns (sigma:Z -> value) (a:set Z) (sigma':Z -> value) : Prop :=
  forall (i:Z), ~ (mem i a) -> ((sigma i) = (sigma' i)).

Axiom assigns_refl :
  forall (sigma:Z -> value) (a:set Z), assigns sigma a sigma.

Axiom assigns_trans :
  forall (sigma1:Z -> value) (sigma2:Z -> value) (sigma3:Z -> value)
    (a:set Z),
  ((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) ->
  assigns sigma1 a sigma3.

Axiom assigns_union_left :
  forall (sigma:Z -> value) (sigma':Z -> value) (s1:set Z) (s2:set Z),
  (assigns sigma s1 sigma') -> assigns sigma (union s1 s2) sigma'.

Axiom assigns_union_right :
  forall (sigma:Z -> value) (sigma':Z -> value) (s1:set Z) (s2:set Z),
  (assigns sigma s2 sigma') -> assigns sigma (union s1 s2) sigma'.

(* Why3 assumption *)
Fixpoint stmt_writes (i:stmt) (w:set Z) {struct i}: Prop :=
  match i with
  | (Sskip|(Sassert _)) => True
  | (Sassign id _) => mem id w
  | ((Sseq s1 s2)|(Sif _ s1 s2)) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
  | (Swhile _ _ s) => stmt_writes s w
  end.

(* Why3 goal *)
Theorem VC_compute_writes :
  forall (s:stmt), forall (result:set Z),
  (exists x:term, exists x1:fmla, exists x2:stmt,
   (s = (Swhile x x1 x2)) /\
   forall (sigma:Z -> value) (pi:Z -> value) (sigma':Z -> value)
     (pi':Z -> value) (n:Z),
   (many_steps sigma pi x2 sigma' pi' Sskip n) -> assigns sigma result sigma') ->
  forall (sigma:Z -> value) (pi:Z -> value) (sigma':Z -> value)
    (pi':Z -> value) (n:Z),
  (many_steps sigma pi s sigma' pi' Sskip n) -> assigns sigma result sigma'.
(* Why3 intros s result (x,(x1,(x2,(h1,h2)))) sigma pi sigma' pi' n h3. *)
intros s result (x,(x1,(x2,(h1,h2)))); rewrite h1 in *. intros.
generalize sigma pi sigma' pi' H.
generalize (steps_non_neg _ _ _ _ _ _ _ H).
clear sigma pi sigma' pi' H.
intro H_n_pos.
pattern n.
apply Z_lt_induction; auto.
intros x3 Hind sigma pi sigma' qt' Hsteps.
inversion Hsteps; subst; clear Hsteps.
inversion H; subst; clear H.

generalize (many_steps_seq _ _ _ _ _ _ _ H0).
intros (sigma3&pi3&n1&n2&h3&h4&h5).
apply assigns_trans with sigma3; split.
eapply h2; eauto.
eapply Hind; eauto.
generalize (steps_non_neg _ _ _ _ _ _ _ h3).
generalize (steps_non_neg _ _ _ _ _ _ _ h4).
omega.

inversion H0; subst; clear H0.
apply assigns_refl.
inversion H.
Qed.