Require Import VST.floyd.proofauto.
Require Import VST.progs.dotprod.

Instance CompSpecs : compspecs.
(* Goal: compspecs *)
Proof. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.


Local Open Scope logic.

(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (Vfloat (@Znth float Inhabitant_float i fy)) (Vfloat (@Znth float Inhabitant_float i fz))))))) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) *)
Fixpoint map2 {A B C: Type} (f: A -> B -> C) (al: list A) (bl: list B) : list C :=
 match al, bl with
  | a::al', b::bl' => f a b :: map2 f al' bl'
  | _, _ => nil
  end.

Definition add_spec :=
 DECLARE _add
  WITH x: val, y : val, z: val, fy : list float, fz: list float
  PRE  [_x OF tptr tdouble, _y OF tptr tdouble, _z OF tptr tdouble]
      PROP ()
      LOCAL (temp _x x; temp _y y; temp _z z)
      SEP (data_at_ Tsh (tarray tdouble 3)  x ;
             data_at Tsh (tarray tdouble 3) (map Vfloat fy) y;
             data_at Tsh (tarray tdouble 3) (map Vfloat fz) z)
  POST [ tvoid ]
      PROP ()
      LOCAL ()
      SEP (data_at Tsh (tarray tdouble 3) (map Vfloat (map2 Float.add fy fz)) x;
             data_at Tsh (tarray tdouble 3) (map Vfloat fy) y;
             data_at Tsh (tarray tdouble 3) (map Vfloat fz) z).

Definition dotprod (fx fy : list float) : float :=
  fold_left Float.add (map2 Float.mul fx fy) Float.zero .

Definition dotprod_spec :=
 DECLARE _dotprod
  WITH n: Z, x: val, y : val, fx : list float, fy: list float, sh: share
  PRE  [_n OF tint, _x OF tptr tdouble, _y OF tptr tdouble]
      PROP (0 <= n < Int.max_signed)
      LOCAL (temp _n (Vint (Int.repr n)); temp _x x; temp _y y)
      SEP (data_at Tsh (tarray tdouble n) (map Vfloat fx) x;
             data_at Tsh (tarray tdouble n) (map Vfloat fy) y)
  POST [ tdouble ]
      PROP ()
      LOCAL (temp ret_temp (Vfloat (dotprod fx fy)))
      SEP (data_at Tsh (tarray tdouble n) (map Vfloat fx) x;
             data_at Tsh (tarray tdouble n) (map Vfloat fy) y).


Definition Gprog : funspecs :=   ltac:(with_library prog [add_spec; dotprod_spec]).

Lemma map2_app:
 forall (A B C: Type) (f: A -> B -> C) al al' bl bl',
  Zlength al = Zlength bl ->
  Zlength al' = Zlength bl' ->
   map2 f (al ++ al') (bl ++ bl') = map2 f al bl ++ map2 f al' bl'.
Proof.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
intros.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
rewrite !Zlength_correct in *.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
apply Nat2Z.inj in H. apply Nat2Z.inj in H0.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
revert bl H al' bl' H0; induction al; intros.
*
(* Goal: @eq C (@nth C (S j) (@map2 A B C f (@cons A a0 al) bl) c) (f (@nth A (S j) (@cons A a0 al) a) (@nth B (S j) bl b)) *)
destruct bl; inv H.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl. auto.
*
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B bl bl')) (@app C (@map2 A B C f (@cons A a al) bl) (@map2 A B C f al' bl')) *)
destruct bl.
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@nil B) bl')) (@app C (@map2 A B C f (@cons A a al) (@nil B)) (@map2 A B C f al' bl')) *)
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@cons B b bl) bl')) (@app C (@map2 A B C f (@cons A a al) (@cons B b bl)) (@map2 A B C f al' bl')) *)
inv H.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
f_equal.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
auto.
Qed.

Lemma Zlength_map2: forall A B C (f: A -> B -> C) fy fz,
  Zlength fy = Zlength fz -> Zlength (map2 f fy fz) = Zlength fy.
