Commit 895fadef authored by Armaël Guéneau's avatar Armaël Guéneau

StackDFS_proof: prove subgoals related to index

parent 6d4b2a2d
......@@ -142,19 +142,11 @@ Proof.
{ intros k Hk Ck. rew_array* in Ck. case_if~. subst k.
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. (* à 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. *)
applys~ reachable_trans_edge i. }
{ intros i' j' Ci' E. rew_array*. case_if~. tests~: (i' = j).
forwards~ [H|[H|H]]: inv_true_edges0 i' j'.
- rew_array*. case_if~.
- rew_set in H. branches; auto_tilde. subst j'.
(* 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. *)
rew_array*. case_if~. }
- rew_array* in Ci'. case_if~.
- rew_set in H. branches; auto_tilde. }
Qed.
Lemma inv_step_skip : forall G n a C L j js,
......@@ -247,11 +239,9 @@ Proof.
{ 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.
(* toute la ligne: utiliser [rew_array] étendu avec [case_if] *) }
xapps*. xif.
{ xapps*. xapp. intros _. unfold hinv. hsimpl.
{ rew_array*. case_if~. }
applys~ inv_step_push i. }
{ (* mieux: [unfold hinv. xrets~. applys~ inv_step_skip j.] *)
xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } }
......@@ -272,4 +262,4 @@ Proof.
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
Qed.
\ 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