Commit 9289ec98 authored by Armaël Guéneau's avatar Armaël Guéneau

StackDFS_proof: prove the termination

parent 636fc490
......@@ -184,6 +184,61 @@ Proof.
rew_listx in M. branches; autos*. }
Qed.
Definition count {A} (P : A -> Prop) (l: list A) :=
length (filter P l).
Definition measure C (L: list int) :=
count (= false) C + length L.
Lemma count_nonneg : forall A P (l: list A),
0 <= count P l.
Proof. intros. unfold count. applys~ length_nonneg. Qed.
Lemma count_cons : forall A (P: A -> Prop) x L,
count P (x :: L) = If P x then 1 + count P L else count P L.
Proof. intros. unfold count. rew_listx. case_if~. rew_listx~. Qed.
(* FIXME: lemmas about read and update are inconsistent.
For example:
- there is LibListZ.read_succ, but not LibListZ.update_succ
(only LibList.update_succ)
- there is read_cons_case, but not update_cons_case,
only update_cons_pos *)
Lemma count_update_remove : forall A `{Inhab A} (P: A -> Prop) L i x,
index L i ->
P L[i] ->
~ P x ->
count P L[i:=x] = count P L - 1.
Proof.
induction L; introv Ii PLi Px.
- destruct Ii. rew_list* in *.
- tests: (i = 0).
{ rewrite read_zero in PLi. rewrite update_zero.
rewrite !count_cons. repeat case_if*. }
{ rewrite read_cons_case in PLi. case_if~.
rewrite index_eq_inbound, length_cons in Ii.
rewrite* update_cons_pos. rewrite !count_cons. case_if~.
{ rewrite* IHL. rewrite* index_eq_inbound. }
{ rewrite~ IHL. rewrite* index_eq_inbound. } }
Qed.
Lemma measure_step : forall C L i,
index C i ->
C[i] = false ->
measure C[i:=true] (i :: L) = measure C L.
Proof.
introv Ii Ci. unfold measure. rew_listx.
erewrite~ count_update_remove. math.
Qed.
Lemma measure_nonneg : forall C L,
0 <= measure C L.
Proof.
intros. unfold measure.
forwards: count_nonneg (= false) C.
forwards*: length_nonneg L.
Qed.
Lemma reachable_imperative_spec : forall g G a b,
a \in nodes G ->
b \in nodes G ->
......@@ -200,45 +255,51 @@ Proof.
\* c ~> Array C
\* s ~> Stack L
\* \[inv G n a C L E]).
(* TODO: fix termination
set (W := lexico2 (binary_map (count (= true)) (upto n))
(binary_map (fun L:list int => LibList.length L) (downto 0))). *)
set (K := (fun (C: array bool) (L: list int) => bool_of (L <> nil))).
xseq (# Hexists C, hinv \{} C nil).
xwhile_inv_skip (fun (b:bool) => Hexists C L, hinv \{} C L \* \[b = isTrue (L<>nil)]).
(* TODO: xwhile_inv_basic (hinv \{}) W *)
xwhile_inv (fun (b:bool) (m:int) =>
Hexists C L, hinv \{} C L \*
\[b = isTrue (L<>nil)] \*
\[m = measure C L]
) (downto 0).
{ unfold hinv. hsimpl~. apply* inv_init. }
{ intros S LS r HS. unfold hinv at 1. xpull ;=> C L I Er.
{ intros S LS r m HS. unfold hinv at 1. xpull ;=> C L I Er Em.
(* while condition *)
xlet. xapps. xret. xpull ;=> E.
(* todo: simplify E *)
xif.
{ (* case loop step *)
xseq (Hexists C L, hinv \{} C L).
xseq (Hexists C' L', hinv \{} C' L' \* \[ measure C' L' < measure C L ]).
xapp*. intros L' HL'. subst L.
xfun as f. forwards~ [Gi Ci]: inv_stack I i.
xapp_spec iter_edges_remaining_spec
(>> (fun E => Hexists C2 L2, hinv E C2 L2 \* \[ C2[i] = true ]) G).
{ auto. }
xapp_spec~ iter_edges_remaining_spec
(>> (fun E =>
Hexists C2 L2, hinv E C2 L2 \*
\[ C2[i] = true ] \*
\[ measure C2 L2 = measure C L'])
G).
{ intros L. unfold hinv. applys heap_contains_intro (Hexists C2 L2,
c ~> Array C2 \* s ~> Stack L2 \*
\[ inv G n a C2 L2 L] \* \[ C2[i] = true]); hsimpl*.
\[ inv G n a C2 L2 L] \* \[ C2[i] = true]
\* \[ measure C2 L2 = measure C L' ]
); hsimpl*.
(* ça on automatisera plus tard avec une tactique *) }
{ introv N Hij. xpull. intros C2 L2 C2i.
{ introv N Hij. xpull. intros C2 L2 C2i Hm.
xapp_spec Sf.
unfold hinv at 1. xpull. intros I'.
xapps*. xif.
{ xapps*. xapp. intros _. unfold hinv. hsimpl.
{ rewrite* measure_step. rew_bool_eq~. }
{ rew_array*. case_if~. }
applys~ inv_step_push i. }
{ unfold hinv. xrets~. applys~ inv_step_skip j. } }
{ unfold hinv. hsimpl. apply~ inv_step_pop. }
{ rew_bool_eq~. }
{ hsimpl. }
{ intros C2 L2. xapplys~ HS. } }
{ intros ?. xpull;=> C2 L2 C2i Hm. hsimpl. rewrite Hm.
unfold measure. rew_listx. math. }
{ intros C2 L2 Hm. xapplys~ HS. lets*: measure_nonneg C2 L2. } }
{ (* case loop end *)
xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
{ intros r. hpull ;=> C L E. rew_bool_eq in *. subst L.
{ intros r. hpull ;=> m C L E Em. rew_bool_eq in *. subst L.
(* on pourra peut être essayer de patcher des x-tactiques
pour que le [rew_bool_eq] soit fait automatiquement? *)
hsimpl C. }
......@@ -246,6 +307,8 @@ Proof.
intro C. xpull. intros I. (* dans cfm2, c'est pratique on peut faire [xpull ;=> C I]
directement. il faudrait voir pour patcher [xpull] de cfml1 pour qu'il laisse
les quantificateurs en tête de la même manière *)
(* Armael: je ne sais pas comment implémenter ça. faire un pose mark /
gen_until_mark ne marche pas parce que xpull shuffle le contexte *)
lets: inv_length_C I.
xapp*. hsimpl. apply affine_Stack. (* à mettre en hint *)
forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment