Skip to content

Commit f279216

Browse files
hackedyhackedy
committed
Merge branch 'master' of github.com:DistributedComponents/verdi-aggregation
2 parents 1543e74 + b9d2d05 commit f279216

File tree

1 file changed

+58
-78
lines changed

1 file changed

+58
-78
lines changed

‎systems/TreeDynamicCorrect.v

Lines changed: 58 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -1092,25 +1092,22 @@ Proof.
10921092
auto with datatypes.
10931093
}
10941094
eapply IHrefl_trans_1n_trace1 with (d:=d) in H_in; eauto.
1095-
break_or_hyp.
1096-
-- exfalso.
1097-
match goal with
1098-
| [ H : refl_trans_1n_trace _ _ (?failed, net0) ?tr |- _ ] =>
1099-
assert (H_step: step_ordered_dynamic_failure_star
1100-
step_ordered_dynamic_failure_init
1101-
(failed, net0) tr)
1102-
by auto;
1103-
pose proof (Tree_in_after_all_fail_level H_step n) as H_after; simpl in H_after
1104-
end.
1105-
assert (before_all (Level lvo') Fail (odnwPackets net0 n' n)) by eauto.
1106-
find_rewrite.
1107-
simpl in *;
1108-
break_or_hyp;
1109-
break_and;
1110-
by auto.
1111-
-- find_rewrite.
1112-
right.
1113-
eapply In_cons_neq; congruence||eauto.
1095+
break_or_hyp; last by find_rewrite; simpl in *; break_or_hyp; last by right.
1096+
exfalso.
1097+
match goal with
1098+
| [ H : refl_trans_1n_trace _ _ (?failed, net0) ?tr |- _ ] =>
1099+
assert (H_step: step_ordered_dynamic_failure_star
1100+
step_ordered_dynamic_failure_init
1101+
(failed, net0) tr)
1102+
by auto;
1103+
pose proof (Tree_in_after_all_fail_level H_step n) as H_after; simpl in H_after
1104+
end.
1105+
assert (before_all (Level lvo') Fail (odnwPackets net0 n' n)) by eauto.
1106+
find_rewrite.
1107+
simpl in *;
1108+
break_or_hyp;
1109+
break_and;
1110+
by auto.
11141111
* match goal with
11151112
| [H : In (Level lvo') (odnwPackets _ n' n) |- _ ] =>
11161113
eapply IHrefl_trans_1n_trace1 with (d:=d) in H; auto
@@ -1159,33 +1156,28 @@ Proof.
11591156
by auto.
11601157
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
11611158
subst; rewrite_update2; rewrite_update; eauto.
1162-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1159+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
11631160
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
1164-
break_or_hyp.
1165-
-- left. by find_inversion.
1166-
-- find_rewrite.
1167-
right.
1168-
eapply In_cons_neq; eauto || congruence.
1169-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1161+
break_or_hyp; [left|]; first by find_inversion.
1162+
find_rewrite.
1163+
simpl in *.
1164+
by break_or_hyp; last by right.
1165+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
11701166
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
11711167
break_or_hyp.
11721168
-- left. by find_inversion.
11731169
-- find_rewrite.
11741170
right.
1175-
eauto using In_cons_neq.
1171+
by eauto using In_cons_neq.
11761172
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
11771173
subst; rewrite_update2; rewrite_update; try find_injection; eauto.
1178-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1174+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
11791175
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
1180-
break_or_hyp.
1181-
-- repeat find_rewrite.
1182-
auto.
1183-
-- find_rewrite.
1184-
right.
1185-
eauto ||
1186-
eapply In_cons_neq;
1187-
eauto || congruence.
1188-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1176+
break_or_hyp; [left|]; first by repeat find_rewrite.
1177+
find_rewrite.
1178+
simpl in *.
1179+
by break_or_hyp; last by right.
1180+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
11891181
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
11901182
break_or_hyp.
11911183
-- repeat find_rewrite.
@@ -1197,17 +1189,13 @@ Proof.
11971189
eauto || congruence.
11981190
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
11991191
subst; rewrite_update2; rewrite_update; try find_injection; eauto.
1200-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1192+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12011193
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
1202-
break_or_hyp.
1203-
-- repeat find_rewrite.
1204-
auto.
1205-
-- find_rewrite.
1206-
right.
1207-
eauto ||
1208-
eapply In_cons_neq;
1209-
eauto || congruence.
1210-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1194+
break_or_hyp; [left|]; first by repeat find_rewrite.
1195+
find_rewrite.
1196+
simpl in *.
1197+
by break_or_hyp; last by right.
1198+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12111199
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
12121200
break_or_hyp.
12131201
-- repeat find_rewrite.
@@ -1219,17 +1207,13 @@ Proof.
12191207
eauto || congruence.
12201208
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
12211209
subst; rewrite_update2; rewrite_update; try find_injection; eauto.
1222-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1210+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12231211
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
1224-
break_or_hyp.
1225-
-- repeat find_rewrite.
1226-
auto.
1227-
-- find_rewrite.
1228-
right.
1229-
eauto ||
1230-
eapply In_cons_neq;
1231-
eauto || congruence.
1232-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1212+
break_or_hyp; [left|]; first by repeat find_rewrite.
1213+
find_rewrite.
1214+
simpl in *.
1215+
by break_or_hyp; last by right.
1216+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12331217
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
12341218
break_or_hyp.
12351219
-- repeat find_rewrite.
@@ -1241,17 +1225,13 @@ Proof.
12411225
eauto || congruence.
12421226
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
12431227
subst; rewrite_update2; rewrite_update; try find_injection; eauto.
1244-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1228+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12451229
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
1246-
break_or_hyp.
1247-
-- repeat find_rewrite.
1248-
auto.
1249-
-- find_rewrite.
1250-
right.
1251-
eauto ||
1252-
eapply In_cons_neq;
1253-
eauto || congruence.
1254-
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n))
1230+
break_or_hyp; [left|]; first by repeat find_rewrite.
1231+
find_rewrite.
1232+
simpl in *.
1233+
by break_or_hyp; last by right.
1234+
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)).
12551235
by (eapply IHrefl_trans_1n_trace1; eauto; repeat find_rewrite; eauto with datatypes).
12561236
break_or_hyp.
12571237
-- repeat find_rewrite.
@@ -1284,11 +1264,11 @@ Proof.
12841264
auto with datatypes.
12851265
}
12861266
repeat find_rewrite.
1287-
auto with set.
1267+
by auto with set.
12881268
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)) by eauto.
12891269
break_or_hyp; [left|by auto].
12901270
find_rewrite.
1291-
auto with set.
1271+
by auto with set.
12921272
* move {H1}.
12931273
case (name_eq_dec from n) => H_dec.
12941274
subst_max.
@@ -1316,11 +1296,11 @@ Proof.
13161296
}
13171297
break_or_hyp;
13181298
repeat find_rewrite;
1319-
auto with set.
1299+
by auto with set.
13201300
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)) by eauto.
13211301
break_or_hyp;
13221302
repeat find_rewrite;
1323-
auto with set.
1303+
by auto with set.
13241304
+ destruct (name_eq_dec from n'), (name_eq_dec to n);
13251305
subst; rewrite_update2; rewrite_update; try find_injection; eauto.
13261306
* assert (n' <> n).
@@ -1344,17 +1324,17 @@ Proof.
13441324
find_rewrite.
13451325
auto with datatypes.
13461326
}
1347-
break_or_hyp;
1348-
repeat find_rewrite;
1349-
auto with set.
1327+
break_or_hyp; [left|]; first by repeat find_rewrite; auto with set.
1328+
repeat find_rewrite.
1329+
by left; auto with set.
13501330
* assert (NSet.In n' (adjacent d) \/ In New (odnwPackets net0 n' n)) by eauto.
1351-
break_or_hyp;
1352-
find_rewrite;
1353-
auto with set.
1331+
break_or_hyp; [left|by auto].
1332+
find_rewrite.
1333+
by auto with set.
13541334
* move {H1}.
13551335
case (name_eq_dec from n) => H_dec.
13561336
subst_max.
1357-
case (name_eq_dec to n') => H_dec.
1337+
case (name_eq_dec to n') => H_dec'.
13581338
subst_max.
13591339
rewrite_update2.
13601340
have H_in: In New (odnwPackets net0 n n') by find_rewrite; left.

0 commit comments

Comments
 (0)