Proof.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
intros.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
rewrite !Zlength_correct in *.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
apply Nat2Z.inj in H. f_equal.
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@nil B) bl')) (@app C (@map2 A B C f (@cons A a al) (@nil B)) (@map2 A B C f al' bl')) *)
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@cons B b bl) bl')) (@app C (@map2 A B C f (@cons A a al) (@cons B b bl)) (@map2 A B C f al' bl')) *)
revert fz H; induction fy; destruct fz; intros; inv H.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
auto.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl. f_equal; auto.
Qed.

Lemma Znth_map2:
 forall A B C (a: Inhabitant A) (b: Inhabitant B) (c: Inhabitant C) (f: A -> B -> C) (al: list A) (bl: list B) i,
  Zlength al = Zlength bl ->
  0 <= i < Zlength al ->
  Znth i (map2 f al bl) = f (Znth i al) (Znth i bl).
Proof.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
intros.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
rewrite !Zlength_correct in *.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
apply Nat2Z.inj in H. f_equal.
(* Goal: @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
unfold Znth.
(* Goal: @eq C (if zlt i Z0 then @default C c else @nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (if zlt i Z0 then @default A a else @nth A (Z.to_nat i) al a) (if zlt i Z0 then @default B b else @nth B (Z.to_nat i) bl b)) *)
if_tac. omega.
(* Goal: @eq C (@nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (@nth A (Z.to_nat i) al a) (@nth B (Z.to_nat i) bl b)) *)
assert (Z.to_nat i < length al)%nat.
(* Goal: lt (Z.to_nat i) (@Datatypes.length A al) *)
(* Goal: @eq C (@nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (@nth A (Z.to_nat i) al a) (@nth B (Z.to_nat i) bl b)) *)
rewrite <- (Nat2Z.id (length al)).
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
apply Z2Nat.inj_lt; try omega.
(* Goal: @eq C (@nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (@nth A (Z.to_nat i) al a) (@nth B (Z.to_nat i) bl b)) *)
clear H0 H1.
(* Goal: @eq C (@nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (@nth A (Z.to_nat i) al a) (@nth B (Z.to_nat i) bl b)) *)
forget (Z.to_nat i) as j. clear i.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
revert al bl H H2; induction j; intros.
(* Goal: @eq C (@nth C O (@map2 A B C f al bl) c) (f (@nth A O al a) (@nth B O bl b)) *)
(* Goal: @eq C (@nth C (S j) (@map2 A B C f al bl) c) (f (@nth A (S j) al a) (@nth B (S j) bl b)) *)
destruct al; inv H2.
(* Goal: @eq C (@nth C (S j) (@map2 A B C f (@cons A a0 al) bl) c) (f (@nth A (S j) (@cons A a0 al) a) (@nth B (S j) bl b)) *)
destruct bl; inv H.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl. auto.
(* Goal: @eq C (@nth C (S j) (@map2 A B C f (@cons A a0 al) bl) c) (f (@nth A (S j) (@cons A a0 al) a) (@nth B (S j) bl b)) *)
destruct bl; inv H.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl. auto.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
destruct al; simpl in H2; try omega.
(* Goal: @eq C (@nth C (S j) (@map2 A B C f (@cons A a0 al) bl) c) (f (@nth A (S j) (@cons A a0 al) a) (@nth B (S j) bl b)) *)
destruct bl; inv H.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
apply IHj; auto.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
omega.
Qed.

Lemma body_dotprod:  semax_body Vprog Gprog f_dotprod dotprod_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_add add_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble n) (@map float val Vfloat fx) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble n) (@map float val Vfloat fy) y) (@nil mpred)))))) (Ssequence (Sset _sum (Econst_float (Float.of_bits (Int64.repr Z0)) tdouble)) MORE_COMMANDS) POSTCONDITION *)
name n_ _n.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name i_ _i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name x_ _x.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name y_ _y.
forward. (* sum = 0.0; *)
forward_for_simple_bound n
   (EX i:Z,
      PROP ()
      LOCAL (temp _sum (Vfloat (dotprod (sublist 0 i fx) (sublist 0 i fy))); temp _x x; temp _y y; temp _n (Vint (Int.repr n)))
      SEP (data_at Tsh (tarray tdouble n) (map Vfloat fx) x;
             data_at Tsh (tarray tdouble n) (map Vfloat fy) y)).
