Library examples
Require Import EqNat.
Require Import ssreflect eqtype ssrbool ssrnat.
Require Import Lists_ext ZArith_ext Bool_ext.
Require Import string_c nodup.
Require Import bipl seplog integral_type syntax.
Module syntax_m := Syntax ZIT.
Import syntax_m.seplog_m.assert_m.expr_m.
Import syntax_m.seplog_m.assert_m.
Import syntax_m.seplog_m.
Local Open Scope Z_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope seplog_hoare_scope.
Module Div2.
Definition x := O.
Lemma div2_verif : forall vx,
{{ fun s h => [ x ]_ s = vx}} x <- var_e x ./e cst_e 2 {{ fun s h => [ x ]_ s = vx / 2}}.
Proof.
move=> vx.
eapply hoare_prop_m.hoare_stren; last by apply while.hoare_hoare0, hoare0_assign.
rewrite /while.entails => s h H.
rewrite /wp_assign; repeat Store_upd => //.
by rewrite /= /ZIT.t_div H.
Qed.
End Div2.
Module GCD.
Require Import ssreflect eqtype ssrbool ssrnat.
Require Import Lists_ext ZArith_ext Bool_ext.
Require Import string_c nodup.
Require Import bipl seplog integral_type syntax.
Module syntax_m := Syntax ZIT.
Import syntax_m.seplog_m.assert_m.expr_m.
Import syntax_m.seplog_m.assert_m.
Import syntax_m.seplog_m.
Local Open Scope Z_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope seplog_hoare_scope.
Module Div2.
Definition x := O.
Lemma div2_verif : forall vx,
{{ fun s h => [ x ]_ s = vx}} x <- var_e x ./e cst_e 2 {{ fun s h => [ x ]_ s = vx / 2}}.
Proof.
move=> vx.
eapply hoare_prop_m.hoare_stren; last by apply while.hoare_hoare0, hoare0_assign.
rewrite /while.entails => s h H.
rewrite /wp_assign; repeat Store_upd => //.
by rewrite /= /ZIT.t_div H.
Qed.
End Div2.
Module GCD.
Euclid version
Definition gcd0 a b x y :=
x <- cst_e a ;
y <- cst_e b ;
while.while (var_e x <>e var_e y) (
ifte (var_e y >> var_e x) thendo
(y <- var_e y .-e var_e x)
elsedo
(x <- var_e x .-e var_e y)
).
Local Open Scope seplog_expr_scope.
Lemma gcd0_verif : forall a b x y,
nodup (x :: y :: nil) ->
{{ fun s h => 0 < a /\ 0 < b }}
gcd0 a b x y
{{ fun s h => exists d, [ x ]_ s = d /\ Zis_gcd a b d }}.
Proof.
move=> a b x y Hset.
rewrite /gcd0.
x <- cst_e a ;
y <- cst_e b ;
while.while (var_e x <>e var_e y) (
ifte (var_e y >> var_e x) thendo
(y <- var_e y .-e var_e x)
elsedo
(x <- var_e x .-e var_e y)
).
Local Open Scope seplog_expr_scope.
Lemma gcd0_verif : forall a b x y,
nodup (x :: y :: nil) ->
{{ fun s h => 0 < a /\ 0 < b }}
gcd0 a b x y
{{ fun s h => exists d, [ x ]_ s = d /\ Zis_gcd a b d }}.
Proof.
move=> a b x y Hset.
rewrite /gcd0.
x <- cst_e a;
apply hoare_assign with (fun s _ => 0 < a /\ 0 < b /\ [ x ]_ s = a).
move=> s h /= [H1 H2].
by rewrite /wp_assign; repeat Store_upd => //.
move=> s h /= [H1 H2].
by rewrite /wp_assign; repeat Store_upd => //.
x <- cst_e b;
apply hoare_assign with (fun s _ => 0 < a /\ 0 < b /\ [ x ]_ s = a /\ [ y ]_ s = b).
move=> s h /= [H1 [H2 H3]].
by rewrite /wp_assign; repeat Store_upd => //.
move=> s h /= [H1 [H2 H3]].
by rewrite /wp_assign; repeat Store_upd => //.
while (var_e x =/= var_e y)
apply hoare_prop_m.hoare_stren with (fun s _ =>
exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\
[ x ]_ s = vx /\ [ y ]_ s = vy /\
Zis_gcd vx vy d /\ Zis_gcd a b d).
move=> s h /= [H1 [H2 [H3 H4]]].
exists a; exists b.
case: (Zgcd_spec a b) => d [Hd1 Hd2].
by exists d.
apply hoare_prop_m.hoare_weak with (fun s _ =>
(exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\
[ x ]_ s = vx /\ [ y ]_ s = vy /\
Zis_gcd vx vy d /\ Zis_gcd a b d)
/\ ~~ [ var_e x <>e var_e y ]b_ s).
move=> s h /= [[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8].
move/negPn : H8.
move/Zeq_bool_eq=> H8.
rewrite H4 H5 in H8; subst vy vx.
rewrite -H8{H2 H8} in H6.
have H : 0 <= store.get x s by omega.
case: (Zis_gcd_eq _ _ H H6) => X.
- by exists d.
- exists (-d); split; first by done.
apply Zis_gcd_opp.
by apply Zis_gcd_sym.
apply while.hoare_while.
exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\
[ x ]_ s = vx /\ [ y ]_ s = vy /\
Zis_gcd vx vy d /\ Zis_gcd a b d).
move=> s h /= [H1 [H2 [H3 H4]]].
exists a; exists b.
case: (Zgcd_spec a b) => d [Hd1 Hd2].
by exists d.
apply hoare_prop_m.hoare_weak with (fun s _ =>
(exists vx, exists vy, exists d, 0 < vx /\ 0 < vy /\
[ x ]_ s = vx /\ [ y ]_ s = vy /\
Zis_gcd vx vy d /\ Zis_gcd a b d)
/\ ~~ [ var_e x <>e var_e y ]b_ s).
move=> s h /= [[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8].
move/negPn : H8.
move/Zeq_bool_eq=> H8.
rewrite H4 H5 in H8; subst vy vx.
rewrite -H8{H2 H8} in H6.
have H : 0 <= store.get x s by omega.
case: (Zis_gcd_eq _ _ H H6) => X.
- by exists d.
- exists (-d); split; first by done.
apply Zis_gcd_opp.
by apply Zis_gcd_sym.
apply while.hoare_while.
var_e y >> var_e x
apply while.hoare_ifte.
y <- var_e y .-e var_e x
apply hoare_assign'.
move=> s h /= [[[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8] H9].
rewrite /wp_assign.
exists vx; exists (vy - vx); exists d.
repeat Store_upd => //.
split; first by done.
split.
- move/negb_true_is_false: H8 => /= H8. rewrite /ZIT.t_eqb in H8.
rewrite /ZIT.t_gtb in H9. move/Zgt_bool_true : H9 => /= H9.
subst vx vy; omega.
- split; first by done.
split.
+ by rewrite /= /ZIT.t_minus H4 H5.
+ split; last by done.
have -> : vy-vx = vx * (-1) + vy by ring.
apply Zis_gcd_for_euclid2.
by apply Zis_gcd_sym.
move=> s h /= [[[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8] H9].
rewrite /wp_assign.
exists vx; exists (vy - vx); exists d.
repeat Store_upd => //.
split; first by done.
split.
- move/negb_true_is_false: H8 => /= H8. rewrite /ZIT.t_eqb in H8.
rewrite /ZIT.t_gtb in H9. move/Zgt_bool_true : H9 => /= H9.
subst vx vy; omega.
- split; first by done.
split.
+ by rewrite /= /ZIT.t_minus H4 H5.
+ split; last by done.
have -> : vy-vx = vx * (-1) + vy by ring.
apply Zis_gcd_for_euclid2.
by apply Zis_gcd_sym.
x <- var_e x .-e var_e y
apply hoare_assign'.
move=> s h /= [[[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8] H9].
rewrite /wp_assign.
exists (vx - vy); exists vy; exists d.
repeat Store_upd => //.
split.
- move/negbTE: H8 => /=; move/Zeq_bool_neq => H8.
move/negbTE: H9; move/Zgt_bool_false => /= H9.
subst vx vy; omega.
- split; first by done.
split.
+ by rewrite /= H4 H5.
+ split; first by done.
split; last by done.
have -> : vx - vy = vy * (-1) + vx by ring.
by apply Zis_gcd_sym, Zis_gcd_for_euclid2.
Qed.
move=> s h /= [[[vx [vy [d [H1 [H2 [H4 [H5 [H6 H7]]]]]]]] H8] H9].
rewrite /wp_assign.
exists (vx - vy); exists vy; exists d.
repeat Store_upd => //.
split.
- move/negbTE: H8 => /=; move/Zeq_bool_neq => H8.
move/negbTE: H9; move/Zgt_bool_false => /= H9.
subst vx vy; omega.
- split; first by done.
split.
+ by rewrite /= H4 H5.
+ split; first by done.
split; last by done.
have -> : vx - vy = vy * (-1) + vx by ring.
by apply Zis_gcd_sym, Zis_gcd_for_euclid2.
Qed.
classical algorithm
Definition gcd1 a b r :=
while.while (var_e b <>e cst_e 0) (
r <- var_e a mode var_e b ;
a <- var_e b ;
b <- var_e r
).
Lemma gcd1_verif : forall a b r,
nodup (a :: b :: r :: nil) ->
forall va vb, 0 <= va -> 0 <= vb ->
{{ fun s h => [ a ]_ s = va /\ [ b ]_ s = vb }}
gcd1 a b r
{{ fun s h => exists wa, exists wb, exists d,
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d }}.
Proof.
move=> a b r Hset va vb Hva Hvb.
rewrite /gcd1.
while.while (var_e b <>e cst_e 0) (
r <- var_e a mode var_e b ;
a <- var_e b ;
b <- var_e r
).
Lemma gcd1_verif : forall a b r,
nodup (a :: b :: r :: nil) ->
forall va vb, 0 <= va -> 0 <= vb ->
{{ fun s h => [ a ]_ s = va /\ [ b ]_ s = vb }}
gcd1 a b r
{{ fun s h => exists wa, exists wb, exists d,
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d }}.
Proof.
move=> a b r Hset va vb Hva Hvb.
rewrite /gcd1.
while (var_e b =/= cst_e 0)
apply hoare_prop_m.hoare_stren with (fun s _ =>
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d))).
move=> s h /= [H1 H2].
exists va; exists vb.
move: (Zgcd_spec va vb) => [d [Hd1 Hd2] ].
exists d => //.
apply hoare_prop_m.hoare_weak with (fun s _ =>
(exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d)))
/\ ~~ [ var_e b <>e cst_e 0 ]b_ s).
move=> s h /= [ [wa [wb [ d [H2 [H3 [H4 [H6 [H7 H8]]]]]]]] H1].
exists wa; exists wb; exists d => //.
apply while.hoare_while with (P := fun s _ =>
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\ Zis_gcd wa wb d /\ Zis_gcd va vb d))).
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d))).
move=> s h /= [H1 H2].
exists va; exists vb.
move: (Zgcd_spec va vb) => [d [Hd1 Hd2] ].
exists d => //.
apply hoare_prop_m.hoare_weak with (fun s _ =>
(exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d)))
/\ ~~ [ var_e b <>e cst_e 0 ]b_ s).
move=> s h /= [ [wa [wb [ d [H2 [H3 [H4 [H6 [H7 H8]]]]]]]] H1].
exists wa; exists wb; exists d => //.
apply while.hoare_while with (P := fun s _ =>
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 <= wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\ Zis_gcd wa wb d /\ Zis_gcd va vb d))).
r <- var_e a mode var_e b;
apply hoare_assign with (fun s _ =>
(exists wa, (exists wb, (exists d, 0 <= wa /\ 0 < wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d /\ [ r ]_ s = Zmod wa wb)))).
move=> s h /= [ [wa [wb [ d [H2 [H3 [H4 [H6 [H7 H8]]]]]]]] H1].
exists wa; exists wb; exists d.
repeat Store_upd => //.
split; first by done.
split.
- move/negb_true_is_false : H1; move/Zeq_bool_neq => /= H1.
subst wa wb; omega.
- split; first by done.
split.
+ done.
+ split; first by done.
split; first by done.
by rewrite /= H4 H6.
(exists wa, (exists wb, (exists d, 0 <= wa /\ 0 < wb /\
[ a ]_ s = wa /\ [ b ]_ s = wb /\
Zis_gcd wa wb d /\ Zis_gcd va vb d /\ [ r ]_ s = Zmod wa wb)))).
move=> s h /= [ [wa [wb [ d [H2 [H3 [H4 [H6 [H7 H8]]]]]]]] H1].
exists wa; exists wb; exists d.
repeat Store_upd => //.
split; first by done.
split.
- move/negb_true_is_false : H1; move/Zeq_bool_neq => /= H1.
subst wa wb; omega.
- split; first by done.
split.
+ done.
+ split; first by done.
split; first by done.
by rewrite /= H4 H6.
a <- var_e b;
apply hoare_assign with (fun s _ =>
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 < wb /\
[ a ]_ s = wb /\ [ b ]_ s = wb /\ Zis_gcd wa wb d /\ Zis_gcd va vb d /\
[ r ]_ s = wa mod wb))).
move=> s h /= [wa [wb [ d [H2 [H3 [H4 [H6 [H7 [H8 H9]]]]]]]]] .
exists wa; exists wb; exists d.
by repeat Store_upd => //.
exists wa, (exists wb, (exists d, 0 <= wa /\ 0 < wb /\
[ a ]_ s = wb /\ [ b ]_ s = wb /\ Zis_gcd wa wb d /\ Zis_gcd va vb d /\
[ r ]_ s = wa mod wb))).
move=> s h /= [wa [wb [ d [H2 [H3 [H4 [H6 [H7 [H8 H9]]]]]]]]] .
exists wa; exists wb; exists d.
by repeat Store_upd => //.
b <- var_e r
apply hoare_assign'.
move=> s h /= [wa [wb [d [H2 [H3 [H4 [H6 [H7 [H8 H9]]]]]]]]].
exists wb; exists (wa mod wb); exists d.
repeat Store_upd => //.
split; first by omega.
split.
- case: (Z_mod_lt wa wb (Zlt_gt _ _ H3)) => X1 _ //.
- split; first by done.
split; first by done.
split; last by done.
move: (Z_div_mod_eq wa wb (Zlt_gt _ _ H3)) => H.
have ->: wa mod wb = wb * (- (wa / wb)) + wa.
have -> : wa mod wb = wa - wb * (wa / wb) by omega.
by ring.
by apply (Zis_gcd_for_euclid2 (wb) d (-(wa / wb)) wa).
Qed.
End GCD.
Module Factorial.
Lemma factorial : forall n, 0 <= n -> forall x m, nodup (x :: m :: nil) ->
{{ fun s h => [ m ]_ s = n /\ [ x ]_ s = 1 }}
while.while (var_e m <>e cst_e 0) (
x <- var_e x *e var_e m;
m <- var_e m .-e cst_e 1 )
{{ fun s h => [ x ]_ s = Zfact n }}.
Proof.
move=> n n_pos x m Hvars.
apply hoare_prop_m.hoare_stren with (fun s _ =>
[ x ]_ s * Zfact ([ m ]_ s) = Zfact n /\ 0 <= [ m ]_ s).
move=> s h /= [H1 H2].
rewrite H1 H2.
split; [ring | omega].
apply hoare_prop_m.hoare_weak with (fun s _ =>
([ x ]_ s * Zfact ([ m ]_ s) = Zfact n /\ 0 <= [ m ]_ s) /\
~~ [ var_e m <>e cst_e 0 ]b_ s).
move=> s h /= [[H1 H2] H3].
move/negPn : H3 => H3.
apply Zeq_bool_eq in H3.
by rewrite -H1 H3 //= Zmult_1_r.
apply while.hoare_while.
apply hoare_assign with (fun s _ =>
[ x ]_ s * Zfact ([ m ]_ s - 1) = Zfact n /\ 0 <= [ m ]_ s - 1).
move=> s h /= [[H1 H2] H3].
rewrite /wp_assign; repeat Store_upd => //.
move/Zeq_boolP : H3 => /= H3.
split; last by omega.
rewrite -H1 (Zfact_pos ([ m ]_ s)) /= /ZIT.t_mult; last by omega.
ring.
apply hoare_assign'.
move=> s h /= [H1 H2].
by rewrite /wp_assign; repeat Store_upd.
Qed.
Local Open Scope heap_scope.
Module StringCopy.
move=> s h /= [wa [wb [d [H2 [H3 [H4 [H6 [H7 [H8 H9]]]]]]]]].
exists wb; exists (wa mod wb); exists d.
repeat Store_upd => //.
split; first by omega.
split.
- case: (Z_mod_lt wa wb (Zlt_gt _ _ H3)) => X1 _ //.
- split; first by done.
split; first by done.
split; last by done.
move: (Z_div_mod_eq wa wb (Zlt_gt _ _ H3)) => H.
have ->: wa mod wb = wb * (- (wa / wb)) + wa.
have -> : wa mod wb = wa - wb * (wa / wb) by omega.
by ring.
by apply (Zis_gcd_for_euclid2 (wb) d (-(wa / wb)) wa).
Qed.
End GCD.
Module Factorial.
Lemma factorial : forall n, 0 <= n -> forall x m, nodup (x :: m :: nil) ->
{{ fun s h => [ m ]_ s = n /\ [ x ]_ s = 1 }}
while.while (var_e m <>e cst_e 0) (
x <- var_e x *e var_e m;
m <- var_e m .-e cst_e 1 )
{{ fun s h => [ x ]_ s = Zfact n }}.
Proof.
move=> n n_pos x m Hvars.
apply hoare_prop_m.hoare_stren with (fun s _ =>
[ x ]_ s * Zfact ([ m ]_ s) = Zfact n /\ 0 <= [ m ]_ s).
move=> s h /= [H1 H2].
rewrite H1 H2.
split; [ring | omega].
apply hoare_prop_m.hoare_weak with (fun s _ =>
([ x ]_ s * Zfact ([ m ]_ s) = Zfact n /\ 0 <= [ m ]_ s) /\
~~ [ var_e m <>e cst_e 0 ]b_ s).
move=> s h /= [[H1 H2] H3].
move/negPn : H3 => H3.
apply Zeq_bool_eq in H3.
by rewrite -H1 H3 //= Zmult_1_r.
apply while.hoare_while.
apply hoare_assign with (fun s _ =>
[ x ]_ s * Zfact ([ m ]_ s - 1) = Zfact n /\ 0 <= [ m ]_ s - 1).
move=> s h /= [[H1 H2] H3].
rewrite /wp_assign; repeat Store_upd => //.
move/Zeq_boolP : H3 => /= H3.
split; last by omega.
rewrite -H1 (Zfact_pos ([ m ]_ s)) /= /ZIT.t_mult; last by omega.
ring.
apply hoare_assign'.
move=> s h /= [H1 H2].
by rewrite /wp_assign; repeat Store_upd.
Qed.
Local Open Scope heap_scope.
Module StringCopy.
for (c1=buf, c2=s; ( *c1++ = *c2++ )!=0)
Definition StringCopy c1 c2 buf str str_tmp :=
c1 <- var_e buf;
c2 <- var_e str;
str_tmp <-* var_e c2;
while.while (var_e str_tmp <>e cst_e 0) (
var_e c1 *<- var_e str_tmp ;
c1 <- var_e c1 +e cst_e 1 ;
c2 <- var_e c2 +e cst_e 1 ;
str_tmp <-* var_e c2
) ;
var_e c1 *<- var_e str_tmp.
Lemma StringCopy_specif :
forall c1 c2 buf str str_tmp,
nodup (c1 :: c2 :: buf :: str :: str_tmp :: nil) ->
forall buf_lst str_lst,
(0 < length buf_lst)%nat ->
(length str_lst <= length buf_lst)%nat ->
string str_lst ->
{{ var_e buf |---> buf_lst ** var_e str |---> str_lst }}
StringCopy c1 c2 buf str str_tmp
{{ (var_e buf |---> str_lst) ** TT ** (var_e str |---> str_lst) }}.
Proof.
move=> c1 c2 buf str str_tmp Hset buf_lst str_lst Hbuf Hbuf2 Hstr.
rewrite /StringCopy.
c1 <- var_e buf;
c2 <- var_e str;
str_tmp <-* var_e c2;
while.while (var_e str_tmp <>e cst_e 0) (
var_e c1 *<- var_e str_tmp ;
c1 <- var_e c1 +e cst_e 1 ;
c2 <- var_e c2 +e cst_e 1 ;
str_tmp <-* var_e c2
) ;
var_e c1 *<- var_e str_tmp.
Lemma StringCopy_specif :
forall c1 c2 buf str str_tmp,
nodup (c1 :: c2 :: buf :: str :: str_tmp :: nil) ->
forall buf_lst str_lst,
(0 < length buf_lst)%nat ->
(length str_lst <= length buf_lst)%nat ->
string str_lst ->
{{ var_e buf |---> buf_lst ** var_e str |---> str_lst }}
StringCopy c1 c2 buf str str_tmp
{{ (var_e buf |---> str_lst) ** TT ** (var_e str |---> str_lst) }}.
Proof.
move=> c1 c2 buf str str_tmp Hset buf_lst str_lst Hbuf Hbuf2 Hstr.
rewrite /StringCopy.
c1 <- var_e buf;
apply hoare_assign with (fun s h =>
(var_e buf |---> buf_lst ** (var_e str |---> str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s).
move=> s h H; rewrite /wp_assign; split.
- apply inde_upd_store => //.
apply inde_sep_con.
+ apply inde_mapstos'.
apply disj_cons_L.
by apply disj_nil_L.
by Nodup_not_In.
+ apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
rewrite [vars _]/=; by Nodup_not_In.
- by repeat Store_upd.
(var_e buf |---> buf_lst ** (var_e str |---> str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s).
move=> s h H; rewrite /wp_assign; split.
- apply inde_upd_store => //.
apply inde_sep_con.
+ apply inde_mapstos'.
apply disj_cons_L.
by apply disj_nil_L.
by Nodup_not_In.
+ apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
rewrite [vars _]/=; by Nodup_not_In.
- by repeat Store_upd.
c2 <- var_e str;
apply hoare_assign with (fun s h =>
(var_e buf |---> buf_lst ** (var_e str |---> str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s /\ [ c2 ]_ s = [ str ]_ s).
move=> s h [H1 H2]; rewrite /wp_assign; split.
- apply inde_upd_store => //.
+ apply inde_sep_con.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
+ apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- by repeat Store_upd.
destruct str_lst as [|str0 str_lst]; first by move: string_nil.
(var_e buf |---> buf_lst ** (var_e str |---> str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s /\ [ c2 ]_ s = [ str ]_ s).
move=> s h [H1 H2]; rewrite /wp_assign; split.
- apply inde_upd_store => //.
+ apply inde_sep_con.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
+ apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- by repeat Store_upd.
destruct str_lst as [|str0 str_lst]; first by move: string_nil.
str_tmp <-* var_e c2;
apply hoare_lookup_back_strictly_exact with (fun s h =>
(var_e buf |---> buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s /\ [ c2 ]_ s = [ str ]_ s /\ [ str_tmp ]_ s = str0).
move=> s h [H1 [H2 H3]]; exists (cst_e str0); split.
- case_sepcon H1.
rewrite /mapstos' /= in H1_h2.
case_sepcon H1_h2.
exists h21; exists (h1 +++ h22); split; first by map_tac_m.Disj.
split; first by map_tac_m.Equal.
split; [by Mapsto | done].
- rewrite /wp_assign; repeat Store_upd => //.
split; last by done.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
(var_e buf |---> buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s /\ [ c2 ]_ s = [ str ]_ s /\ [ str_tmp ]_ s = str0).
move=> s h [H1 [H2 H3]]; exists (cst_e str0); split.
- case_sepcon H1.
rewrite /mapstos' /= in H1_h2.
case_sepcon H1_h2.
exists h21; exists (h1 +++ h22); split; first by map_tac_m.Disj.
split; first by map_tac_m.Equal.
split; [by Mapsto | done].
- rewrite /wp_assign; repeat Store_upd => //.
split; last by done.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
while (var_e str_tmp =/= cst_e 0)
apply hoare_prop_m.hoare_stren with (fun s h => exists i,
(var_e buf |---> firstn i (str0 :: str_lst) ++ skipn i buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\
(i <= length (str0 :: str_lst))%nat /\ 0 <= [ str_tmp ]_ s).
move=> s h [H1 [H2 [H3 Hstr_tmp_is_0]]]; exists O; split => //=.
do 2 rewrite -Zplus_0_r_reverse.
repeat (split => //).
apply string_hd_ge0 in Hstr.
apply Zge_le; by rewrite Hstr_tmp_is_0.
apply while.hoare_seq with (fun s h => (exists i,
(var_e buf |---> (firstn i (str0 :: str_lst)) ++ (skipn i buf_lst) ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\
(i <= length (str0 :: str_lst))%nat /\ 0 <= [ str_tmp ]_ s) /\
~~ [ var_e str_tmp <>e cst_e 0 ]b_ s).
apply while.hoare_while.
(var_e buf |---> firstn i (str0 :: str_lst) ++ skipn i buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\
(i <= length (str0 :: str_lst))%nat /\ 0 <= [ str_tmp ]_ s).
move=> s h [H1 [H2 [H3 Hstr_tmp_is_0]]]; exists O; split => //=.
do 2 rewrite -Zplus_0_r_reverse.
repeat (split => //).
apply string_hd_ge0 in Hstr.
apply Zge_le; by rewrite Hstr_tmp_is_0.
apply while.hoare_seq with (fun s h => (exists i,
(var_e buf |---> (firstn i (str0 :: str_lst)) ++ (skipn i buf_lst) ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\
(i <= length (str0 :: str_lst))%nat /\ 0 <= [ str_tmp ]_ s) /\
~~ [ var_e str_tmp <>e cst_e 0 ]b_ s).
apply while.hoare_while.
var_e c1 *<- var_e str_tmp;
apply hoare_mutation_backwards'' with (fun s h => exists i,
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ (skipn (S i) buf_lst) ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [[x [H2 [H3 [H4 [H5 [H6 H7]]]]]] H1].
have [H0 | H0] : (length buf_lst <= x \/ x < length buf_lst)%coq_nat by omega.
Require Import ssrnat_ext.
-
rewrite skipn_all in H2; last by ssrnat_omega.
have H : length buf_lst = length (str0 :: str_lst) by ssrnat_omega.
rewrite H in H0.
have H8 : x = length (str0 :: str_lst) by ssrnat_omega.
have H9 : store.get str_tmp s = -1 by rewrite H8 // nth_last in H5.
rewrite H9 in H7.
have [//] : False by omega.
- have H : 0 < [ str_tmp ]_ s.
rewrite /hoare_m.eval_b in H1.
eval_b2Prop_hyp H1.
apply Zle_neq_lt => //.
by auto.
have [H9|[H9|H8]] : (S x = length (str0 :: str_lst) \/ x = length (str0 :: str_lst) \/ S x < length (str0 :: str_lst))%coq_nat by ssrnat_omega.
+ rewrite string_last' // in H5; last by omega.
rewrite H5 in H; by inversion H.
+ subst x.
rewrite nth_last // in H5.
rewrite H5 in H.
have [//] : False by omega.
+ rewrite (skipn_S (-1)) // in H2.
case_sepcon H2.
move/mapstos'_app_sepcon : H2_h1 => H2_h1.
case_sepcon H2_h1.
move/mapstos'_cons_sepcon : H2_h1_h12 => H2_h1_h12.
case_sepcon H2_h1_h12.
exists (cst_e (nth x buf_lst (-1))).
Compose_sepcon h121 (h2 +++ h11 +++ h122).
Mapsto.
rewrite /= H3 // (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /imp => h121' [X1 X2] h' Hh'.
exists x.
repeat (split => //).
* Compose_sepcon (h11 +++ h121' +++ h122) h2 => //.
apply mapstos'_sepcon_app.
Compose_sepcon (h11 +++ h121') h122.
rewrite (firstn_S (-1)); last by omega.
eapply mapstos'_sepcon_app.
Compose_sepcon h11 h121' => //.
rewrite /mapstos' [nth]lock /= -lock.
apply assert_m.con_emp'.
Mapsto.
rewrite H3 //.
rewrite (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /mapstos' in H2_h1_h12_h122 *.
move: H2_h1_h12_h122; apply mapstos_ext => //.
rewrite [firstn]lock /= -lock -ZIT.t_plus_assoc; f_equal.
rewrite ZIT.t_plus_comm {1}(_ : 1 = ZIT.nat2t 1) // ZIT.t_plus_1.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
rewrite /= in H8 *; by ssrnat_omega.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
rewrite /= in H8 *; by ssrnat_omega.
* rewrite /= in H8 *; by ssrnat_omega.
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ (skipn (S i) buf_lst) ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + Z_of_nat i /\ [ c2 ]_ s = [ str ]_ s + Z_of_nat i /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [[x [H2 [H3 [H4 [H5 [H6 H7]]]]]] H1].
have [H0 | H0] : (length buf_lst <= x \/ x < length buf_lst)%coq_nat by omega.
Require Import ssrnat_ext.
-
rewrite skipn_all in H2; last by ssrnat_omega.
have H : length buf_lst = length (str0 :: str_lst) by ssrnat_omega.
rewrite H in H0.
have H8 : x = length (str0 :: str_lst) by ssrnat_omega.
have H9 : store.get str_tmp s = -1 by rewrite H8 // nth_last in H5.
rewrite H9 in H7.
have [//] : False by omega.
- have H : 0 < [ str_tmp ]_ s.
rewrite /hoare_m.eval_b in H1.
eval_b2Prop_hyp H1.
apply Zle_neq_lt => //.
by auto.
have [H9|[H9|H8]] : (S x = length (str0 :: str_lst) \/ x = length (str0 :: str_lst) \/ S x < length (str0 :: str_lst))%coq_nat by ssrnat_omega.
+ rewrite string_last' // in H5; last by omega.
rewrite H5 in H; by inversion H.
+ subst x.
rewrite nth_last // in H5.
rewrite H5 in H.
have [//] : False by omega.
+ rewrite (skipn_S (-1)) // in H2.
case_sepcon H2.
move/mapstos'_app_sepcon : H2_h1 => H2_h1.
case_sepcon H2_h1.
move/mapstos'_cons_sepcon : H2_h1_h12 => H2_h1_h12.
case_sepcon H2_h1_h12.
exists (cst_e (nth x buf_lst (-1))).
Compose_sepcon h121 (h2 +++ h11 +++ h122).
Mapsto.
rewrite /= H3 // (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /imp => h121' [X1 X2] h' Hh'.
exists x.
repeat (split => //).
* Compose_sepcon (h11 +++ h121' +++ h122) h2 => //.
apply mapstos'_sepcon_app.
Compose_sepcon (h11 +++ h121') h122.
rewrite (firstn_S (-1)); last by omega.
eapply mapstos'_sepcon_app.
Compose_sepcon h11 h121' => //.
rewrite /mapstos' [nth]lock /= -lock.
apply assert_m.con_emp'.
Mapsto.
rewrite H3 //.
rewrite (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /mapstos' in H2_h1_h12_h122 *.
move: H2_h1_h12_h122; apply mapstos_ext => //.
rewrite [firstn]lock /= -lock -ZIT.t_plus_assoc; f_equal.
rewrite ZIT.t_plus_comm {1}(_ : 1 = ZIT.nat2t 1) // ZIT.t_plus_1.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
rewrite /= in H8 *; by ssrnat_omega.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
rewrite /= in H8 *; by ssrnat_omega.
* rewrite /= in H8 *; by ssrnat_omega.
c1 <- var_e c1 +e cst_e 1;
apply hoare_assign with (fun s h => exists i,
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ skipn (S i) buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + (Z_of_nat i) + 1 /\ [ c2 ]_ s = [ str ]_ s + (Z_of_nat i) /\
[ str_tmp ]_ s = nth i (str0::str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [x [H1 [H2 [H3 [H4 [H5 H6]]]]]]; rewrite /wp_assign.
repeat Store_upd => //.
exists x; split.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
split; last by done.
by rewrite /= H2.
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ skipn (S i) buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + (Z_of_nat i) + 1 /\ [ c2 ]_ s = [ str ]_ s + (Z_of_nat i) /\
[ str_tmp ]_ s = nth i (str0::str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [x [H1 [H2 [H3 [H4 [H5 H6]]]]]]; rewrite /wp_assign.
repeat Store_upd => //.
exists x; split.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
split; last by done.
by rewrite /= H2.
c2 <- var_e c2 +e cst_e 1;
apply hoare_assign with (fun s h => exists i,
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ skipn (S i) buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + (Z_of_nat i) + 1 /\ [ c2 ]_ s = [ str ]_ s + (Z_of_nat i) + 1 /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [x [H1 [H2 [H3 [H4 [H5 H6]]]]]]; rewrite /wp_assign.
repeat Store_upd => //.
exists x; split.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
split; first by done.
split=> /=; last by done.
by rewrite H3.
(var_e buf |---> firstn (S i) (str0 :: str_lst) ++ skipn (S i) buf_lst ** (var_e str |---> str0 :: str_lst)) s h /\
[ c1 ]_ s = [ buf ]_ s + (Z_of_nat i) + 1 /\ [ c2 ]_ s = [ str ]_ s + (Z_of_nat i) + 1 /\
[ str_tmp ]_ s = nth i (str0 :: str_lst) (-1) /\ 0 < [ str_tmp ]_ s /\
(S i < length (str0 :: str_lst))%nat).
move=> s h [x [H1 [H2 [H3 [H4 [H5 H6]]]]]]; rewrite /wp_assign.
repeat Store_upd => //.
exists x; split.
apply inde_upd_store => //.
apply inde_sep_con.
- apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
- apply inde_mapstos' => /=.
apply disj_cons_R.
by apply disj_nil_R.
by Nodup_not_In.
split; first by done.
split=> /=; last by done.
by rewrite H3.
str_tmp <-* var_e c2);
apply hoare_lookup_back'.
move=> s h [x [Hmem [Hc1 [Hc2 [Hstr_tmp [_ Hlenstr_lst]]]]]].
exists (cst_e (nth (S x) (str0 :: str_lst) (-1))).
apply mapsto_strictly_exact.
split.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
rewrite -(@firstn_skipn _ (S x) (str0 :: str_lst)) in Hmem2.
case: {Hmem2}(mapstos'_app_sepcon _ _ _ _ _ Hmem2) => h21 [h22 [Hdisj'' [Hunion'' [Hmem21 Hmem22]]]].
rewrite (skipn_S (-1)) // in Hmem22; last first.
by apply/ltP.
case: {Hmem22}(mapstos'_cons_sepcon _ _ _ _ _ Hmem22) => h221 [h222 [Hdisj' [Hunion' [Hmem221 Hmem222]]]].
Compose_sepcon h221 (h222 +++ h21 +++ h1) => //.
rewrite (_ : S x = x + 1)%nat in Hmem221; last by rewrite addnC. Mapsto.
- rewrite Hc2.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
apply lt_le_weak.
by ssrnat_omega.
rewrite A_prop_m.t_inj_plus.
rewrite {+}/ZIT.t_plus (_ : 1 = (ZIT.nat2t 1)) //.
rewrite /ZIT.nat2t Zplus_assoc //.
- by rewrite addnC /=.
rewrite /wp_assign.
repeat Store_upd => //.
exists (S x).
split.
apply inde_upd_store => //.
apply inde_sep_con.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
split.
by rewrite Hc1 Z_S Zplus_assoc.
split => //.
by rewrite Hc2 Z_S Zplus_assoc.
split; first by done.
split.
by ssrnat_omega.
rewrite [nth]lock /= -lock.
apply Zge_le.
apply string_last'' => //.
by ssrnat_omega.
move=> s h [x [Hmem [Hc1 [Hc2 [Hstr_tmp [_ Hlenstr_lst]]]]]].
exists (cst_e (nth (S x) (str0 :: str_lst) (-1))).
apply mapsto_strictly_exact.
split.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
rewrite -(@firstn_skipn _ (S x) (str0 :: str_lst)) in Hmem2.
case: {Hmem2}(mapstos'_app_sepcon _ _ _ _ _ Hmem2) => h21 [h22 [Hdisj'' [Hunion'' [Hmem21 Hmem22]]]].
rewrite (skipn_S (-1)) // in Hmem22; last first.
by apply/ltP.
case: {Hmem22}(mapstos'_cons_sepcon _ _ _ _ _ Hmem22) => h221 [h222 [Hdisj' [Hunion' [Hmem221 Hmem222]]]].
Compose_sepcon h221 (h222 +++ h21 +++ h1) => //.
rewrite (_ : S x = x + 1)%nat in Hmem221; last by rewrite addnC. Mapsto.
- rewrite Hc2.
rewrite (len_firstn (length (str0 :: str_lst))) //; last first.
apply lt_le_weak.
by ssrnat_omega.
rewrite A_prop_m.t_inj_plus.
rewrite {+}/ZIT.t_plus (_ : 1 = (ZIT.nat2t 1)) //.
rewrite /ZIT.nat2t Zplus_assoc //.
- by rewrite addnC /=.
rewrite /wp_assign.
repeat Store_upd => //.
exists (S x).
split.
apply inde_upd_store => //.
apply inde_sep_con.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
apply inde_mapstos'.
apply disj_cons_R.
by apply disj_nil_R.
by rewrite [vars _]/=; Nodup_not_In.
split.
by rewrite Hc1 Z_S Zplus_assoc.
split => //.
by rewrite Hc2 Z_S Zplus_assoc.
split; first by done.
split.
by ssrnat_omega.
rewrite [nth]lock /= -lock.
apply Zge_le.
apply string_last'' => //.
by ssrnat_omega.
var_e c1 *<- var_e str_tmp.
apply hoare_mutation_backwards'.
move=> s h [[x [Hmem [Hc1 [Hc2 [Hstr_tmp [Hx _]]]]]] Hstr_tmp_is_0].
have {Hstr_tmp_is_0}Hstr_tmp_is_0 : [ str_tmp ]_ s = 0.
eval_b2Prop_hyps.
by case: (ZIT.t_dec ([ str_tmp ]_ s) 0).
have H : (x = length (str0 :: str_lst) - 1)%nat.
apply string_last => //.
by rewrite -Hstr_tmp.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
rewrite (skipn_S (-1)) // in Hmem1.
case: {Hmem1}(mapstos'_app_sepcon _ _ _ _ _ Hmem1) => h11 [h12 [Hdisj' [Hunion' [Hmem11 Hmem12]]]].
case: {Hmem12}(mapstos'_cons_sepcon _ _ _ _ _ Hmem12) => h121 [h122 [Hdisj'' [Hunion'' [Hmem121 Hmem122]]]].
exists (cst_e (nth x buf_lst (-1))).
Compose_sepcon h121 (h122 +++ h11 +++ h2) => //.
Mapsto.
rewrite (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /imp => h121' [X1 X2] h' Hh'.
Compose_sepcon (h122 +++ h11 +++ h121') h2 => //.
Compose_sepcon (h11 +++ h121') h122 => //.
rewrite (firstn_last (-1) (str0 :: str_lst) x) //.
apply mapstos'_sepcon_app.
Compose_sepcon h11 h121' => //.
rewrite /mapstos' [nth]lock /= -lock.
apply assert_m.con_emp'.
Mapsto.
rewrite Hc1 (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /= in Hbuf2, Hx, H.
rewrite subn1 /= in H.
subst x.
by apply/ltP.
Qed.
End StringCopy.
Local Open Scope vc_scope.
Lemma vc_factorial : forall n, n >= 0 ->
forall x m, nodup (x :: m :: nil) ->
{{ fun s _ => [ m ]_ s = n /\ [ x ]_ s = 1 }} proj_cmd
(while' ( (var_e m) <>e cst_e 0 )
(fun s _ => [ x ]_ s * (Zfact [ m ]_ s) = Zfact n /\ [ m ]_ s >= 0)
( x <- var_e x *e var_e m;
m <- var_e m .-e cst_e 1))
{{ fun s _ => [ x ]_ s = Zfact n }}.
Proof.
move=> n Hpos x m Hvars.
apply wp_vc_util.
move=> s h /=.
move=> s h [[x [Hmem [Hc1 [Hc2 [Hstr_tmp [Hx _]]]]]] Hstr_tmp_is_0].
have {Hstr_tmp_is_0}Hstr_tmp_is_0 : [ str_tmp ]_ s = 0.
eval_b2Prop_hyps.
by case: (ZIT.t_dec ([ str_tmp ]_ s) 0).
have H : (x = length (str0 :: str_lst) - 1)%nat.
apply string_last => //.
by rewrite -Hstr_tmp.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
rewrite (skipn_S (-1)) // in Hmem1.
case: {Hmem1}(mapstos'_app_sepcon _ _ _ _ _ Hmem1) => h11 [h12 [Hdisj' [Hunion' [Hmem11 Hmem12]]]].
case: {Hmem12}(mapstos'_cons_sepcon _ _ _ _ _ Hmem12) => h121 [h122 [Hdisj'' [Hunion'' [Hmem121 Hmem122]]]].
exists (cst_e (nth x buf_lst (-1))).
Compose_sepcon h121 (h122 +++ h11 +++ h2) => //.
Mapsto.
rewrite (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /imp => h121' [X1 X2] h' Hh'.
Compose_sepcon (h122 +++ h11 +++ h121') h2 => //.
Compose_sepcon (h11 +++ h121') h122 => //.
rewrite (firstn_last (-1) (str0 :: str_lst) x) //.
apply mapstos'_sepcon_app.
Compose_sepcon h11 h121' => //.
rewrite /mapstos' [nth]lock /= -lock.
apply assert_m.con_emp'.
Mapsto.
rewrite Hc1 (len_firstn (length (str0 :: str_lst))) //.
by ssrnat_omega.
rewrite /= in Hbuf2, Hx, H.
rewrite subn1 /= in H.
subst x.
by apply/ltP.
Qed.
End StringCopy.
Local Open Scope vc_scope.
Lemma vc_factorial : forall n, n >= 0 ->
forall x m, nodup (x :: m :: nil) ->
{{ fun s _ => [ m ]_ s = n /\ [ x ]_ s = 1 }} proj_cmd
(while' ( (var_e m) <>e cst_e 0 )
(fun s _ => [ x ]_ s * (Zfact [ m ]_ s) = Zfact n /\ [ m ]_ s >= 0)
( x <- var_e x *e var_e m;
m <- var_e m .-e cst_e 1))
{{ fun s _ => [ x ]_ s = Zfact n }}.
Proof.
move=> n Hpos x m Hvars.
apply wp_vc_util.
move=> s h /=.
vc
rewrite /wp_assign /=.
repeat Store_upd => //.
split.
move=> [[<- H2]].
move/negPn.
move/Zeq_boolP => -> /=. by rewrite Zmult_1_r.
split => //.
move=> [[H1 H2] H3].
move/negb_true_is_false : H3.
move/Zeq_bool_neq => H3.
split.
rewrite -H1 (Zfact_pos (store.get m s)).
rewrite /ZIT.t_mult /ZIT.t_minus.
ring.
omega.
rewrite /ZIT.t_minus.
omega.
move=> s h /= [-> ->].
split => //; ring.
Qed.
End Factorial.
Module Swap.
Lemma swap : forall x y z v a b, nodup (x :: y :: z :: v :: nil) ->
{{ (var_e x |~> cst_e a) ** (var_e y |~> cst_e b) }}
z <-* var_e x;
v <-* var_e y;
var_e x *<- var_e v;
var_e y *<- var_e z
{{ (var_e x |~> cst_e b) ** (var_e y |~> cst_e a) }}.
Proof.
move=> x y z v a b Hvars.
apply hoare_lookup_back'' with (fun s h =>
(var_e x |~> cst_e a ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_s = a).
move=> s h H.
case_sepcon H.
exists (cst_e a).
Compose_sepcon h1 h2 => //.
rewrite /imp => h1' [X1 X2] h' Hh'.
rewrite /wp_assign.
split.
Compose_sepcon h1' h2; by Mapsto.
rewrite /=; repeat Store_upd => //.
apply hoare_lookup_back'' with (fun s h =>
(var_e x |~> cst_e a ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_ s = a /\ [ var_e v ]e_ s = b).
move=> s h [H1 H2].
case_sepcon H1.
exists (cst_e b).
Compose_sepcon h2 h1 => //.
rewrite /imp => h2' [X1 X2] h' Hh'.
rewrite /wp_assign.
split.
Compose_sepcon h1 h2'; by Mapsto.
rewrite /=.
by split; repeat Store_upd.
apply hoare_mutation_backwards'' with (fun s h =>
(var_e x |~> cst_e b ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_s = a /\ [ var_e v ]e_s = b).
move=> s h [H1 [H2 H3]].
case_sepcon H1.
exists (cst_e a).
Compose_sepcon h1 h2 => //.
rewrite /imp => h1' [X1 X2] h' Hh'.
split.
Compose_sepcon h1' h2; by Mapsto.
done.
apply hoare_mutation_backwards'.
move=> s h /= [H1 [H2 H3] ].
case_sepcon H1.
exists (cst_e b).
Compose_sepcon h2 h1 => //.
rewrite /imp => h2' [X1 X2] h' Hh'.
Compose_sepcon h1 h2'; by Mapsto.
Qed.
Local Open Scope vc_scope.
Lemma vc_swap : forall x y z v a b, nodup (x :: y :: z :: v :: nil) ->
{{ (var_e x |~> cst_e a) ** (var_e y |~> cst_e b) }}
proj_cmd
(z <-*var_e x;
v <-* var_e y;
var_e x *<- var_e v;
var_e y *<- var_e z)
{{ (var_e x |~> cst_e b) ** (var_e y |~> cst_e a) }}.
Proof.
move=> x y z v a b Hvars.
apply wp_vc_util.
repeat Store_upd => //.
split.
move=> [[<- H2]].
move/negPn.
move/Zeq_boolP => -> /=. by rewrite Zmult_1_r.
split => //.
move=> [[H1 H2] H3].
move/negb_true_is_false : H3.
move/Zeq_bool_neq => H3.
split.
rewrite -H1 (Zfact_pos (store.get m s)).
rewrite /ZIT.t_mult /ZIT.t_minus.
ring.
omega.
rewrite /ZIT.t_minus.
omega.
move=> s h /= [-> ->].
split => //; ring.
Qed.
End Factorial.
Module Swap.
Lemma swap : forall x y z v a b, nodup (x :: y :: z :: v :: nil) ->
{{ (var_e x |~> cst_e a) ** (var_e y |~> cst_e b) }}
z <-* var_e x;
v <-* var_e y;
var_e x *<- var_e v;
var_e y *<- var_e z
{{ (var_e x |~> cst_e b) ** (var_e y |~> cst_e a) }}.
Proof.
move=> x y z v a b Hvars.
apply hoare_lookup_back'' with (fun s h =>
(var_e x |~> cst_e a ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_s = a).
move=> s h H.
case_sepcon H.
exists (cst_e a).
Compose_sepcon h1 h2 => //.
rewrite /imp => h1' [X1 X2] h' Hh'.
rewrite /wp_assign.
split.
Compose_sepcon h1' h2; by Mapsto.
rewrite /=; repeat Store_upd => //.
apply hoare_lookup_back'' with (fun s h =>
(var_e x |~> cst_e a ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_ s = a /\ [ var_e v ]e_ s = b).
move=> s h [H1 H2].
case_sepcon H1.
exists (cst_e b).
Compose_sepcon h2 h1 => //.
rewrite /imp => h2' [X1 X2] h' Hh'.
rewrite /wp_assign.
split.
Compose_sepcon h1 h2'; by Mapsto.
rewrite /=.
by split; repeat Store_upd.
apply hoare_mutation_backwards'' with (fun s h =>
(var_e x |~> cst_e b ** var_e y |~> cst_e b) s h /\ [ var_e z ]e_s = a /\ [ var_e v ]e_s = b).
move=> s h [H1 [H2 H3]].
case_sepcon H1.
exists (cst_e a).
Compose_sepcon h1 h2 => //.
rewrite /imp => h1' [X1 X2] h' Hh'.
split.
Compose_sepcon h1' h2; by Mapsto.
done.
apply hoare_mutation_backwards'.
move=> s h /= [H1 [H2 H3] ].
case_sepcon H1.
exists (cst_e b).
Compose_sepcon h2 h1 => //.
rewrite /imp => h2' [X1 X2] h' Hh'.
Compose_sepcon h1 h2'; by Mapsto.
Qed.
Local Open Scope vc_scope.
Lemma vc_swap : forall x y z v a b, nodup (x :: y :: z :: v :: nil) ->
{{ (var_e x |~> cst_e a) ** (var_e y |~> cst_e b) }}
proj_cmd
(z <-*var_e x;
v <-* var_e y;
var_e x *<- var_e v;
var_e y *<- var_e z)
{{ (var_e x |~> cst_e b) ** (var_e y |~> cst_e a) }}.
Proof.
move=> x y z v a b Hvars.
apply wp_vc_util.
vc
move=> s h //=.
wp
rewrite /=.
exists (cst_e a).
move: H; apply assert_m.monotony => // h''; apply assert_m.currying => h0 H0.
exists (cst_e b) => /=.
have : ((var_e y |~> cst_e b) ** (var_e x |~> cst_e a))
(store.upd z ([ cst_e a ]e_ s) s) h0.
apply inde_upd_store.
apply inde_sep_con.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
assumption.
apply assert_m.monotony => // h''0; apply assert_m.currying => h1 H1.
exists (cst_e a).
have : ((var_e x |~> cst_e a) ** (var_e y |~> cst_e b)) (store.upd v b (store.upd z a s)) h1.
apply inde_upd_store.
apply inde_sep_con.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
assumption.
apply assert_m.monotony => // h''1; apply assert_m.currying => h2 H2.
exists (cst_e b).
move: H2; apply assert_m.monotony => // h''2; apply assert_m.currying => h3 H3.
case_sepcon H3.
Compose_sepcon h31 h32; by Mapsto.
Qed.
End Swap.
exists (cst_e a).
move: H; apply assert_m.monotony => // h''; apply assert_m.currying => h0 H0.
exists (cst_e b) => /=.
have : ((var_e y |~> cst_e b) ** (var_e x |~> cst_e a))
(store.upd z ([ cst_e a ]e_ s) s) h0.
apply inde_upd_store.
apply inde_sep_con.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
assumption.
apply assert_m.monotony => // h''0; apply assert_m.currying => h1 H1.
exists (cst_e a).
have : ((var_e x |~> cst_e a) ** (var_e y |~> cst_e b)) (store.upd v b (store.upd z a s)) h1.
apply inde_upd_store.
apply inde_sep_con.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
apply inde_mapsto => /=.
apply disj_singl; by Nodup_neq.
by apply disj_nil_L.
assumption.
apply assert_m.monotony => // h''1; apply assert_m.currying => h2 H2.
exists (cst_e b).
move: H2; apply assert_m.monotony => // h''2; apply assert_m.currying => h3 H3.
case_sepcon H3.
Compose_sepcon h31 h32; by Mapsto.
Qed.
End Swap.