Commit abbfe37d authored by charguer's avatar charguer

more

parent 245cfb14
......@@ -89,14 +89,29 @@ Lemma inv_init : forall G n a C,
a \in nodes G ->
inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
(* Ici il faudrait pousser une version spécialisée du lemme [mem_one_eq] (?),
qui dit [mem i (a::nil) = (i = a)], à utiliser dans les branches.
Ou alors, s'appuyer sur [rew_listx] qui devrait faire cette réécriture. *)
introv Ha EC Ga. constructors.
{ subst C. rew_array~. destruct~ Ha. }
{ subst C. rew_array~.
destruct~ Ha. (* should be auto *) }
{ rew_array. case_if~. subst C. apply~ index_make. }
{ introv H. inverts H as H.
{ splits~. rew_array~. case_if~. }
{ splits~. rew_array~. case_if~.
(* il faudrait introduire une tactique qui fait
[rew_array; repeat case_if], mais avec la subtilité
que ça ne fait [case_if] que sur le [if] introduit
par les [read_update] sur les tableaux. On peut coder
ça en utilisant une base de hint différentes que rew_array,
et une marque identité qu'une variante de [case_if] pourrait
reconnaitre spécifiquement. On peut, en option, avoir une
variante qui effectue des [subst] sur les égalités générées
par [case_if] *) }
{ inverts H. } }
{ introv Gi H. assert (i = a) as ->.
{ subst C. rew_array~ in H. case_if~. }
{ subst C. rew_array~ in H. case_if~.
(* idem, c'est un [rew_array;case_if] *) }
(* ici je ferai un lemma dans DFS_proof pour reachable_refl *)
exists (nil:path). constructors*. }
{ introv Ci E. assert (i = a) as ->.
{ subst C. rew_array~ in Ci. case_if~. }
......@@ -114,17 +129,24 @@ Proof.
{ rew_array~. case_if~. }
{ intros i' M'. rew_listx in M'. destruct M' as [-> | M'].
- splits. now applys~ (>> has_edge_nodes i j). rew_array~. case_if~.
- rew_array~. case_if~. splits~. subst i'. applys~ has_edge_nodes i j. }
- rew_array~. case_if~.
splits~. subst i'. applys~ has_edge_nodes i j. (* toute la ligne devrait etre auto *) }
{ intros k Hk Ck. rew_array~ in Ck. case_if~. subst k.
forwards~ Ri: inv_true_reachable0 i. { applys~ has_edge_nodes i j. }
forwards~ Ri: inv_true_reachable0 i.
{ applys~ has_edge_nodes i j. } (* à automatiser *)
skip. (* use rtclosure from LibRelation *) }
{ intros i' j' Ci' E.
rewrite read_update_case in Ci' by skip.
case_if~. { subst i'. rew_listx~. }
rewrite read_update_case in Ci' by skip. (* à automatiser *)
case_if~. { subst i'. rew_listx~. } (* utiliser la variante de case_if
(à définir?) qui fait le subst sur lgalité produite.
ensuite, eauto sait prouver [mem j (j::l)] ou du moins devrait le faire. *)
forwards~ [H|[H|H]]: inv_true_edges0 i' j'.
- rew_array~. case_if~.
- rew_set in H. branches; auto_tilde. subst j'.
rewrite~ read_update_same. }
(* pour la ligne du dessus, il faudrait définir [set_in H],
qui fait un [rew_set in H] puis un [branches in H as H], puis un
[try subst H] sur les égalités générées. *)
rewrite~ read_update_same. (* celui là c'est rew_array qui doit le gérer *) }
Qed.
Lemma inv_step_skip : forall G n a C L j js,
......@@ -135,7 +157,7 @@ Proof.
introv I Cj. inverts I. constructors; auto.
{ intros i' j' Ci' E.
lets [M|[M|M]]: inv_true_edges0 Ci' E; [ eauto | eauto | ].
rew_set in M. destruct~ M. subst*. }
rew_set in M. destruct~ M. subst*. (* set_in M devrait faire ça *) }
Qed.
Lemma inv_end : forall G n a C,
......@@ -148,7 +170,7 @@ Proof.
generalize a as i. intros i P. induction P.
{ auto. }
{ introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H.
{ inverts M. }
{ inverts M. } (* [rew_list in *; auto_false] devrait prouver les 3 buts *)
{ auto. }
{ inverts M. } } }
{ applys* inv_true_reachable. }
......@@ -159,10 +181,18 @@ Lemma inv_step_pop : forall G n a C i L,
inv G n a C L (out_edges G i).
Proof.
introv I. destruct I. constructors~.
intros i' j ? ?.
forwards~ [M|[M|M]]: inv_true_edges0 i' j.
rew_listx in M. branches; try tauto. subst i'.
right. right. rewrite~ out_edges_has_edge.
{ intros i' j ? ?. (* nommer les hypothèses c'est mieux *)
forwards~ [M|[M|M]]: inv_true_edges0 i' j.
(* il faudrait peut être que je définisse une tactic
[forwards_branches M: inv_true_edges0 i' j] qui évite
de se taper le intro_pattern tout moche *)
rew_listx in M. branches; try tauto. subst i'.
(* [branch 3] est mieux que right; right. *)
right. right.
rewrite~ out_edges_has_edge. (* side-condition à automatiser *)
(* du coup, le [branch 3] n'est plus nécessaire techniquement,
eauto fera tout. C'est trivial que [has_edge i j] implique
[j \in out_edges i]. *) }
Qed.
......@@ -204,23 +234,34 @@ Proof.
{ auto. }
{ 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*. }
{ introv N Hij. xpull. intros C2 L2 ?. xapp_spec Sf.
\[ inv G n a C2 L2 L] \* \[ C2[i] = true]); hsimpl*.
(* ça on automatisera plus tard avec une tactique *) }
{ introv N Hij. xpull. intros C2 L2 ?. (* nommer toutes les hyps *)
xapp_spec Sf.
unfold hinv at 1. xpull. intros I'.
xapps. skip.
xif.
{ xapps. skip. xapp. intros _. unfold hinv. hsimpl.
{ rewrite read_update_case. case_if~. skip. }
{ rewrite read_update_case. case_if~. skip.
(* toute la ligne: utiliser [rew_array] étendu avec [case_if] *) }
applys~ inv_step_push i. }
{ xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } }
{ (* mieux: [unfold hinv. xrets~. applys~ inv_step_skip j.] *)
xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } }
{ unfold hinv. hsimpl. apply~ inv_step_pop. }
{ rew_bool_eq~. }
{ hsimpl. }
{ intros C2 L2. xapplys~ HS. } }
{ (* case loop end *)
xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
{ intros r. hpull ;=> C L E. rew_bool_eq in *. subst L. hsimpl C. }
{ unfolds hinv. clear hinv K. intro C. xpull. intros I. lets: inv_length_C I.
xapp*. hsimpl. apply affine_Stack.
{ intros r. hpull ;=> C L E. 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. }
{ unfolds hinv. clear hinv K.
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 *)
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*. }
Admitted.
\ No newline at end of file
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