* (* initializer *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
entailer!.
* (* body *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _sum (Vfloat (dotprod (@sublist float Z0 i fx) (@sublist float Z0 i fy)))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble n) (@map float val Vfloat fx) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble n) (@map float val Vfloat fy) y) (@nil mpred)))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength fx = n /\ Zlength fy = n). {
    entailer!. autorewrite with sublist in *; split; auto.
} destruct H1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward. 
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
rewrite !Znth_map by omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward. 
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
  entailer!.
  autorewrite with sublist in *.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
  f_equal.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
  rewrite (sublist_split 0 i _ fx) by omega.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
  rewrite (sublist_split 0 i _ fy) by omega.
(* Goal: @eq float (dotprod (@app float (@sublist float Z0 i fx) (@sublist float i (Z.add i (Zpos xH)) fx)) (@app float (@sublist float Z0 i fy) (@sublist float i (Z.add i (Zpos xH)) fy))) (Float.add (dotprod (@sublist float Z0 i fx) (@sublist float Z0 i fy)) (Float.mul (@Znth float Inhabitant_float i fx) (@Znth float Inhabitant_float i fy))) *)
  unfold dotprod.
(* Goal: @eq float (@fold_left float float Float.add (@map2 float float float Float.mul (@app float (@sublist float Z0 i fx) (@sublist float i (Z.add i (Zpos xH)) fx)) (@app float (@sublist float Z0 i fy) (@sublist float i (Z.add i (Zpos xH)) fy))) Float.zero) (Float.add (@fold_left float float Float.add (@map2 float float float Float.mul (@sublist float Z0 i fx) (@sublist float Z0 i fy)) Float.zero) (Float.mul (@Znth float Inhabitant_float i fx) (@Znth float Inhabitant_float i fy))) *)
 rewrite map2_app by list_solve.
(* Goal: @eq float (@fold_left float float Float.add (@app float (@map2 float float float Float.mul (@sublist float Z0 i fx) (@sublist float Z0 i fy)) (@map2 float float float Float.mul (@sublist float i (Z.add i (Zpos xH)) fx) (@sublist float i (Z.add i (Zpos xH)) fy))) Float.zero) (Float.add (@fold_left float float Float.add (@map2 float float float Float.mul (@sublist float Z0 i fx) (@sublist float Z0 i fy)) Float.zero) (Float.mul (@Znth float Inhabitant_float i fx) (@Znth float Inhabitant_float i fy))) *)
 rewrite fold_left_app.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@sublist val (Zpos xH) (@Zlength val (@cons val Vundef (@nil val))) (@cons val Vundef (@nil val)))) (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 rewrite !sublist_len_1 by list_solve.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 simpl. auto.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
 forward.
 autorewrite with sublist in *.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 autorewrite with sublist.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
 entailer!.
Qed.

Lemma body_add:  semax_body Vprog Gprog f_add add_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_add add_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name i_ _i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name x_ _x.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name y_ _y.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name z_ _z.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
pose (fx := map2 Float.add fy fz).
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (Vfloat (@Znth float Inhabitant_float i fy)) (Vfloat (@Znth float Inhabitant_float i fz))))))) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) *)
assert_PROP (Zlength fx = 3 /\ Zlength fy = 3 /\ Zlength fz = 3). {
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
  entailer!.
  autorewrite with sublist in *.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  split3; auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fx) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  subst fx. clear - H1 H4.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  rewrite Zlength_map2 by omega; auto.
} destruct H as [Hx [Hy Hz]].
forward_for_simple_bound 3
   (EX i:Z,
      PROP ()
      LOCAL (temp _x x; temp _y y; temp _z z)
      SEP (data_at Tsh (tarray tdouble 3) 
          (map Vfloat (sublist 0 i fx) ++ list_repeat (Z.to_nat (3-i)) Vundef) x;
   data_at Tsh (tarray tdouble 3) (map Vfloat fy) y;
   data_at Tsh (tarray tdouble 3) (map Vfloat fz) z)).
