Library insertionsort
Require Import programming.
Require Import listaux.
Require Import Omega.
Require Import Permutation.
Definition insertionsort:=
(
program_cons (statement_assignment (var_scope 1) (exp_constant (value_nat 1)) )
(program_loop
(loop_intro (exp_binoperation binoperation_lt (exp_variable (var_scope 1)) (exp_unioperation unioperation_len (exp_variable (var_scope 0))) )
(program_cons (statement_assignment (var_scope 2) (exp_binoperation binoperation_get (exp_variable (var_scope 0)) (exp_variable (var_scope 1)) ))
(program_cons (statement_assignment (var_scope 3) (exp_variable (var_scope 1)) )
(program_loop
(loop_intro (exp_binoperation binoperation_and
(exp_binoperation binoperation_lt (exp_constant (value_nat 0)) (exp_variable (var_scope 3)) )
(exp_binoperation binoperation_lt (exp_variable (var_scope 2)) (exp_binoperation binoperation_get (exp_variable (var_scope 0)) (exp_binoperation binoperation_minus (exp_variable (var_scope 3)) (exp_constant (value_nat 1)) ) ))
)
(program_cons (statement_listset (var_scope 0) (exp_variable (var_scope 3) ) (exp_binoperation binoperation_get (exp_variable (var_scope 0)) (exp_binoperation binoperation_minus (exp_variable (var_scope 3) ) (exp_constant (value_nat 1)) ) ) )
(program_cons (statement_assignment (var_scope 3) (exp_binoperation binoperation_minus (exp_variable (var_scope 3)) (exp_constant (value_nat 1)) ) )
program_nil))
)
(program_cons (statement_listset (var_scope 0) (exp_variable (var_scope 3)) (exp_variable (var_scope 2)) )
(program_cons (statement_assignment (var_scope 1) (exp_binoperation binoperation_plus (exp_variable (var_scope 1)) (exp_constant (value_nat 1)) ) )
program_nil)))))
)
program_nil)
).
Eval compute in
execute
insertionsort
(nil, ((value_listnat(4::6::2::8::1::nil))::nil) )
100.
Theorem insertionsort_preservedtype: forall (l:list nat),
invariant insertionsort (nil, (value_listnat l :: nil) )
(fun mem:memory=>
match variable_value mem (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output => True
end
).
Proof.
simpl.
set(PRESERVED:=fun m:memory=>_).
intros l.
unfold PRESERVED.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
clear l. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_loop.
apply invariant_loop_iterations. auto.
clear a l s INV. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
clear a l s INV. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
clear a l s INV. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_loop.
apply invariant_loop_iterations. auto.
clear a l s INV. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
clear a l s INV. intros mem INV.
destruct mem as [a s];simpl in INV;try inversion INV.
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
clear a l s INV. intros mem INV.
intros limit.
destruct limit;simpl;auto.
Qed.
Theorem insertionsort_invariant_1lower: forall (l:list nat),
invariant insertionsort (nil, (value_listnat l :: nil))
(fun mem:memory=>
match variable_value mem (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value mem (var_scope 1) with
| value_nat index => index<=S (length output)
| other => True
end
end
).
Proof.
set(LOWER:=fun m:memory=>_).
intros l.
unfold LOWER.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
omega. omega.
clear l. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_loop.
apply invariant_loop_iterations_informative. auto.
clear a l s INV. intros mem. destruct mem as [a s].
destruct s as [|var0 s];simpl;auto.
destruct s as [|var1 s];simpl;auto.
destruct var1 as [var1|var1|var1];simpl;auto.
destruct var0 as [var0|var0|var0];simpl;auto.
destruct(le_lt_dec _ _);simpl;auto. intros INV.
rewrite<- program_app_nil_l with (P:=program_cons (_ (var_scope 1) _) program_nil).
rewrite<- program_app_cons_fold.
rewrite<- program_app_loop_fold.
do 2 rewrite<- program_app_cons_fold.
set(P:=program_cons _ (program_cons _ (program_loop _ _))).
set(mem:=(a,_)).
set(LOWER':=fun m : memory =>
match variable_value m (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value m (var_scope 1) with
| value_none => True
| value_nat index => index < length output
| value_listnat _ => True
end
end).
assert(INVP: invariant P mem LOWER').
unfold P, LOWER', mem;clear P LOWER LOWER' mem.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
clear a var0 var1 s l INV. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_cons.
intros limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
clear a l s INV. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
apply invariant_loop.
apply invariant_loop_iterations. auto.
clear a l s INV. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
destruct v;simpl;auto. simpl in INV.
assert(L:=setandraise_longer l n (nth (n-1) l 0) 0). omega.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
destruct v;simpl;auto. simpl in INV.
assert(L:=setandraise_longer l n (nth (n-1) l 0) 0). omega.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct s;simpl;auto.
destruct v1;simpl;auto.
destruct v;simpl;auto. simpl in INV.
assert(L:=setandraise_longer l n (nth (n-1) l 0) 0). omega.
clear a l s INV. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
intros limit.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct v;simpl;auto. simpl in INV.
assert(L:=setandraise_longer l n0 n 0). omega.
destruct v0;simpl;auto.
destruct s;simpl;auto.
destruct v0;simpl;auto.
destruct v;simpl;auto. simpl in INV.
assert(L:=setandraise_longer l n0 n 0). omega.
set(B:=program_cons _ _).
assert(Happ:=program_app_invariant_informative P B mem LOWER' LOWER).
apply Happ;auto;
unfold LOWER',LOWER,B;clear LOWER a var0 var1 s l INV P mem INVP Happ LOWER' B.
intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct v;simpl;auto. simpl in INV. omega.
destruct limit;simpl;auto.
destruct s;simpl;auto.
destruct v;simpl;auto. simpl in INV. omega.
destruct s;simpl;auto.
destruct v;simpl;auto. simpl in INV. omega.
intros mem. destruct mem as [a s]. simpl.
destruct s;simpl;auto.
destruct v;simpl;auto.
destruct s;simpl;auto.
destruct v;simpl;auto. omega.
clear a l s INV. intros mem INV. destruct mem as [a s].
destruct s;simpl in INV;try inversion INV.
destruct v;simpl in INV;try inversion INV.
destruct limit;simpl;auto.
Qed.
Theorem insertionsort_finishes: forall (l:list nat),
program_finishes insertionsort (nil, (value_listnat l :: nil)) .
Proof.
intros.
apply finishes_cons.
set(MAIN_IND:=fun mem:memory=>
match variable_value mem (var_scope 1) with
| value_nat n =>
match variable_value mem (var_scope 0) with
| value_listnat l => (length l) -n
| other => 0
end
| other => 0
end
).
set(MAIN_INFO:=fun mem:memory=>
match variable_value mem (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value mem (var_scope 1) with
| value_nat index => index<=S (length output)
| other => True
end
end
).
set(INNER_LOOP:=loop_intro (exp_binoperation binoperation_and _ _) _).
set(MAIN_LOOP:=loop_intro _ _).
set(MAIN_LOOP_P:=program_cons _ (program_cons _ (program_loop _ _))) in MAIN_LOOP.
set(MAIN_LOOP_E:=exp_binoperation _ _ _) in MAIN_LOOP.
set(mem:=statement_execute _ _).
assert(DMAIN:=descending_loop_finishes_general_informative MAIN_LOOP_P MAIN_LOOP_E
mem MAIN_IND MAIN_INFO).
assert(DMAIN_PRE: MAIN_INFO mem).
unfold MAIN_INFO, mem. simpl. omega.
specialize(DMAIN DMAIN_PRE).
destruct(cast_value_bool (expression_value mem MAIN_LOOP_E)) eqn:MAIN_LOOP_E_0.
Focus 2. exists 2. simpl. simpl in MAIN_LOOP_E_0. rewrite MAIN_LOOP_E_0. omega.
assert(DMAIN_PRE2:
(forall mem' : memory,
MAIN_INFO mem' ->
let x := MAIN_IND mem' in
if cast_value_bool (expression_value mem' MAIN_LOOP_E)
then
0 < x /\
program_finishes_info MAIN_LOOP_P
(fun m : memory => MAIN_IND m < x /\ MAIN_INFO m) mem'
else True)
).
- clear l mem MAIN_LOOP_E_0 DMAIN DMAIN_PRE.
intros mem INFO IND. unfold MAIN_INFO in INFO. unfold MAIN_IND in IND. simpl.
destruct mem as [a [|v0 s]];simpl;auto.
destruct s as [|v1 s];simpl;auto.
destruct v1 as [|v1|v1];simpl;auto.
destruct v0 as [|v0|v0];simpl;auto.
simpl in INFO,IND.
destruct(le_lt_dec);simpl;auto.
apply conj. unfold IND. omega.
clear MAIN_LOOP MAIN_LOOP_E.
unfold MAIN_LOOP_P.
rewrite<- program_app_nil_l with (P:=program_cons (_ (var_scope 1) _) program_nil).
rewrite<- program_app_cons_fold.
rewrite<- program_app_loop_fold.
do 2 rewrite<- program_app_cons_fold.
set(MAIN_LOOP_PA:=program_cons _ (program_cons _ (program_loop _ _))).
set(MAIN_LOOP_PB:=program_cons _ _).
set(mem:=(a,_)).
set(MAIN_INFO':=fun m : memory =>
match variable_value m (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value m (var_scope 1) with
| value_none => False
| value_nat index => index=v1 /\ length output=length v0 /\ index<length output /\
match variable_value m (var_scope 3) with
| value_nat pos => pos<=index
| other => True
end
| value_listnat _ => False
end
end).
assert(CLAIM: program_finishes_info MAIN_LOOP_PA MAIN_INFO' mem).
+ unfold mem. clear MAIN_LOOP_P MAIN_LOOP_PB MAIN_INFO mem MAIN_IND.
unfold MAIN_LOOP_PA.
do 2 apply finishes_info_cons.
apply finishes_info_loop.
Focus 2. intros. exists 2. simpl. apply conj. omega.
revert H. unfold MAIN_INFO'. clear a s INFO IND.
rename v0 into initial_list. rename v1 into initial_index.
destruct m as [a s].
destruct s as [|v0 s];simpl;auto.
destruct v0 as [|v0|v0];simpl;auto.
destruct s as [|v1 s];simpl;auto.
destruct s as [|v2 s];simpl;auto.
destruct v2 as [|v2|v2];simpl;auto.
destruct s as [|v3 s];simpl;auto.
destruct v3 as [|v3|v3];simpl;auto.
destruct v1 as [|v1|v1];simpl;auto.
intros. destruct H as [Hindex [Hlist Hpos]]. apply conj;auto.
assert(L:=setandraise_equallength v0 v3 v2 0). omega.
clear MAIN_LOOP_PA.
set(mem:=statement_execute _ (statement_execute _ _)).
set(INNER_LOOP_E:=exp_binoperation binoperation_and _ _)in INNER_LOOP.
set(INNER_LOOP_P:=program_cons _ (program_cons _ _)) in INNER_LOOP.
set(INNER_IND:=fun mem:memory=>
match variable_value mem (var_scope 3) with
| value_nat i => i
| other => 0
end
).
set(INNER_INFO:=fun mem:memory=>MAIN_INFO' mem /\
match variable_value mem (var_scope 3) with
| value_nat i => True
| other => False
end
).
assert(DINNER:=descending_loop_finishes_general_informative INNER_LOOP_P INNER_LOOP_E
mem INNER_IND INNER_INFO).
assert(DINNER_PRE: INNER_INFO mem).
unfold INNER_INFO, MAIN_INFO', mem. simpl.
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
specialize(DINNER DINNER_PRE).
destruct(cast_value_bool (expression_value mem INNER_LOOP_E)) eqn:INNER_LOOP_E_0.
Focus 2. exists 2. simpl. simpl in INNER_LOOP_E_0. rewrite INNER_LOOP_E_0.
apply conj. omega. unfold MAIN_INFO',mem. simpl.
destruct s;simpl;auto. destruct s;simpl;auto.
assert(DINNER_PRE2:
(forall mem' : memory,
INNER_INFO mem' ->
let x := INNER_IND mem' in
if cast_value_bool (expression_value mem' INNER_LOOP_E)
then
0 < x /\
program_finishes_info INNER_LOOP_P
(fun m : memory => INNER_IND m < x /\ INNER_INFO m) mem'
else True)
).
* clear DINNER DINNER_PRE mem INNER_LOOP INNER_LOOP_E_0 a s INFO IND l.
intros mem INFO IND.
rename v0 into initial_list. rename v1 into initial_index.
unfold INNER_LOOP_E.
destruct mem as [a s]. simpl.
destruct INFO as [INFOM INFOI].
destruct s as [|v0 s];simpl;auto.
destruct s as [|v1 s];simpl;auto.
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
destruct v3 as [|v3|v3];simpl;auto.
unfold MAIN_INFO' in INFOM.
simpl in INFOM,INFOI. unfold IND;clear IND INFOI.
destruct v3 as [|v3];simpl;auto.
destruct v2 as [|v2|v2];simpl;auto.
destruct v0 as [|v0|v0];simpl;auto.
destruct (le_lt_dec _ _);simpl;auto.
unfold INNER_INFO, MAIN_INFO', INNER_IND, INNER_LOOP_P. simpl.
apply conj. omega.
exists 3. simpl. apply conj. auto.
apply conj. omega. apply conj;auto.
destruct v1 as [|v1|v1];simpl;auto.
destruct INFOM as [INFOindex [INFOlist [INFOlower INFOpos]]].
apply conj;auto.
destruct v0 as [|n v0];simpl. simpl in INFOlower. inversion INFOlower.
assert(Q:v3-0=v3). omega. rewrite Q in l|-*. clear Q.
destruct v3. simpl. destruct v0;simpl in *|-*;auto. exfalso. omega. omega.
assert(L:=setandraise_equallength v0 (S v3) (nth v3 v0 0) 0).
simpl in INFOlist,INFOlower,l.
rewrite<- L;try omega.
*specialize(DINNER DINNER_PRE2).
destruct DINNER as [limit HDINNER]. exists limit.
destruct(execute _ mem limit). destruct HDINNER as [Hn [Hm _]]. tauto.
+
destruct CLAIM as [limit CLAIM].
assert(Happ:=finishes_info_app MAIN_LOOP_PA MAIN_LOOP_PB
(fun m : memory => MAIN_IND m < IND /\ MAIN_INFO m) mem limit).
destruct(execute MAIN_LOOP_PA mem limit) as [An Am].
destruct CLAIM as [HAn CLAIM]. specialize(Happ HAn).
unfold MAIN_INFO' in CLAIM.
destruct Am as [Aa As].
destruct As as [|Av0 As];simpl in CLAIM. inversion CLAIM.
destruct Av0 as [|Av0|Av0];simpl in CLAIM. inversion CLAIM. inversion CLAIM.
destruct As as [|Av1 As];simpl in CLAIM. inversion CLAIM.
destruct Av1 as [|Av1|Av1];simpl in CLAIM. inversion CLAIM.
Focus 2. inversion CLAIM.
destruct CLAIM as [HAv1 [HAv0 [Hlower CLAIM]]].
rewrite HAv1 in Happ,Hlower,CLAIM;clear Av1 HAv1.
assert(HB:program_finishes_info MAIN_LOOP_PB
(fun m : memory => MAIN_IND m < IND /\ MAIN_INFO m)
(Aa, value_listnat Av0 :: value_nat v1 :: As)
).
exists 2. simpl. apply conj;auto. unfold MAIN_IND,MAIN_INFO,IND.
apply conj;simpl;omega.
specialize(Happ HB).
exact Happ.
-specialize(DMAIN DMAIN_PRE2).
destruct DMAIN as [limit DMAIN].
exists limit. fold MAIN_LOOP in DMAIN.
destruct(execute _ mem limit). tauto.
Qed.
Theorem insertionsort_sorted: forall (l:list nat),
postcondition insertionsort (nil, (value_listnat l :: nil) )
(fun mem:memory=> let (a,s):=mem in
match nth 0 s value_none with
| value_listnat output => issorted output
| other => False
end
).
Proof.
intros. set(PSORTED:=fun m:memory=>_).
unfold PSORTED. rename l into input.
apply postcondition_cons.
destruct input as [|input0 input].
unfold PSORTED;clear PSORTED. intro limit.
destruct limit;simpl;auto.
destruct limit;simpl;auto.
apply postcondition_loop_general with (FL:=
fun mem:memory=> let (a,s):=mem in
match nth 0 s value_none with
| value_listnat output =>
match nth 1 s value_none with
| value_nat n => n<=length output /\ issorted (firstn n output)
| other => False
end
| other => False
end
). clear PSORTED.
apply postcondition_loop_iterations_informative. simpl.
apply conj. omega. auto.
clear input0 input. intros mem.
destruct(cast_value_bool _) eqn:HE;auto.
destruct mem as [a s]. intros INV.
destruct s as [|v0 s];simpl in INV|-*;auto. inversion INV.
destruct v0 as [|v0|v0];simpl in INV|-*;auto. inversion INV. inversion INV.
apply postcondition_cons.
apply postcondition_cons.
set(INNER_POST:=fun m : memory =>
match variable_value m (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value m (var_scope 1) with
| value_none => False
| value_nat index => index<length output /\ issorted (firstn (S index) output) /\
match variable_value m (var_scope 2) with
| value_nat V =>
match variable_value m (var_scope 3) with
| value_nat pos => V <= nth pos output 0 /\ pos<=index
| other => False
end
| other => False
end
| value_listnat _ => False
end
end).
apply postcondition_loop_general with (FL:=INNER_POST).
-
set(INNER_PRE:=fun m : memory =>
match variable_value m (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value m (var_scope 1) with
| value_none => False
| value_nat index => index<length output /\ issorted (firstn index output) /\
match variable_value m (var_scope 2) with
| value_nat V =>
match variable_value m (var_scope 3) with
| value_nat pos => V <= nth pos output 0 /\ pos<=index /\
(issorted (firstn (S index) output) \/ pos=index)
| other => False
end
| other => False
end
| value_listnat _ => False
end
end).
apply postcondition_loop_iterations_special with (PRE:=INNER_PRE).
+
unfold INNER_PRE;clear INNER_PRE INNER_POST. simpl in *|-*.
destruct s as [|v1 s];simpl;auto. simpl in HE. inversion HE.
destruct v1 as [|v1|v1];simpl in HE. inversion HE. Focus 2. inversion HE.
destruct(le_lt_dec (length v0) v1) as [|Hlength]. simpl in HE. inversion HE.
clear HE. apply conj;auto. simpl in INV. destruct INV as [_ INV].
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
+
unfold INNER_POST;clear INNER_PRE INNER_POST.
destruct s as [|v1 s];simpl in HE. inversion HE.
destruct v1 as [|v1|v1];simpl in HE. inversion HE. Focus 2. inversion HE.
destruct(le_lt_dec (length v0) v1) as [|Hlength]. simpl in HE. inversion HE.
clear HE. simpl in INV. destruct INV as [_ INV].
intros HE.
assert(HE':
cast_value_bool
(if (cast_value_bool
(if le_lt_dec v1 0 then value_nat 0 else value_nat 1) &&
cast_value_bool
(if le_lt_dec (nth (v1 - 1) v0 0) (nth v1 v0 0)
then value_nat 0
else value_nat 1))%bool
then value_nat 1
else value_nat 0) = false
).
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto. simpl.
apply conj;auto.
destruct(le_lt_dec v1 0);simpl in *;auto.
destruct v0;auto. inversion Hlength.
destruct v1. apply conj;auto.
destruct s;simpl;auto. destruct s;simpl;auto.
inversion l.
apply conj. clear HE.
assert(minus0:forall n:nat, n-0=n). intros;omega.
destruct v0;auto.
destruct(le_lt_dec (nth (v1 - 1) (n :: v0) 0) (nth v1 (n :: v0) 0));
simpl in HE'.
destruct v1. inversion l.
clear a l s. revert n v1 Hlength INV l0. induction v0. auto.
intros. destruct v0. simpl. destruct v1;simpl;auto.
simpl in INV. destruct v1;simpl;auto.
destruct v1;simpl;auto.
specialize(IHv0 a v1).
assert(Hlength':S v1 < length (a :: n0 :: v0) ). simpl in *. omega.
assert(Hsorted': issorted (firstn (S v1) (a :: n0 :: v0)) ).
simpl in *. inversion INV;auto.
specialize(IHv0 Hlength' Hsorted'). simpl in IHv0.
rewrite minus0 in IHv0.
simpl in INV. inversion INV. constructor;auto.
inversion HE'.
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
+
unfold INNER_PRE, INNER_POST;clear a v0 s HE INV INNER_PRE INNER_POST.
intros mem.
destruct mem as [a s].
destruct s as [|v0 s];simpl;auto.
destruct s as [|v1 s];simpl;auto.
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
destruct v3 as [|v3|v3];simpl;auto.
destruct v3 as [|pv3];simpl;auto.
destruct v2 as [|v2|v2];simpl;auto.
destruct v0 as [|v0|v0];simpl;auto.
destruct(le_lt_dec _ _) as [_|Hlower];simpl;auto.
intros INV.
destruct v1 as [|v1|v1];simpl in INV;auto.
inversion INV. Focus 2. inversion INV.
destruct INV as [Hlength [Hsorted [Hlower' [Hindex HsortedP]]]].
assert(Q3:pv3-0=pv3). omega. rewrite Q3 in Hlower.
apply postcondition_cons.
apply postcondition_cons.
apply postcondition_nil. simpl. rewrite Q3.
destruct v0. inversion Hlength.
set(X:=setandraise _ _ _ _).
assert(CLAIMlength:v1 < length (n :: X)). unfold X.
simpl in *. rewrite<- setandraise_equallength;omega.
assert(CLAIMlower:v2 <= nth pv3 (n :: X) 0).
destruct pv3. simpl in *. omega.
simpl. unfold X. simpl in Hlength. rewrite setandraise_set;[|omega].
rewrite set_nth_different;[|omega]. simpl in *. omega.
assert(CLAIMindex:pv3<=v1). omega.
assert(CLAIMsorted:issorted (n :: firstn v1 X)). unfold X. Focus 1.
simpl in Hlength,Hlower'.
rewrite setandraise_set;[|omega].
destruct HsortedP as [HsortedP|HsortedP].
clear a v2 s Hlower Hlower' CLAIMlower Hsorted Q3 X CLAIMlength CLAIMindex.
clear Hlength Hindex. revert n v1 pv3 HsortedP.
induction v0.
intros. destruct pv3;simpl;auto.
intros. destruct pv3;simpl;auto. destruct v1;simpl;auto.
destruct v0;simpl;auto. destruct v1;simpl;auto.
simpl in HsortedP. inversion HsortedP. destruct v1;simpl;auto.
simpl in H3. inversion H3. constructor;auto. constructor;auto. omega.
destruct v1;simpl;auto.
specialize(IHv0 a v1 pv3). simpl in *. inversion HsortedP.
constructor;auto.
clear X CLAIMlength CLAIMlower CLAIMindex.
rewrite<- HsortedP in Hsorted, Hindex, Hlength|-*.
clear v1 HsortedP Q3 Hindex v2 Hlower Hlower' a s.
clear Hlength. simpl in Hsorted.
revert n pv3 Hsorted. induction v0.
intros. destruct pv3;simpl;auto.
intros. destruct pv3;simpl;auto.
specialize(IHv0 a pv3). simpl in Hsorted. inversion Hsorted.
constructor;auto.
assert(CLAIMsorted':issorted (firstn v1 (n :: X)) ).
apply issorted_firstn_S. simpl. assumption.
tauto.
- clear a v0 s HE INV.
unfold INNER_POST;clear INNER_POST.
intros mem H.
destruct mem as [a s].
destruct(cast_value_bool _) eqn:HE;auto.
destruct s as [|v0 s];simpl in H. inversion H.
destruct v0 as [|v0|v0];simpl in H;try inversion H.
destruct s as [|v1 s];simpl in H. inversion H.
destruct v1 as [|v1|v1];simpl in H. inversion H. Focus 2. inversion H.
destruct H as [Hlength [Hsorted H]].
destruct s as [|v2 s];simpl in H. inversion H.
destruct v2 as [|v2|v2];simpl in H. inversion H. Focus 2. inversion H.
destruct s as [|v3 s];simpl in H. inversion H.
destruct v3 as [|v3|v3];simpl in H. inversion H. Focus 2. inversion H.
destruct H as [Hlower Hpos]. simpl in *.
assert(ENDLOOP:v3=0 \/ (0<v3 /\ nth (v3 - 1) v0 0<=v2)).
destruct(le_lt_dec (nth (v3 - 1) v0 0) v2) as [Hhigh|Hhigh];simpl in HE.
destruct(le_lt_dec v3 0);simpl in HE;auto. apply or_introl. omega.
apply or_introl. destruct(le_lt_dec v3 0);simpl in HE.
destruct v3;auto. inversion l. inversion HE.
clear HE.
apply postcondition_cons.
apply postcondition_cons.
apply postcondition_nil. simpl.
rewrite plus_comm.
apply conj. rewrite<- setandraise_equallength;omega.
rewrite setandraise_set;[|omega].
clear a s.
destruct ENDLOOP.
+ rewrite H in Hlower,Hpos|-*. clear v3 H. simpl.
destruct v0;simpl;auto. destruct v0;simpl;destruct v1;simpl;auto.
simpl in *. inversion Hsorted. constructor;auto. omega.
+ destruct H as [Hv3 Hhigher].
destruct v0. inversion Hlength.
destruct v3. inversion Hv3. simpl in Hhigher.
assert(Q:v3-0=v3). omega. rewrite Q in Hhigher. clear Q Hv3.
revert n v1 v3 Hlength Hsorted Hlower Hpos Hhigher.
induction v0.
intros. destruct v3;simpl;auto.
intros. destruct v1;simpl;auto. simpl in Hsorted.
inversion Hsorted. destruct v3;simpl;auto.
constructor;auto. destruct v0;simpl;auto. destruct v1;simpl;auto.
destruct v1;simpl;auto. simpl in H3. inversion H3. constructor;auto.
simpl in Hlower. omega.
constructor;auto. simpl in IHv0. apply IHv0;auto;simpl in *;try omega.
- clear input0 input PSORTED. intros mem PRE.
destruct mem as [a s].
destruct s as [|v0 s];simpl in PRE. inversion PRE.
destruct v0 as [|v0|v0];simpl in PRE;try inversion PRE.
destruct s as [|v1 s];simpl in PRE. inversion PRE.
destruct v1 as [|v1|v1];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
simpl.
destruct(le_lt_dec (length v0) v1) as [HlengthH|HlengthH];simpl;auto.
apply postcondition_nil. simpl.
destruct PRE as [HlengthL SORTED].
apply firstn_issorted.
assert(Hlength:v1=length v0). omega.
rewrite<- Hlength. exact SORTED.
Qed.
Theorem insertionsort_permutes: forall (l:list nat),
postcondition insertionsort (nil, (value_listnat l :: nil) )
(fun mem:memory=> let (a,s):=mem in
match nth 0 s value_none with
| value_listnat output => Permutation output l
| other => False
end
).
Proof.
intros. set(PERMUTED:=fun m:memory=>_).
unfold PERMUTED. rename l into input.
apply postcondition_cons.
apply postcondition_loop_iterations_informative. apply Permutation_refl.
intros mem.
destruct(cast_value_bool _) eqn:HE;auto.
destruct mem as [a s].
intro PRE.
destruct s as [|v0 s];simpl in PRE. inversion PRE.
destruct v0 as [|v0|v0];simpl in PRE. inversion PRE. inversion PRE.
apply postcondition_cons.
apply postcondition_cons.
destruct s as [|v1 s];simpl in HE. inversion HE.
destruct v1 as [|v1|v1];simpl in HE. inversion HE. Focus 2. inversion HE.
destruct(le_lt_dec (length v0) v1) as [Hlength|Hlength];simpl in HE.
inversion HE. clear HE.
set(INNER_INV:=fun m : memory =>
match variable_value m (var_scope 0) with
| value_none => False
| value_nat _ => False
| value_listnat output =>
match variable_value m (var_scope 1) with
| value_none => False
| value_nat index =>
match variable_value m (var_scope 2) with
| value_nat V =>
match variable_value m (var_scope 3) with
| value_nat pos =>
pos<length output /\ Permutation (set pos output V) input
| other => False
end
| other => False
end
| value_listnat _ => False
end
end).
apply postcondition_loop_general with (FL:=INNER_INV).
-
apply postcondition_loop_iterations_informative.
+
unfold INNER_INV;clear INNER_INV PERMUTED. simpl in *.
assert(COMMON:v1 < length v0 /\ Permutation (set v1 v0 (nth v1 v0 0)) input).
apply conj. omega.
rewrite nth_set_same. assumption.
destruct s as [|v2 s];simpl;auto.
destruct s as [|v3 s];simpl;auto.
+
clear a v0 v1 s Hlength PRE.
unfold INNER_INV;clear PERMUTED INNER_INV.
intros mem.
destruct(cast_value_bool _) eqn:HE;auto.
intros PRE.
destruct mem as [a s].
destruct s as [|v0 s];simpl in PRE. inversion PRE.
destruct v0 as [|v0|v0];simpl in PRE. inversion PRE. inversion PRE.
destruct s as [|v1 s];simpl in PRE. inversion PRE.
destruct v1 as [|v1|v1];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
destruct s as [|v2 s];simpl in PRE. inversion PRE.
destruct v2 as [|v2|v2];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
destruct s as [|v3 s];simpl in PRE. inversion PRE.
destruct v3 as [|v3|v3];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
apply postcondition_cons.
apply postcondition_cons.
apply postcondition_nil.
simpl in *.
destruct(le_lt_dec v3 0) as [Hpos|Hpos];simpl in HE. inversion HE.
destruct(le_lt_dec (nth (v3 - 1) v0 0) v2) as [_|Hlower];simpl in HE.
inversion HE. clear HE.
destruct PRE as [Hlength Hpermuted].
apply conj.
rewrite<- setandraise_equallength. omega. auto.
rewrite setandraise_set;[|omega].
destruct v3. inversion Hpos. simpl.
assert(Q:v3-0=v3). omega. rewrite Q.
clear v1 s Hpos Hlower Q.
eapply perm_trans;[|apply Hpermuted].
apply Permutation_sym.
apply Permutation_set_displacement;auto.
-
clear a v0 v1 s Hlength PRE.
unfold INNER_INV;clear PERMUTED INNER_INV.
intros mem PRE.
destruct mem as [a s].
destruct s as [|v0 s];simpl in PRE. inversion PRE.
destruct v0 as [|v0|v0];simpl in PRE. inversion PRE. inversion PRE.
destruct s as [|v1 s];simpl in PRE. inversion PRE.
destruct v1 as [|v1|v1];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
destruct s as [|v2 s];simpl in PRE. inversion PRE.
destruct v2 as [|v2|v2];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
destruct s as [|v3 s];simpl in PRE. inversion PRE.
destruct v3 as [|v3|v3];simpl in PRE. inversion PRE. Focus 2. inversion PRE.
destruct PRE as [Hlength Hpermuted].
destruct(cast_value_bool _) eqn:HE. auto.
apply postcondition_cons.
apply postcondition_cons.
apply postcondition_nil.
simpl in *.
rewrite setandraise_set;auto.
Qed.
Theorem insertionsort_sorts: program_sorts insertionsort.
Proof.
assert(FINISHES:=insertionsort_finishes).
assert(SORTED:=insertionsort_sorted).
assert(PERMUTES:=insertionsort_permutes).
intro input.
specialize(FINISHES input).
destruct FINISHES as [limit FINISHED].
exists limit.
specialize(SORTED input limit).
specialize(PERMUTES input limit).
destruct(execute _ _ _).
apply conj;auto.
destruct m as [a s].
specialize(SORTED FINISHED).
specialize(PERMUTES FINISHED).
destruct s as [|v0 s];simpl in *. inversion SORTED.
destruct v0 as [|v0|v0];simpl in *.
inversion SORTED. inversion SORTED.
apply conj. exact PERMUTES. exact SORTED.
Qed.