StackDFS: some cleanup

examples/DFS/StackDFS_proof.v

@@ -117,14 +117,14 @@ Proof.
          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 ->.
+  { introv Gi H.
+    assert (i = a) as ->.
     { 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*. }
+    applys~ reachable_self. }
   { introv Ci E. assert (i = a) as ->.
     { subst C. rew_array* in Ci. case_if~. }
-    left*. }
+    autos. }
 Qed.
 
 Lemma inv_step_push : forall G n a C L i j js,
@@ -137,16 +137,14 @@ Proof.
   { rew_array~. }
   { 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~.
+    - splits*. rew_array*. case_if~.
     - forwards~ (?&?): inv_stack0 i'. rew_array*. case_if~. }
   { 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 *)
-    applys~ reachable_trans_edge i. }
+    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* in Ci'. case_if~.
-    - rew_set in H. branches; auto_tilde. }
+    - rew_set in H. branches; autos. }
 Qed.
 
 Lemma inv_step_skip : forall G n a C L j js,
@@ -169,10 +167,7 @@ Proof.
   { destruct H as [p P]. lets PC: inv_source I. gen P PC.
    generalize a as i. intros i P. induction P.
      { auto. }
-     { introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H.
-       { inverts M. } (* [rew_list in *; auto_false]  devrait prouver les 3 buts *)
-       { auto. }
-       { inverts M. } } }
+     { introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H; rew_listx~ in M. } }
   { applys* inv_true_reachable. }
 Qed.
 
@@ -181,21 +176,14 @@ 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 ? ?. (* nommer les hypothèses c'est mieux *)
+  { intros i' j Ci' E.
     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]. *) }
+    rew_listx in M. branches; autos*. }
 Qed.
 
-
 Lemma reachable_imperative_spec : forall g G a b,
   a \in nodes G ->
   b \in nodes G ->
@@ -236,15 +224,14 @@ Proof.
            c ~> Array C2 \* s ~> Stack L2 \*
            \[ 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 *)
+       { introv N Hij. xpull. intros C2 L2 C2i.
          xapp_spec Sf.
          unfold hinv at 1. xpull. intros I'.
          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. } }
+         { unfold hinv. xrets~. applys~ inv_step_skip j. } }
        { unfold hinv. hsimpl. apply~ inv_step_pop. }
        { rew_bool_eq~. }
        { hsimpl. }