* (* initializer *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
entailer!. simpl; entailer!.
* (* body *)
forward. (* x[i] = y[i] + z[i]; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (@Znth val Vundef i (@map float val Vfloat fz))) (@cons localdef (temp _t'1 (@Znth val Vundef i (@map float val Vfloat fy))) (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (@Znth val Vundef i (@map float val Vfloat fy)) (@Znth val Vundef i (@map float val Vfloat fz))))))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) *)
entailer!. {
  autorewrite with sublist in *.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
  simpl.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@upd_Znth val Z0 (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))))) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) *)
  unfold data_at.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
  apply derives_refl'. f_equal.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: @eq (list val) (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@upd_Znth val Z0 (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))))) (@app val (@map float val Vfloat (@app float (@sublist float Z0 i fx) (@sublist float i (Z.add i (Zpos xH)) fx))) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) *)
 rewrite map_app.
(* Goal: @eq (list val) (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@upd_Znth val Z0 (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))))) (@app val (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx))) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) *)
 rewrite <- app_assoc.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 f_equal.
(* Goal: @eq (list val) (@upd_Znth val Z0 (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz)))) (@app val (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) *)
 replace (Z.to_nat (3-i)) with (Init.Nat.add (Z.to_nat 1) (Z.to_nat (3-(i+1)))).
(* Goal: @eq (list val) (@upd_Znth val Z0 (@list_repeat val (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz)))) (@app val (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 rewrite <-list_repeat_app.
(* Goal: @eq (list val) (@upd_Znth val Z0 (@app val (@list_repeat val (Z.to_nat (Zpos xH)) Vundef) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz)))) (@app val (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 rewrite upd_Znth_app1 by list_solve.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 f_equal.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 autorewrite with sublist.
(* Goal: @eq (list val) (@upd_Znth val Z0 (@list_repeat val (Z.to_nat (Zpos xH)) Vundef) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz)))) (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 simpl list_repeat.
(* Goal: @eq (list val) (@upd_Znth val Z0 (@cons val Vundef (@nil val)) (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz)))) (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 rewrite upd_Znth0.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@sublist val (Zpos xH) (@Zlength val (@cons val Vundef (@nil val))) (@cons val Vundef (@nil val)))) (@map float val Vfloat (@sublist float i (Z.add i (Zpos xH)) fx)) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 rewrite !sublist_len_1 by list_solve.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 autorewrite with sublist.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 simpl. 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fx) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 subst fx.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
  f_equal. f_equal.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
 rewrite Znth_map2 with (a:=Float.zero) (b:=Float.zero) (c:=Float.zero); try omega.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 auto.
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
 rewrite <- Z2Nat.inj_add by omega.
(* Goal: @eq nat (Z.to_nat (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
 f_equal. omega.
}
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
 autorewrite with sublist. subst fx. auto.
Qed.

Definition Svector_add (n: Z) (_i _x _y _z : ident) :=
   Ssequence (Sset _i (Econst_int (Int.repr 0) tint))
     (Sloop
        (Ssequence
           (Sifthenelse
              (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr n) tint) tint)
              Sskip
              Sbreak)
           (Sassign
              (Ederef
                 (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint)
                    (tptr tdouble)) tdouble)
              (Ebinop Oadd
                 (Ederef
                    (Ebinop Oadd (Etempvar _y (tptr tdouble))
                       (Etempvar _i tint) (tptr tdouble)) tdouble)
                 (Ederef
                    (Ebinop Oadd (Etempvar _z (tptr tdouble))
                       (Etempvar _i tint) (tptr tdouble)) tdouble) tdouble)))
        (Sset _i
           (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint)
              tint))).

Definition vector_add (fx fy: Z -> float) i :=
    Float.add (fx i) (fy i).

