Commit 6bf0cf9c authored by Björn Brandenburg's avatar Björn Brandenburg

tweak proofs to be less "bulky" and less brittle

parent 8f809b9d
Pipeline #22027 failed with stages
in 3 minutes and 56 seconds
......@@ -113,10 +113,7 @@ Section WCCorrectnessFacts.
Proof.
move=> i sched_swap.
rewrite /find_swap_candidate.
destruct (search_arg sched_swap (relevant_pstate i)
(fun _ : processor_state Job => xpred0)
i (max_deadline_for_jobs_arrived_before arr_seq i))
as [n|] eqn:search_result; last by done.
destruct (search_arg _ _ _ ) as [n|] eqn:search_result; last by done.
apply search_arg_in_range in search_result.
by move:search_result => /andP [LEQ LMAX].
Qed.
......@@ -129,6 +126,7 @@ Section WCCorrectnessFacts.
Lemma wc_transform_prefix_inclusion:
forall t,
t < h1 -> sched1 t = sched2 t.
Proof.
move=> t before_horizon.
rewrite /sched1 /sched2.
induction h2; first by move: (ltn_leq_trans before_horizon H_horizon_order).
......@@ -136,8 +134,8 @@ Section WCCorrectnessFacts.
move: LT. rewrite ltnS => H_horizon_order_lt.
rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.
rewrite {1}/make_wc_at.
destruct (prefix_map sched (make_wc_at arr_seq) i i) as [j|] eqn:SCHED; first by done.
rewrite -(swap_before_invariant _ i (find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i));
destruct (prefix_map sched _ _ _) as [j|] eqn:SCHED; first by done.
rewrite -(swap_before_invariant _ i _);
last by apply ltn_leq_trans with (n := h1).
rewrite //.
by apply swap_candidate_is_in_future.
......
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