Library programming

Require Import List.
Require Import Omega.
Require Import Permutation.

Require Import listaux.

Require Export programming_machine.

Definition invariant (P:program) (mem:memory) (F:memory->Prop):=
 forall limit:nat, let (n,m):=execute P mem limit in F m.

Theorem invariant_nil: forall (mem:memory) (F:memory->Prop),
F mem -> invariant program_nil mem F.
Proof.
intros.
destruct limit;simpl;auto.
Qed.

Theorem invariant_cons_execute: forall (P:program) (ST:statement)
(mem:memory) (F:memory->Prop),
 F mem ->
 (F mem ->invariant P (statement_execute ST mem) F) ->
 invariant (program_cons ST P) mem F.
Proof.
intros. intros limit.
destruct limit;simpl;auto.
specialize(H0 H limit).
destruct(execute P _ limit).
assumption.
Qed.

Theorem invariant_cons: forall (P:program) (ST:statement) (mem:memory) (F:memory->Prop),
 invariant (program_cons ST program_nil) mem F ->
 (forall mem':memory, F mem'->
  invariant P mem' F
 ) ->
 invariant (program_cons ST P) mem F.
Proof.
intros. intros limit.
assert(Hbase:=H 0). simpl in Hbase.
specialize(H limit).
destruct limit. simpl. exact Hbase.
simpl in H|-*.
set(m:=statement_execute _ _) in H|-*.
destruct limit. simpl in *|-*. exact H.
simpl in H. specialize(H0 m H (S limit)).
destruct(execute _ _ _).
exact H0.
Qed.

Theorem after_loop: forall (E:expression) (P:program) (mem:memory) (limit:nat),
let (n,m):=loop_execute (loop_intro E P) mem limit in
0<n -> if cast_value_bool (expression_value m E) then False else True.
Proof.
intros. revert mem. induction limit.
simpl. intros. inversion H.
intros. simpl.
destruct(cast_value_bool _) eqn:HE.
Focus 2. rewrite HE. auto.
clear HE.
destruct(execute P mem limit) as [Pn Pm].
specialize(IHlimit Pm).
destruct(loop_execute (loop_intro E P) Pm limit) as [Ln Lm].
destruct Pn;simpl. intros. inversion H.
destruct Ln;simpl;auto. intros _.
apply IHlimit. omega.
Qed.