(*
Lemma semax_vector_add:
    forall (lx ly lz sx sy sz: nat)
              (n: Z) Espec Delta P Q R  (_i _x _y _z : ident) (x y z: val) (fx: Z -> val) (fy fz : Z -> float),
    typeof_temp Delta _i = Some tint ->
    Forall (closed_wrt_vars (eq _i)) Q ->
    Forall (closed_wrt_vars (eq _i)) R ->
    (0 <= n <= Int.max_signed) ->
    nth_error Q lx = Some (`(eq x) (eval_id _x)) ->
    nth_error Q ly = Some (`(eq y) (eval_id _y)) ->
    nth_error Q lz = Some (`(eq z) (eval_id _z)) ->
    nth_error R sx = Some (`(array_at tdouble Tsh fx 0 n x)) ->
    nth_error R sy = Some (`(array_at tdouble Tsh (Vfloat oo fy) 0 n y)) ->
    nth_error R sz = Some (`(array_at tdouble Tsh (Vfloat oo fz) 0 n z)) ->
    sx <> sy ->
    sx <> sz ->
   @semax Espec Delta
        (PROPx P (LOCALx Q (SEPx R)))
        (Svector_add n _i _x _y _z)
        (normal_ret_assert
         (PROPx P (LOCALx Q
          (SEPx  (replace_nth sx R
             (`(array_at tdouble Tsh (Vfloat oo (vector_add fy fz)) 0 n x))))))).
Proof.
intros until 4. intros Jx Jy Jz H3 H4 H5 Ny Nz.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (Vfloat (@Znth float Inhabitant_float i fy)) (Vfloat (@Znth float Inhabitant_float i fz))))))) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) *)
assert (Ti: (temp_types (initialized _i Delta)) ! _i = Some (tint, true)). {
clear - H. unfold typeof_temp in H.
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@nil B) bl')) (@app C (@map2 A B C f (@cons A a al) (@nil B)) (@map2 A B C f al' bl')) *)
(* Goal: @eq (list C) (@map2 A B C f (@app A (@cons A a al) al') (@app B (@cons B b bl) bl')) (@app C (@map2 A B C f (@cons A a al) (@cons B b bl)) (@map2 A B C f al' bl')) *)
destruct ((temp_types Delta) ! _i) eqn:?; inv H. destruct p.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
inv H1. eapply temp_types_init_same; eauto.
}
apply semax_pre0 with
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@upd_Znth val i (@app val (@map float val Vfloat (@sublist float Z0 i fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) i)) Vundef)) (force_val (sem_cast_f2f (force_val (both_float (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) sem_cast_f2f sem_cast_f2f (Vfloat (@Znth float Inhabitant_float i fy)) (Vfloat (@Znth float Inhabitant_float i fz))))))) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Z.add i (Zpos xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) Vundef)) x) *)
 (PROPx (isptr x :: isptr y :: isptr z :: P) (LOCALx Q (SEPx R))). {
repeat rewrite <- insert_prop.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
repeat rewrite <- andp_assoc. apply andp_right; auto.
repeat apply andp_right.
rewrite (replace_nth_nth_error _ _ _ H3).
erewrite SEP_replace_nth_isolate by (eapply H3).
go_lowerx; normalize; rewrite array_at_isptr; normalize.
rewrite (replace_nth_nth_error _ _ _ H4).
erewrite SEP_replace_nth_isolate by (eapply H4).
go_lowerx; normalize; rewrite array_at_isptr; normalize.
rewrite (replace_nth_nth_error _ _ _ H5).
erewrite SEP_replace_nth_isolate by (eapply H5).
go_lowerx; normalize; rewrite array_at_isptr; normalize.
}
repeat rewrite <- insert_prop.
apply semax_extract_prop; intro Px.
apply semax_extract_prop; intro Py.
apply semax_extract_prop; intro Pz.
apply (semax_for_simple_bound_const_init n
   (EX  i : Z, PROPx ((fun _ => P) i)
                  (LOCALx ((fun _ => Q) i)
                  (SEPx ((fun i =>
                 replace_nth sx R
                   (`(array_at tdouble Tsh
                         (fun j => if zlt j i then Vfloat (Float.add (fy j) (fz j)) else fx j) 0 n x))
               ) i))))
     Espec Delta _ (fun _ => P) (fun _ => Q) (fun i =>
                 replace_nth sx R
                   (`(array_at tdouble Tsh (fun j => if zlt j i then Vfloat (Float.add (fy j) (fz j)) else fx j) 0 n x))
               ));
(* Goal: @eq Z (Z.add (Zpos xH) (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH)))) (Z.sub (Zpos (xI xH)) i) *)
  try reflexivity; try auto with closed; try rep_omega.
*
apply andp_left2.
replace (array_at tdouble Tsh
                 (fun j : Z =>
                  if zlt j 0
                  then Vfloat (Float.add (fy j) (fz j))
                  else fx j) 0 n)
 with (array_at tdouble Tsh fx 0 n).
Focus 2.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
simple apply array_at_ext; intros.
rewrite if_false by omega; reflexivity.
rewrite <- (replace_nth_nth_error _ _ _ H3).
rewrite <- insert_local.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
apply andp_right; auto. go_lowerx. normalize.
*
intro i.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
go_lowerx; normalize. apply prop_right. hnf. simpl.
(* Goal: @eq (list val) (@cons val (Vfloat (Float.add (@Znth float Inhabitant_float i fy) (@Znth float Inhabitant_float i fz))) (@nil val)) (@map float val Vfloat (@cons float (@Znth float Inhabitant_float i fx) (@nil float))) *)
(* Goal: @eq nat (Init.Nat.add (Z.to_nat (Zpos xH)) (Z.to_nat (Z.sub (Zpos (xI xH)) (Z.add i (Zpos xH))))) (Z.to_nat (Z.sub (Zpos (xI xH)) i)) *)
rewrite Ti. simpl. apply I.
*
rewrite normal_ret_assert_elim.
drop_LOCAL 0%nat.
drop_LOCAL 0%nat.
apply replace_nth_SEP.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
go_lowerx. apply array_at_ext'; intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
rewrite if_true by omega. auto.
*
intro i.
drop_LOCAL 1%nat.
match goal with |- semax _ (PROPx ?P (LOCALx ?Q (SEPx ?R))) _ _ =>
   apply semax_pre0
   with (PROPx P (LOCALx (`(eq x) (eval_id _x) :: `(eq y) (eval_id _y) ::
                           `(eq z) (eval_id _z) :: Q) (SEPx R)))
 end.
