Commit 6d4b2a2d authored by Armaël Guéneau's avatar Armaël Guéneau

DFS_proof: actually prove index sidegoals

parent deeb1d12
This diff is collapsed.
......@@ -74,7 +74,9 @@ End Stack_proof.
- [E] describes a set of vertices: the neighbors of the currently processed vertex *)
Record inv (G:graph) (n:int) (a:int) (C:list bool) (L:list int) (E:set int) := {
inv_nodes_index : nodes_index G n;
inv_length_C : length C = n;
inv_source_node : a \in nodes G;
inv_source : C[a] = true;
inv_stack : forall i, mem i L -> i \in nodes G /\ C[i] = true;
inv_true_reachable : forall i, i \in nodes G ->
......@@ -83,8 +85,16 @@ Record inv (G:graph) (n:int) (a:int) (C:list bool) (L:list int) (E:set int) := {
C[i] = true -> has_edge G i j ->
mem i L \/ C[j] = true \/ j \in E }.
Lemma inv_index : forall G n a C L E i,
i \in nodes G ->
inv G n a C L E ->
index C i.
Proof. introv Hi I. destruct* I. Qed.
Hint Resolve inv_index.
Lemma inv_init : forall G n a C,
index a n ->
nodes_index G n ->
C = LibListZ.make n false ->
a \in nodes G ->
inv G n a (C[a:=true]) (a :: nil) \{}.
......@@ -92,12 +102,11 @@ 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. (* should be auto *) }
{ rew_array. case_if~. subst C. apply~ index_make. }
introv Gn EC Ga. constructors~.
{ subst C. rew_array*. destruct* Gn. (* should be auto *) }
{ rew_array*. case_if~. }
{ 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
......@@ -109,12 +118,12 @@ Proof.
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~. }
{ subst C. rew_array* in Ci. case_if~. }
left*. }
Qed.
......@@ -124,14 +133,13 @@ Lemma inv_step_push : forall G n a C L i j js,
has_edge G i j ->
inv G n a (C[j:=true]) (j :: L) js.
Proof.
introv I Ci M. inverts I. constructors.
introv I Ci M. lets I': I. inverts I. constructors~.
{ rew_array~. }
{ rew_array~. case_if~. }
{ 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. (* toute la ligne devrait etre auto *) }
{ intros k Hk Ck. rew_array~ in Ck. case_if~. subst k.
- splits. now applys~ (>> has_edge_nodes i j). 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 *)
skip. (* use rtclosure from LibRelation *) }
......@@ -141,12 +149,12 @@ Proof.
(à 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_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. *)
rewrite~ read_update_same. (* celui là c'est rew_array qui doit le gérer *) }
rew_array*. case_if~. }
Qed.
Lemma inv_step_skip : forall G n a C L j js,
......
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