Theorem invariant_loop_informative: forall (LE:expression) (LP P:program)
(mem:memory) (F:memory->Prop),
 invariant (program_loop (loop_intro LE LP) program_nil) mem F ->
 (forall mem':memory,
  if cast_value_bool (expression_value mem' LE) then True
  else F mem' -> invariant P mem' F
 ) ->
 invariant (program_loop (loop_intro LE LP) P) mem F.
Proof.
intros. intros limit. rename H0 into HP.
assert(Hbase:=H 0). simpl in Hbase.
specialize(H limit).
destruct limit. simpl. exact Hbase.
simpl in H|-*.
assert(AL:=after_loop LE LP mem limit).
destruct(loop_execute (loop_intro LE LP) mem limit) as [Ln Lm].
destruct Ln;simpl;auto.
specialize(HP Lm).
destruct(cast_value_bool (expression_value Lm LE)).
exfalso. apply AL. omega.
destruct limit;auto. simpl in H.
specialize(HP H (S limit)).
destruct(execute P Lm _) as [Pn Pm].
exact HP.
Qed.

Theorem invariant_loop: forall (P:program) (L:loop) (mem:memory) (F:memory->Prop),
 invariant (program_loop L program_nil) mem F ->
 (forall mem':memory, F mem' -> invariant P mem' F) ->
 invariant (program_loop L P) mem F.
Proof.
intros. intros limit.
assert(Hbase:=H 0). simpl in Hbase.
specialize(H limit).
destruct limit. simpl. exact Hbase.
simpl in H|-*.
destruct(loop_execute _ _ _).
destruct n;auto.
destruct limit. simpl in *|-*. exact H.
simpl in H. specialize(H0 m H (S limit)).
destruct(execute _ _ _).
exact H0.
Qed.

Theorem invariant_loop_iterations_informative: forall (E:expression) (P:program)
 (mem:memory) (F:memory->Prop),
 F mem->
 (forall mem':memory, if cast_value_bool (expression_value mem' E)
  then F mem'-> invariant P mem' F else True)->
 invariant (program_loop (loop_intro E P) program_nil) mem F.
Proof.
intros. intros limit. rename H0 into HI.
revert mem H.
induction limit. intros. simpl. exact H.
intros.
assert(HIs:=HI mem).
simpl.
set(X:=loop_execute _ _ _).
destruct limit. simpl. exact H.
simpl in X.
destruct(cast_value_bool (expression_value mem E));[|exact H].
specialize(HIs H limit).
destruct (execute P mem limit) as [Pn Pm].
specialize(IHlimit Pm HIs). simpl in IHlimit.
destruct(loop_execute (loop_intro E P) Pm limit) as [Ln Lm].
unfold X;clear X.
destruct Ln;simpl in *|-*.
destruct Pn;auto.
destruct Pn;auto. simpl.
destruct limit;simpl in IHlimit;auto.
Qed.

Theorem invariant_loop_iterations: forall (E:expression) (P:program)
 (mem:memory) (F:memory->Prop),
 F mem->
 (forall mem':memory, F mem'-> invariant P mem' F )->
 invariant (program_loop (loop_intro E P) program_nil) mem F.
Proof.
intros. apply invariant_loop_iterations_informative.
exact H.
intros.
destruct(cast_value_bool _);auto.
Qed.

Theorem invariant_cons_destroy: forall (ST:statement) (P:program)
 (mem:memory) (F:memory->Prop),
 invariant (program_cons ST P) mem F
 -> invariant (program_cons ST program_nil) mem F /\
 let (n,m):=execute (program_cons ST program_nil) mem 1 in
 invariant P m F.
Proof.
intros. apply conj.
- intros limit.
destruct limit;simpl;auto.
specialize(H 0). simpl in H. exact H.
specialize(H 1). simpl in H.
destruct limit;simpl;auto.
- simpl. intros limit. specialize(H (S limit)).
simpl in H.
destruct(execute P (statement_execute ST mem) limit) as [Pn Pm].
exact H.
Qed.

Fixpoint program_app (A B:program) :program:=
match A with
|program_nil => B
|program_cons ST P => program_cons ST (program_app P B)
|program_loop L P => program_loop L (program_app P B)
end.

Theorem execute_app: forall (A B:program) (mem:memory) (limit:nat),
exists limit':nat,
 execute(program_app A B) mem limit=
 let (n,m):=execute A mem limit in
 match n with
 | O=> (0,m)
 | S p => let (n',m'):=execute B m limit' in
     (match n' with O=>0|S _=>p+n' end,m')
 end.
Proof.
induction A.
+ intros.
exists limit. simpl.
destruct limit. simpl. auto.
simpl (execute program_nil _ _ ).
set(X:=execute B). simpl.
destruct(X mem _). destruct n;auto.
+ intros. rename s into ST.
simpl(program_app _ _).
destruct limit. exists 0. simpl. auto.
simpl(execute (program_cons ST _) _ _).
set(m:=statement_execute _ _).
specialize(IHA B m limit).
destruct IHA as [limit' IHA].
exists limit'.
rewrite IHA;clear IHA.
destruct(execute A m limit) as [An Am]. clear ST A limit m.
destruct(execute B Am limit') as [Bn Bm].
destruct An. auto.
destruct Bn. auto.
rewrite plus_comm. simpl.
f_equal. f_equal. omega.
+ intros. rename l into L.
simpl(program_app _ _).
destruct limit. exists 0. simpl. auto.
simpl(execute (program_loop _ _) _ _).
set(X:=loop_execute _ _).
destruct X as [Ln Lm].
specialize(IHA B Lm limit).
destruct IHA as [limit' IHA].
exists limit'.
rewrite IHA;clear IHA.
destruct(execute A Lm limit) as [An Am]. clear L A limit mem.
destruct Ln. auto.
destruct An. auto.
simpl.
destruct(execute B Am limit') as [Bn Bm].
destruct Bn. auto.
rewrite plus_comm. simpl.
f_equal. omega.
Qed.

Theorem program_app_nil_l: forall P:program, program_app program_nil P=P.
Proof.
auto.
Qed.

Theorem program_app_nil_r: forall P:program, program_app P program_nil=P.
Proof.
induction P.
- auto.
- simpl. rewrite IHP. auto.
- simpl. rewrite IHP. auto.
Qed.

Theorem program_app_cons_fold: forall (ST:statement) (A B:program),
program_app (program_cons ST A) B=program_cons ST (program_app A B).
Proof.
auto.
Qed.

Theorem program_app_loop_fold: forall (L:loop) (A B:program),
program_app (program_loop L A) B=program_loop L (program_app A B).
Proof.
auto.
Qed.

Theorem program_app_invariant_informative: forall (A B:program)
 (mem:memory) (F G:memory->Prop),
 invariant A mem F ->
 (forall mem':memory, F mem' -> invariant B mem' G) ->
 (forall mem':memory, F mem' -> G mem') ->
 invariant (program_app A B) mem G.
Proof.
intros. rename H into INVA.
rename H0 into INVB. rename H1 into SUB.
intros limit.
assert(Happ:=execute_app A B mem limit).
destruct Happ as [limit' Happ]. rewrite Happ.
assert(INVAlimit:=INVA limit).
destruct(execute A mem limit) as [An Am].
destruct An. apply SUB. assumption.
assert(INVBlimit':=INVB _ INVAlimit limit').
destruct(execute B Am limit') as [Bn Bm].
assumption.
Qed.

Definition postcondition (P:program) (mem:memory) (F:memory->Prop):=
 forall limit:nat, let (n,m):=execute P mem limit in 0<n -> F m.

Theorem invariant_postcondition: forall (P:program) (mem:memory) (F:memory->Prop),
invariant P mem F -> postcondition P mem F.
Proof.
intros. intros limit. specialize(H limit).
destruct(execute P mem limit);auto.
Qed.

Theorem postcondition_nil: forall (mem:memory) (F:memory->Prop),
F mem -> postcondition program_nil mem F.
Proof.
intros.
destruct limit;simpl;auto.
Qed.

Theorem postcondition_cons: forall (P:program) (ST:statement)
(mem:memory) (F:memory->Prop),
 postcondition P (statement_execute ST mem) F ->
 postcondition (program_cons ST P) mem F.
Proof.
intros. intros limit.
destruct limit;simpl. intros. inversion H0.
specialize(H limit).
destruct(execute P _ limit).
destruct n;simpl;auto.
intros. apply H. omega.
Qed.

Theorem postcondition_loop_general: forall (LE:expression) (LP P:program)
(mem:memory) (F FL:memory->Prop),
 postcondition (program_loop (loop_intro LE LP) program_nil) mem FL ->
 (forall mem':memory, FL mem' ->
  if cast_value_bool (expression_value mem' LE) then True
  else postcondition P mem' F
 ) ->
 postcondition (program_loop (loop_intro LE LP) P) mem F.
Proof.
intros. intros limit. rename H into POST. rename H0 into HP.
specialize(POST limit).
destruct limit;simpl. intros. inversion H.
assert(AL:=after_loop LE LP mem limit).
simpl in POST.
destruct(loop_execute (loop_intro LE LP) mem limit) as [Ln Lm].
destruct Ln;simpl. intros. inversion H.
specialize(HP Lm).
destruct(cast_value_bool (expression_value Lm LE)).
exfalso. apply AL. omega.
destruct limit. simpl. intros. inversion H.
simpl in POST.
assert(Q:0<S (S Ln)). omega. specialize(POST Q).
specialize(HP POST (S limit)).
destruct(execute P Lm _) as [Pn Pm].
destruct Pn;simpl;auto.
intros _. apply HP. omega.
Qed.

Theorem postcondition_loop_iterations_informative:
forall (E:expression) (P:program) (mem:memory) (F:memory->Prop),
 F mem->
 (forall mem':memory, if cast_value_bool (expression_value mem' E)
  then F mem'-> postcondition P mem' F else True)->
 postcondition (program_loop (loop_intro E P) program_nil) mem F.
Proof.
intros. rename H0 into HI. rename H into HF.
intros limit. revert mem HF. induction limit. simpl. intros. inversion H.
intros.
destruct limit;simpl;auto. simpl in IHlimit.
specialize(HI mem).
destruct(cast_value_bool (expression_value mem E));simpl;auto.
specialize(HI HF limit).
destruct limit. simpl. intros. inversion H.
destruct(execute _ mem (S limit)) as [Pn Pm].
destruct Pn;auto.
assert(Q:0<S Pn). omega. specialize(HI Q).
specialize(IHlimit Pm HI).
destruct(loop_execute _ Pm _) as [Ln Lm].
destruct Ln;simpl;auto. simpl in IHlimit.
intros _. apply IHlimit. omega.
Qed.

Theorem postcondition_loop_iterations_special:
forall (E:expression) (P:program) (mem:memory) (PRE POST:memory->Prop),
 PRE mem->
 (cast_value_bool (expression_value mem E)=false->POST mem)->
 (forall mem':memory, PRE mem'-> if cast_value_bool (expression_value mem' E)
  then postcondition P mem' (fun m=>PRE m/\ POST m) else True)->
 postcondition (program_loop (loop_intro E P) program_nil) mem POST.
Proof.
intros. rename H1 into HI. rename H into HPRE. rename H0 into NE.
intros limit. revert mem HPRE NE. induction limit. simpl. intros. inversion H.
intros.
destruct limit;simpl. intros. inversion H. simpl in IHlimit.
specialize(HI mem).
destruct(cast_value_bool (expression_value mem E));simpl;auto.
specialize(HI HPRE limit).
destruct limit. simpl. intros. inversion H.
destruct(execute _ mem (S limit)) as [Pn Pm].
destruct Pn. tauto.
assert(Q:0<S Pn). omega. specialize(HI Q).
destruct HI as [PPRE PPOST].
specialize(IHlimit Pm PPRE).
simpl. simpl in IHlimit.
destruct(cast_value_bool (expression_value Pm E));auto.
destruct(execute P Pm limit) as [PPn PPm].
destruct(loop_execute _ PPm _) as [Ln Lm].
destruct PPn;simpl;auto.
destruct Ln;simpl;auto. simpl in IHlimit.
intros _. apply IHlimit. auto. omega.
Qed.

Theorem program_app_postcondition: forall (A B:program)
 (mem:memory) (F G:memory->Prop),
 postcondition A mem F ->
 (forall mem':memory, F mem' -> postcondition B mem' G) ->
 postcondition (program_app A B) mem G.
Proof.
intros. rename H into POSTA. rename H0 into POSTB.
intros limit.
assert(Happ:=execute_app A B mem limit).
destruct Happ as [limit' Happ]. rewrite Happ;clear Happ.
specialize(POSTA limit).
destruct(execute A mem limit) as [An Am].
destruct An. intros. inversion H.
assert(Q:0<S An). omega. specialize(POSTA Q).
specialize(POSTB Am POSTA limit').
destruct(execute B Am limit') as [Bn Bm].
destruct Bn;auto.
intros _. apply POSTB. omega.
Qed.



Theorem program_greater_limit: forall (P:program) (mem:memory) (limit:nat),
 let (n,m):=execute P mem limit in 0<n ->
 forall limit':nat, limit<=limit' ->
  execute P mem limit'=(n,m).
Proof.
intros P.
pattern P.
set(F:=fun P:program=>_).
set(FL:=fun L:loop=>
forall (mem : memory) (limit : nat),
     let (n, m) := loop_execute L mem limit in
     0 < n ->
     forall limit' : nat, limit <= limit' -> loop_execute L mem limit' = (n, m)
).
assert(R:=program_loop_rect F FL). apply R; unfold F, FL;clear R F FL.
+ intros. destruct limit. simpl. intros. inversion H.
simpl. intros _ limit' Hlimit.
destruct limit'. inversion Hlimit. simpl. auto.
+intros. rename H into IH. clear P. rename p into P.
rename s into ST.
destruct limit. simpl. intros. inversion H.
simpl. set(STm:=statement_execute _ _).
specialize(IH STm limit).
destruct(execute P STm limit) as [Pn Pm].
destruct Pn. intros. inversion H.
intros _ limit' Hlimit.
assert(Q:0<S Pn). omega. specialize(IH Q). clear Q.
destruct limit'. inversion Hlimit.
assert(Hlimit':limit<=limit'). omega.
specialize(IH limit' Hlimit').
simpl. fold STm. rewrite IH. auto.
+intros. clear P. rename p into P. rename H into IHL. rename H0 into IH.
rename l into L.
destruct limit. simpl. intros. inversion H.
simpl.
specialize(IHL mem limit).
destruct(loop_execute L mem limit) as [Ln Lm].
specialize(IH Lm limit).
destruct(execute P Lm limit) as [Pn Pm].
destruct Ln. intros. inversion H.
destruct Pn. intros. inversion H.
intros _ limit' Hlimit.
assert(Q:0<S Pn). omega. specialize(IH Q). clear Q.
destruct limit'. inversion Hlimit.
assert(Hlimit':limit<=limit'). omega.
specialize(IH limit' Hlimit').
assert(Q:0<S Ln). omega.
specialize(IHL Q limit' Hlimit'). clear Q.
simpl.
destruct(loop_execute L mem _).
inversion IHL. clear IHL H0 H1 n m.
rewrite IH. simpl. auto.
+ clear P. intros E P IH mem limit.
revert mem.
induction limit. simpl. intros. inversion H.
simpl.
intros.
set(Es:=cast_value_bool _).
assert(HEs:exists X, Es=X). exists Es. auto.
destruct HEs as [X HEs]. rewrite HEs. destruct X.
* specialize(IH mem limit).
destruct(execute P mem limit) as [Pn Pm].
destruct Pn. intros. inversion H.
specialize(IHlimit Pm).
destruct(loop_execute _ Pm limit) as [Ln Lm].
destruct Ln. intros. inversion H.
intros _ limit' Hlimit.
destruct limit'. inversion Hlimit.
assert(Hlimit':limit<=limit'). omega.
assert(Q:0<S Pn). omega.
specialize(IH Q limit' Hlimit'). clear Q.
assert(Q:0<S Ln). omega.
specialize(IHlimit Q limit' Hlimit'). clear Q.
simpl. fold Es. rewrite HEs.
rewrite IH. rewrite IHlimit. auto.
* intros _ limit' Hlimit. destruct limit'. inversion Hlimit.
simpl. fold Es. rewrite HEs. auto.
Qed.

Theorem loop_greater_limit: forall (L:loop) (mem:memory) (limit:nat),
 let (n,m):=loop_execute L mem limit in 0<n ->
 forall limit':nat, limit<=limit' ->
  loop_execute L mem limit'=(n,m).
Proof.
intros.
assert(G:=program_greater_limit (program_loop L program_nil) mem (S limit) ).
simpl in G.
destruct limit. simpl. intros. inversion H.
destruct(loop_execute L mem _) as [Ln Lm]. simpl in G.
destruct Ln. intros. inversion H.
intros _ limit' Hlimit.
assert(Q:0<S (S Ln)). omega.
assert(Hlimit':S(S limit) <= S limit'). omega.
specialize(G Q _ Hlimit').
simpl in G.
destruct limit'. inversion Hlimit.
destruct(loop_execute L mem _). simpl in G.
destruct n;simpl. inversion G. inversion G. auto.
Qed.

Fixpoint program_chain (P:program) (mem:memory) (niter limit:nat):=
match niter with
|O=>(1,mem)
|S piter=>
 let (n1,m1):=execute P mem limit in
 match n1 with
 |O => (0,m1)
 |S _ =>
  let (n2,m2):=program_chain P m1 piter limit in
   (match n2 with O=>0| S_=>n1+n2 end,m2)
 end
end.

Theorem program_chain_greater_limit: forall (P:program) (mem:memory)
 (niter limit:nat),
 let (n,m):=program_chain P mem niter limit in 0<n ->
 forall limit':nat, limit<=limit' ->
  program_chain P mem niter limit'=(n,m).
Proof.
intros. revert mem. induction niter.
+ simpl. intros. auto.
+ intros. simpl.
assert(G:=program_greater_limit P mem limit).
destruct(execute P mem limit) as [Pn Pm].
specialize(IHniter Pm).
destruct(program_chain P Pm niter limit) as [Cn Cm].
destruct Pn. intros. inversion H.
destruct Cn. intros. inversion H.
intros _ limit' Hlimit.
assert(Q:0<S Pn). omega. specialize(G Q limit' Hlimit);clear Q.
rewrite G;clear G.
assert(Q:0<S Cn). omega. specialize(IHniter Q limit' Hlimit);clear Q.
rewrite IHniter. auto.
Qed.

Theorem loop_iterations_induction: forall (E:expression) (P:program) (mem:memory)
 (limit:nat),
  let (nf,mf):=loop_execute (loop_intro E P) mem limit in 0<nf->
 exists nit:nat,
  let (ni,mi):=program_chain P mem nit limit in
  0<ni /\ mi=mf.
Proof.
intros. revert mem.
induction limit. simpl. intros. inversion H.
intros.
simpl.
destruct(cast_value_bool _);[|exists 0;simpl;auto].
assert(GP:=program_greater_limit P mem limit).
destruct(execute P mem limit) as [Pn Pm].
specialize(IHlimit Pm).
destruct(loop_execute _ Pm limit) as [Ln Lm].
destruct Pn. intros. inversion H.
destruct Ln. intros. inversion H.
assert(Q:0 < S Ln). omega. specialize(IHlimit Q). clear Q.
destruct IHlimit as [nit IH].
intros _.
exists (S nit).
assert(Q:0< S Pn). omega.
assert(Hlimit: limit<=S limit). omega.
specialize(GP Q (S limit) Hlimit). clear Q.
red. fold program_chain.
rewrite GP. clear GP.
assert(G:=program_chain_greater_limit P Pm nit limit).
destruct(program_chain P Pm nit limit) as [Cn Cm].
destruct IH as [HCn HCm].
specialize(G HCn (S limit) Hlimit).
rewrite HCm in G. clear Cm HCm.
rewrite G.
destruct Cn. inversion HCn.
apply conj;auto.
omega.
Qed.

Definition program_finishes (P:program) (mem:memory):= exists limit:nat,
let (n,m):=execute P mem limit in 0<n.

Definition program_finishes_info (P:program) (INFO:memory->Prop) (mem:memory):=
exists limit:nat, let (n,m):=execute P mem limit in 0<n /\ INFO m.


Theorem descending_loop_finishes_general_informative:
forall (P:program) (E:expression) (mem:memory) (F:memory->nat) (G:memory->Prop),
G mem ->
(
if cast_value_bool(expression_value mem E) then
 forall mem': memory, G mem'->
    let x:=F mem' in
      (if cast_value_bool(expression_value mem' E) then
       0<x /\ program_finishes_info P (fun m=>F m<x/\ G m) mem'
      else True)
else True
)->
program_finishes_info (program_loop (loop_intro E P) program_nil ) G mem.
Proof.
intros. rename H into HG. rename H0 into H.
set(Es:=cast_value_bool (expression_value mem E)) in H.
assert(exists b, Es=b). exists Es. auto.
destruct H0 as [b HEs].
destruct b.
Focus 2. exists 2. simpl. fold Es. rewrite HEs. auto.
rewrite HEs in H.
set(n:=F mem).
assert(X:exists n', n=n'). exists n. auto.
destruct X as [n' Hn].
unfold Es in HEs. clear Es.
unfold n in Hn. clear n. rename n' into n.
revert mem HEs Hn HG. simpl in H.
assert(CLAIM:
forall mem : memory,
cast_value_bool (expression_value mem E) = true ->
F mem <= n -> G mem ->
program_finishes_info (program_loop (loop_intro E P) program_nil) G mem
). -
induction n.
+ intros mem HEs Hn HG. specialize(H mem HG). rewrite HEs in H.
destruct(F mem). inversion H. inversion H0. inversion Hn.
+ intros mem HEs Hn HG. specialize(H mem HG). rewrite HEs in H.
destruct(F mem). inversion H. inversion H0.
destruct H as [Hn0 H].
destruct H as [Plimit HP].
destruct (execute P mem Plimit) as [Pn Pm] eqn:HXP.
destruct HP as [HPn [HP HPG]].
assert(HP':F Pm<= n). omega. clear n0 Hn0 Hn HP. rename HP' into HP.
specialize(IHn Pm).
destruct(cast_value_bool (expression_value Pm E)) eqn:HEP.
specialize(IHn (eq_refl)).

Focus 2. exists (S(S Plimit)). simpl. destruct Plimit.
simpl in HXP. inversion HXP. rewrite<- H0 in HPn. inversion HPn.
rewrite HXP. rewrite HEs.
destruct Pn. inversion HPn. simpl. rewrite HEP.
apply conj. omega. assumption.

specialize(IHn HP).
destruct IHn as [Llimit IH]. assumption.
exists (S(S(Plimit + Llimit))).
simpl.
rewrite HEs.
assert(GP:=program_greater_limit P mem Plimit).
rewrite HXP in GP.
assert(Q:Plimit<=Plimit+Llimit). omega.
specialize(GP HPn (Plimit+Llimit) Q). clear Q.
rewrite GP.
destruct Pn. inversion HPn.
assert(GL:=program_greater_limit (program_loop (loop_intro E P) program_nil) Pm Llimit).
destruct(execute _ Pm Llimit) as (Ln,Lm) in IH,GL.
assert(Q:Llimit<=S(Plimit+Llimit)). omega.
destruct IH as [IH IHG].
specialize(GL IH _ Q). clear Q.
simpl in GL.
destruct(loop_execute _ Pm _).
destruct n0. inversion GL. rewrite<- H0 in IH. inversion IH.
simpl. apply conj. omega.
destruct Plimit. simpl in GL.
destruct Llimit. simpl in GL. inversion GL. rewrite<- H0 in IH. inversion IH.
simpl in GL. inversion GL. assumption.
simpl in GL. inversion GL. assumption.

- intros. apply CLAIM. auto.
rewrite Hn. auto. assumption.
Qed.

Theorem descending_loop_finishes_general: forall (P:program) (E:expression)
(mem:memory) (F:memory->nat),
(
if cast_value_bool(expression_value mem E) then
 forall mem': memory,
    let x:=F mem' in
      (if cast_value_bool(expression_value mem' E) then
       0<x /\ exists limit:nat, let(n,m):=execute P mem' limit in 0<n /\ F m<x
      else True)
else True
)->
program_finishes (program_loop (loop_intro E P) program_nil ) mem.
Proof.
intros.
assert(DLGI:=descending_loop_finishes_general_informative P E mem F
 (fun _=>True) I).
simpl in DLGI.
assert(DLGI_PRE:(if cast_value_bool (expression_value mem E)
        then
         forall mem' : memory,
         True ->
         if cast_value_bool (expression_value mem' E)
         then
          0 < F mem' /\
          (exists limit : nat,
             let (n, m) := execute P mem' limit in
             0 < n /\ F m < F mem' /\ True)
         else True
        else True) ).
destruct (cast_value_bool _);simpl;auto.
intros. specialize(H mem').
destruct (cast_value_bool _);simpl;auto. simpl in H.
destruct H as [HF [limit H]].
apply conj;auto. exists limit.
destruct(execute P mem' limit) as [Pn Pm]. tauto.
specialize(DLGI DLGI_PRE);clear DLGI_PRE.
destruct DLGI as [limit DLGI].
exists limit.
destruct(execute _ mem limit) as [n m]. tauto.
Qed.

Theorem finishes_info_True: forall (P:program) (mem:memory),
program_finishes P mem <-> program_finishes_info P (fun m=>True) mem.
Proof.
intros. apply conj.
- intros H. destruct H as [limit H].
exists limit.
destruct(execute P mem limit) as [n m]. tauto.
- intros H. destruct H as [limit H].
exists limit.
destruct(execute P mem limit) as [n m]. tauto.
Qed.

Theorem finishes_info_cons: forall (ST:statement) (P:program)
(INFO:memory->Prop) (mem:memory),
let (n,m):=execute (program_cons ST program_nil) mem 2 in
program_finishes_info P INFO m
-> program_finishes_info (program_cons ST P) INFO mem.
Proof.
intros.
simpl.
set(STm:=statement_execute ST mem).
intros. destruct H as [limit H].
exists (S limit). simpl. fold STm.
destruct(execute P STm limit).
destruct H as [Hn H].
destruct n;auto.
Qed.

Theorem finishes_cons: forall (ST:statement) (P:program) (mem:memory),
let (n,m):=execute (program_cons ST program_nil) mem 2 in
program_finishes P m
-> program_finishes (program_cons ST P) mem.
Proof.
intros.
simpl.
set(STm:=statement_execute ST mem).
intros. destruct H as [limit H].
exists (S limit). simpl. fold STm.
destruct(execute P STm limit).
destruct n;auto.
Qed.

Theorem finishes_info_loop: forall (L:loop) (P:program)
(INFO:memory->Prop) (mem:memory),
program_finishes_info (program_loop L program_nil) INFO mem ->
(forall m:memory, INFO m->program_finishes_info P INFO m)->
program_finishes_info (program_loop L P) INFO mem.
Proof.
intros.
destruct H as [Llimit HL].
destruct(execute (program_loop L program_nil) mem Llimit) as [Ln Lm] eqn:HXL.
rename H0 into HP. destruct HL as [HL HINFO].
specialize(HP Lm HINFO). destruct HP as [Plimit HP].
exists (S(Llimit + Plimit)). simpl.
assert(GL:=program_greater_limit (program_loop L program_nil) mem Llimit).
rewrite HXL in GL.
assert(Q:Llimit<=S(Llimit+Plimit)). omega.
specialize(GL HL _ Q). clear Q. simpl in GL.
destruct(loop_execute L mem (Llimit + Plimit)) as [Ln' Lm'].
destruct Ln'. inversion GL. rewrite<- H0 in HL. inversion HL.
assert(GP:=program_greater_limit P Lm Plimit).
destruct(execute P Lm Plimit) as [Pn Pm].
assert(Q:Plimit<=Llimit + Plimit). omega.
destruct HP as [HP HPINFO].
specialize(GP HP _ Q). clear Q.
destruct Llimit. simpl in HXL. inversion HXL. rewrite<- H0 in HL. inversion HL.
simpl in GL. inversion GL. rewrite GP.
destruct Pn;auto.
apply conj. omega. assumption.
Qed.

Theorem finishes_loop: forall (L:loop) (P:program) (mem:memory),
program_finishes (program_loop L program_nil) mem ->
(forall m:memory, program_finishes P m)->
program_finishes (program_loop L P) mem.
Proof.
intros.
apply<- finishes_info_True.
apply finishes_info_loop.
-apply finishes_info_True. exact H.
- intros. apply finishes_info_True. apply H0.
Qed.

Theorem program_app_finishes_destroy: forall (A B:program) (mem:memory),
program_finishes (program_app A B) mem ->
exists limit:nat, let (n,m):=execute A mem limit in
0<n /\ program_finishes B m.
Proof.
intros.
destruct H as [limit H].
assert(Happ:=execute_app A B mem limit).
destruct Happ as [Blimit Happ].
exists limit.
destruct(execute A mem limit) as [An Am].
destruct(execute (program_app A B) mem limit) as [ABn ABm].
destruct An. inversion Happ. rewrite H1 in H. inversion H.
apply conj. omega.
exists Blimit.
destruct(execute B Am Blimit).
destruct n.
inversion Happ. rewrite H1 in H. exact H.
omega.
Qed.

Theorem finishes_info_app: forall (A B:program) (INFO:memory->Prop) (mem:memory)
(limit:nat),
let (n,m):=execute A mem limit in 0<n ->
program_finishes_info B INFO m
-> program_finishes_info (program_app A B) INFO mem.
Proof.
intros A B INFO. induction A.
- intros. destruct limit;simpl;auto.
- intros. destruct limit;simpl;auto. intros. inversion H.
set(STm:=statement_execute _ _ ).
specialize(IHA STm limit ).
destruct(execute A STm limit) as [An Am].
destruct An;simpl;auto. intros. inversion H. intros _ HB.
assert(Q:0<S An). omega.
specialize(IHA Q HB). clear Q. clear limit HB An Am.
destruct IHA as [limit IHA]. exists (S limit).
simpl. fold STm.
destruct(execute _ STm limit).
destruct n;simpl;auto. apply conj. omega. tauto.
-intros. destruct limit;simpl;auto. intros. inversion H.
destruct(loop_execute l mem limit) as [Ln Lm] eqn:HL.
specialize(IHA Lm limit ).
destruct(execute A Lm limit) as [An Am].
destruct Ln;simpl;auto. intros. inversion H.
destruct An;simpl;auto. intros. inversion H. intros _ HB.
assert(Q:0<S An). omega.
specialize(IHA Q HB). clear Q.
destruct IHA as [limit' IHA]. exists (S limit +limit').
simpl.
assert(GL:=loop_greater_limit l mem limit). rewrite HL in GL.
assert(Q:0<S Ln). omega.
assert(Hlimit:limit<=limit+limit'). omega.
specialize(GL Q _ Hlimit). rewrite GL;clear GL.
assert(GP:=program_greater_limit (program_app A B) Lm limit').
destruct(execute (program_app A B) Lm limit') as [Pn Pm].
destruct IHA as [HPn HINFO].
assert(Hlimit': limit'<=limit+limit'). omega.
specialize(GP HPn _ Hlimit'). rewrite GP;clear GP.
apply conj;auto.
destruct Pn;simpl;auto. omega.
Qed.

Theorem finishes_postcondition: forall (P:program) (mem:memory) (POST:memory->Prop),
postcondition P mem POST -> program_finishes P mem ->
program_finishes_info P POST mem.
Proof.
intros. destruct H0 as [limit Hfinish].
specialize(H limit). exists limit.
destruct(execute P mem limit);auto.
Qed.

Definition program_sorts (P:program):= forall l:list nat, exists (limit:nat),
 let (n,m):=execute P (nil, (value_listnat l::nil)) limit in
 0<n /\
 match variable_value m (var_scope 0) with
 |value_none => False
 |value_nat _ => False
 |value_listnat output => Permutation output l /\ issorted output
 end.