rewrite <- (insert_local (`(eq _) (eval_id _x))).
rewrite <- (insert_local (`(eq _) (eval_id _y))).
rewrite <- (insert_local (`(eq _) (eval_id _z))).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
repeat rewrite <- andp_assoc. apply andp_right; auto.
drop_LOCAL 0%nat.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
repeat apply andp_right; eapply nth_error_local; eauto.
apply semax_extract_PROP; intro.

eapply semax_pre0; [ apply now_later | ].
eapply semax_post_flipped';
   [simple eapply (semax_loadstore_array sx);
       [ reflexivity | apply I | reflexivity | reflexivity| reflexivity
       |
       | erewrite nth_error_replace_nth; eauto
       | auto |  | eassumption ]
    |  ].
 +
  match goal with |- ?PQR  |-- _ =>
       apply derives_trans with
       (PQR
   && ((TT * `(array_at tdouble Tsh (Vfloat oo fy) 0 n y))
     && (TT * `(array_at tdouble Tsh (Vfloat oo fz) 0 n z))))
  end.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  apply andp_right; auto.
  apply andp_right.

  rewrite (replace_nth_nth_error _ _ _ H4).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  rewrite replace_nth_commute by auto.
  erewrite SEP_replace_nth_isolate
    by (rewrite nth_error_replace_nth' by auto; eassumption).
  rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  rewrite <- insert_SEP. apply sepcon_derives; auto.

  rewrite (replace_nth_nth_error _ _ _ H5).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
  rewrite replace_nth_commute by auto.
  erewrite SEP_replace_nth_isolate
   by (rewrite nth_error_replace_nth' by auto; eassumption).
   rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat (@map2 float float float Float.add fy fz)) x) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y)) (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z)) *)
   rewrite <- insert_SEP. apply sepcon_derives; auto.

  go_lowerx. normalize.
  apply andp_left2.
  subst. repeat instantiate_Vptr; repeat apply andp_right.
  rel_expr.
  rel_expr.
  simple eapply rel_expr_cast; [ | try (simpl; rewrite_eval_id; reflexivity) ].
  simple eapply rel_expr_binop; [ |  | ].
  apply andp_left1. rel_expr.
  apply andp_left2. rel_expr.
  reflexivity.
  reflexivity.
 +
   apply I.
 +
  simpl valinject.
  rewrite replace_nth_replace_nth.
  replace (array_at tdouble Tsh
               (upd
                  (fun j : Z =>
                   if zlt j i then Vfloat (Float.add (fy j) (fz j)) else fx j)
                  i (Vfloat (Float.add (fy i) (fz i)))) 0 n)
     with (array_at tdouble Tsh
                   (fun j : Z =>
                    if zlt j (i + 1)
                    then Vfloat (Float.add (fy j) (fz j))
                    else fx j) 0 n).
 entailer.
(* Goal: forall (A B C : Type) (a : Inhabitant A) (b : Inhabitant B) (c : Inhabitant C) (f : forall (_ : A) (_ : B), C) (al : list A) (bl : list B) (i : Z) (_ : @eq Z (@Zlength A al) (@Zlength B bl)) (_ : and (Z.le Z0 i) (Z.lt i (@Zlength A al))), @eq C (@Znth C c i (@map2 A B C f al bl)) (f (@Znth A a i al) (@Znth B b i bl)) *)
 apply array_at_ext; intros. symmetry.
 unfold upd.
(* Goal: @eq C (if zlt i Z0 then @default C c else @nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (if zlt i Z0 then @default A a else @nth A (Z.to_nat i) al a) (if zlt i Z0 then @default B b else @nth B (Z.to_nat i) bl b)) *)
 if_tac. subst. rewrite if_true by omega; try reflexivity.
(* Goal: @eq C (if zlt i Z0 then @default C c else @nth C (Z.to_nat i) (@map2 A B C f al bl) c) (f (if zlt i Z0 then @default A a else @nth A (Z.to_nat i) al a) (if zlt i Z0 then @default B b else @nth B (Z.to_nat i) bl b)) *)
 if_tac.
   rewrite if_true by omega; reflexivity.
   rewrite if_false by omega; reflexivity.
Qed.

Ltac forward_vector_add :=
 repeat match goal with |-
      semax _ _ (Ssequence (Ssequence (Ssequence _ _) _) _) _ =>
      apply -> seq_assoc; abbreviate_semax
 end;
 forward_seq;
 [eapply semax_vector_add;
 [reflexivity | auto 50 with closed | auto 50 with closed
   | rep_omega
   | solve_nth_error | solve_nth_error | solve_nth_error
   | solve_nth_error | solve_nth_error | solve_nth_error
  | computable | computable ]
 | unfold replace_nth
 ].

Lemma body_add':  semax_body Vprog Gprog f_add add_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_add add_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name i_ _i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name x_ _x.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name y_ _y.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef)))) (SEPx (@cons mpred (@data_at_ CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr (Zpos (xI xH))) tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _y (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Ssequence (Sset _t'2 (Ederef (Ebinop Oadd (Etempvar _z (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble)) (Sassign (Ederef (Ebinop Oadd (Etempvar _x (tptr tdouble)) (Etempvar _i tint) (tptr tdouble)) tdouble) (Ebinop Oadd (Etempvar _t'1 tdouble) (Etempvar _t'2 tdouble) tdouble)))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
name z_ _z.

forward_vector_add.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Zpos (xI xH))))) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@cons localdef (temp _z z) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@app val (@map float val Vfloat (@sublist float Z0 (Zpos (xI xH)) fx)) (@list_repeat val (Z.to_nat (Z.sub (Zpos (xI xH)) (Zpos (xI xH)))) Vundef)) x) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fy) y) (@cons mpred (@data_at CompSpecs Tsh (tarray tdouble (Zpos (xI xH))) (@map float val Vfloat fz) z) (@nil mpred))))))) (Sreturn (@None expr)) POSTCONDITION *)
forward.
Qed.

*)



