diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 4e93c38dce0d291d0c76e8097f1f666c64e45588..78c5f22b04d2d9a206efe8fb0ddf94aa72d3dc2f 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -20,7 +20,7 @@ Section Abstract_RTA.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ Context {jc : JobCost Job}.
(** Consider _any_ kind of processor state model. *)
Context {PState : ProcessorState Job}.
@@ -412,7 +412,7 @@ Section Abstract_RTA.
rewrite -H_equivalent; [ | apply relative_rtc_time_is_bounded].
eapply H_job_interference_is_bounded_IBFP with t2; try done.
+ by rewrite -ltnNge (leqRW NC).
- + intros ? ? BUSY.
+ + intros t0 t3 BUSY.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t0 t3; clear BUSY.
by rewrite -job_arrival_eq_t1_plus_A.
@@ -431,7 +431,7 @@ Section Abstract_RTA.
erewrite leq_trans; [ | | apply H_Asp_R_fixpoint]; auto.
apply leq_add; [by rewrite -TSK; apply H_valid_job_cost | ].
eapply H_job_interference_is_bounded_IBFNP with (t2 := t2); eauto 2.
- intros ? ? BUSY.
+ intros t0 t3 BUSY.
edestruct busy_interval_is_unique; [exact H_busy_interval | exact BUSY| ].
subst t0 t3; clear BUSY; split.
- by rewrite H_equivalent //; apply relative_rtc_time_is_bounded.
@@ -464,7 +464,7 @@ Section Abstract_RTA.
task_response_time_bound arr_seq sched tsk R.
Proof.
move => j ARR JOBtsk; unfold job_response_time_bound.
- move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
+ move: (posnP (@job_cost _ jc j)) => [ZERO|POS].
{ by rewrite /completed_by ZERO. }
move: (H_bounded_busy_interval_exists _ ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].
move: (relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY) => AltL.
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index f997aa313863feaeccbff0dd9d1055cf5f05d57a..144242e77de9a97e6bcc408efcc0b1adaa422c9d 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -133,7 +133,7 @@ Section AbstractRTADefinitions.
busy_interval j t1' t2' ->
t1 = t1' /\ t2 = t2'.
Proof.
- intros ? ? ? ? ? BUSY BUSY'.
+ move=> j t1 t2 t1' t2' BUSY BUSY'.
have EQ: t1 = t1'.
{ apply/eqP.
apply/negPn/negP; intros CONTR.
diff --git a/analysis/abstract/ideal/abstract_seq_rta.v b/analysis/abstract/ideal/abstract_seq_rta.v
index 32c5cab6bc1816daf31d4b2c63eadd8545bc7855..536847624da3a6712d7953f8f6eba23fe3c139d8 100644
--- a/analysis/abstract/ideal/abstract_seq_rta.v
+++ b/analysis/abstract/ideal/abstract_seq_rta.v
@@ -26,7 +26,7 @@ Section Sequential_Abstract_RTA.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ Context {jc : JobCost Job}.
Context `{JobPreemptable Job}.
(** Consider any valid arrival sequence with consistent, non-duplicate arrivals...*)
@@ -272,7 +272,7 @@ Section Sequential_Abstract_RTA.
completed_by sched j2 t1.
Proof.
move => JA; move: (H_j2_from_tsk) => /eqP TSK2eq.
- move: (posnP (@job_cost _ H3 j2)) => [ZERO|POS].
+ move: (posnP (@job_cost _ jc j2)) => [ZERO|POS].
{ by rewrite /completed_by /service.completed_by ZERO. }
move: (H_interference_and_workload_consistent_with_sequential_tasks
j1 t1 t2 H_j1_arrives H_j1_from_tsk H_j1_cost_positive H_busy_interval) => SWEQ.
@@ -745,7 +745,7 @@ Section Sequential_Abstract_RTA.
apply ideal_proc_model_provides_unit_service.
{ clear ARR TSK H_R_is_maximum_seq R j.
move => t1 t2 R j ARR TSK BUSY NEQ COMPL.
- move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
+ move: (posnP (@job_cost _ jc j)) => [ZERO|POS].
{ exfalso; move: COMPL => /negP COMPL; apply: COMPL.
by rewrite /service.completed_by /completed_by ZERO.
}
diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index fa3de90402a6501786750af5ea57109851374f91..9e712dd92bb2b8b29a4d687504e57493bc01494b 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -20,7 +20,7 @@ Section JLFPInstantiation.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
- Context `{TaskCost Task}.
+ Context {tc : TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
@@ -572,7 +572,8 @@ Section JLFPInstantiation.
move=> j t1 R upp ARRin TSK ARR NCOMPL; rewrite /cumul_task_interference.
rewrite -big_split //= big_seq_cond [in X in _ = X]big_seq_cond; apply eq_bigr; move => t /andP [IN _].
have BinFact: forall (a b c : bool), (a -> (~~ b && c) || (b && ~~c)) -> (b \/ c -> a) -> nat_of_bool a = nat_of_bool b + nat_of_bool c.
- { by clear; move => [] [] []; try compute; firstorder; inversion H; inversion H0. }
+ { by clear; move=> [] [] [] //=; do ?[by move=> /(_ erefl)]; move=> _;
+ do ?[by move=> /(_ (or_introl erefl))]; move=> /(_ (or_intror erefl)). }
apply: BinFact;
[move=> /task_interference_received_before_P [TNSCHED [jo [INT TIN]]]
| move=> [/priority_inversion_P PRIO | /another_task_hep_job_interference_P [jo [INjo [ATHEP RSERV]]]]].
@@ -638,7 +639,7 @@ Section JLFPInstantiation.
}
{ unfold other_hep_jobs_interfering_workload, workload_of_jobs.
interval_to_duration t1 t2 k.
- induction k.
+ elim: k => [|k IHk].
- rewrite !addn0.
rewrite big_geq; last by done.
rewrite /arrivals_between /arrival_sequence.arrivals_between big_geq; last by done.
@@ -681,7 +682,7 @@ Section JLFPInstantiation.
move=> Phep; clear H_job_of_tsk.
rewrite [RHS]exchange_big /=; apply: eq_big_nat => x /andP[t1lex xltt].
rewrite /another_hep_job_interference_dec.
- ideal_proc_model_sched_case_analysis_eq sched x jo => [|{EqSched_jo}].
+ have [Idle|[jo Sched_jo]] := ideal_proc_model_sched_case_analysis sched x.
{ rewrite (@eq_has _ _ pred0) ?has_pred0 ?big1 // => [j' _ | j'].
+ exact: ideal_not_idle_implies_sched.
+ rewrite /receives_service_at ideal_not_idle_implies_sched //.
@@ -945,7 +946,7 @@ Section JLFPInstantiation.
move => /negP HYP; move : HYP.
rewrite negb_or /another_hep_job_interference.
move => /andP [HYP1 HYP2].
- ideal_proc_model_sched_case_analysis_eq sched t jo.
+ have [Idle|[jo Sched_jo]] := ideal_proc_model_sched_case_analysis sched t.
{ exfalso; clear HYP1 HYP2.
eapply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in H_busy_interval_prefix; rt_eauto.
by eapply not_quiet_implies_not_idle; rt_eauto.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index ae74e993f8c9c0ff62efbc066fcf6e6ad4eab719..39d0eec6b8b9377d62a5bd4f882c07820a1691d2 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -86,7 +86,7 @@ Section AbstractRTAReduction.
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp.
Proof.
- induction A as [|n].
+ induction A as [|n IHn].
- exists 0; repeat split.
by rewrite /is_in_search_space; left.
- have ALT:
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index 507c6cbb4022d1d766f5e5803d91729a1022d903..3ce9511a73e08ad949a32f602dab5396981aea28 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -304,7 +304,7 @@ Section ExistsBusyIntervalJLFP.
{ rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
leq_sum // => t' /andP [/andP [LT GT] _].
rewrite sum_nat_gt0 filter_predT; apply/hasP.
- ideal_proc_model_sched_case_analysis_eq sched t' jo.
+ have [Idle|[jo Sched_jo]] := ideal_proc_model_sched_case_analysis sched t'.
{ exfalso; move: LT; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
{ subst t'.
feed (H_no_quiet_time t1.+1); first by apply/andP; split.
@@ -318,9 +318,9 @@ Section ExistsBusyIntervalJLFP.
- by move: NCOMP; apply contra, completion_monotonic. }
apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
feed (H_work_conserving _ t' ARR').
- { by apply/andP; split; last rewrite scheduled_at_def EqIdle. }
+ { by apply/andP; split; last rewrite scheduled_at_def (eqP Idle). }
move: H_work_conserving => [j_other SCHEDother].
- by rewrite scheduled_at_def EqIdle in SCHEDother. } }
+ by rewrite scheduled_at_def (eqP Idle) in SCHEDother. } }
{ exists jo.
- apply arrived_between_implies_in_arrivals; try done.
apply H_jobs_come_from_arrival_sequence with t'; try done.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index b9b6da6a8737b576bf0cf0bad17eb11657f30d13..caa30aa76179c44eb01615db4a3e3364f7383a19 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -78,7 +78,7 @@ Section ExistsNoCarryIn.
is_idle sched t ->
no_carry_in t.
Proof.
- intros ? IDLE j ARR HA.
+ move=> t IDLE j ARR HA.
apply/negPn/negP; intros NCOMP.
have PEND : job_pending_at j t.
{ apply/andP; split.
@@ -102,7 +102,7 @@ Section ExistsNoCarryIn.
is_idle sched t ->
no_carry_in t.+1.
Proof.
- intros ? IDLE j ARR HA.
+ move=> t IDLE j ARR HA.
apply/negPn/negP; intros NCOMP.
have PEND : job_pending_at j t.
{ apply/andP; split.
@@ -208,7 +208,7 @@ Section ExistsNoCarryIn.
intros s ARR BEF.
by apply idle_instant_implies_no_carry_in_at_t.
Qed.
-
+
(** In the second case, the total service within the time
interval <<[t, t + Δ)>> is equal to [Δ]. On the other hand,
we know that the total workload is lower-bounded by the
@@ -257,7 +257,7 @@ Section ExistsNoCarryIn.
Lemma processor_is_not_too_busy :
forall t, exists δ, δ < Δ /\ no_carry_in (t + δ).
Proof.
- induction t.
+ elim=> [|t IHt].
{ by exists 0; split; [ | rewrite addn0; apply no_carry_in_at_the_beginning]. }
{ move: IHt => [δ [LE FQT]].
move: (posnP δ) => [Z|POS]; last first.
@@ -272,7 +272,7 @@ Section ExistsNoCarryIn.
- by apply low_total_service_implies_existence_of_time_with_no_carry_in.
}
Qed.
-
+
End ProcessorIsNotTooBusy.
(** Consider an arbitrary job [j] with positive cost. *)
diff --git a/analysis/facts/busy_interval/ideal/priority_inversion_bounded.v b/analysis/facts/busy_interval/ideal/priority_inversion_bounded.v
index 1995ea9b28614eadcb03be552ba540aa373ebe5a..0c5fa064b407dfccb8b8a66b029b6608a8d12ee8 100644
--- a/analysis/facts/busy_interval/ideal/priority_inversion_bounded.v
+++ b/analysis/facts/busy_interval/ideal/priority_inversion_bounded.v
@@ -113,7 +113,7 @@ Section PriorityInversionIsBounded.
scheduled_at sched j_hp t.
Proof.
move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
- ideal_proc_model_sched_case_analysis_eq sched t jhp.
+ have [Idle|[jhp Sched_jhp]] := ideal_proc_model_sched_case_analysis sched t.
{ by eapply instant_t_is_not_idle in Idle; rt_eauto;
[ | apply/andP; split; first apply leq_trans with tp]. }
exists jhp.
@@ -407,10 +407,10 @@ Section PriorityInversionIsBounded.
Proof.
rewrite /preemption_time.
move: (H_valid_model_with_bounded_nonpreemptive_segments) => CORR.
- ideal_proc_model_sched_case_analysis_eq sched (t1 + fpt) s'; try done.
- clear EqSched_s'; move: (Sched_s'); rewrite scheduled_at_def;
- move => /eqP EqSched_s'; rewrite EqSched_s'.
- destruct (jlp == s') eqn: EQ.
+ have [Idle|[s' Sched_s']] := ideal_proc_model_sched_case_analysis sched (t1 + fpt).
+ { by rewrite (eqP Idle). }
+ move: (Sched_s'); rewrite scheduled_at_def => /eqP EqSched_s'.
+ rewrite EqSched_s'; destruct (jlp == s') eqn: EQ.
- move: EQ => /eqP EQ; subst s'.
rewrite /service -(service_during_cat _ _ _ t1); last first.
{ by apply/andP; split; last rewrite leq_addr. }
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 341ec973c4058c7878e428953776bb476e27301e..4a3c53e4aefd684686a610cfb892becc776633ee 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -43,7 +43,7 @@ Section PIGenericProcessorModelLemma.
cumulative_priority_inversion arr_seq sched j t1 t_mid
+ cumulative_priority_inversion arr_seq sched j t_mid t2.
Proof.
- intros * LE1 LE2.
+ intros t_mid t1 t2 LE1 LE2.
rewrite /cumulative_priority_inversion -big_cat //=.
replace (index_iota t1 t_mid ++ index_iota t_mid t2) with (index_iota t1 t2); first by reflexivity.
interval_to_duration t1 t_mid δ1.
diff --git a/analysis/facts/hyperperiod.v b/analysis/facts/hyperperiod.v
index 982bf1bf2a58733949f47fbb7f9a7e84b61615dd..bf267994c22d345ff4794b04bbf097d41b27e0c8 100644
--- a/analysis/facts/hyperperiod.v
+++ b/analysis/facts/hyperperiod.v
@@ -95,7 +95,7 @@ Section PeriodicLemmas.
(starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
Proof.
clear H_task_in_ts H_valid_period.
- intros *.
+ move=> j1 j2.
set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
(starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
@@ -132,7 +132,7 @@ Section PeriodicLemmas.
size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
Proof.
- intros * N1_LT.
+ move=> n1 n2 N1_LT.
have -> : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP.
{ by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
@@ -152,7 +152,7 @@ Section PeriodicLemmas.
size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
Proof.
- intros *.
+ move=> n1 n2.
case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite EQ.
move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
+ by apply eq_size_hyp_lt => //; lia.
diff --git a/analysis/facts/model/ideal/schedule.v b/analysis/facts/model/ideal/schedule.v
index d60015e25e7b5b8778436f0a2e864e197bfe886e..abbdc880d7ed4681853c413de01719affa5e169b 100644
--- a/analysis/facts/model/ideal/schedule.v
+++ b/analysis/facts/model/ideal/schedule.v
@@ -114,8 +114,8 @@ Section ScheduleClass.
forall (sched : schedule (ideal.processor_state Job)) (t : instant),
is_idle sched t \/ exists j, scheduled_at sched j t.
Proof.
- intros.
- unfold is_idle; simpl; destruct (sched t) eqn:EQ.
+ move=> sched t.
+ unfold is_idle; simpl; destruct (sched t) as [s|] eqn:EQ.
- by right; exists s; auto; rewrite scheduled_at_def EQ.
- by left; auto.
Qed.
@@ -223,7 +223,7 @@ Section IncrementalService.
Proof.
move=> j t1 t2 k SERV.
have LE: t1 < t2 by move: (service_during_ge _ _ _ _ SERV).
- induction k; first by apply positive_service_during in SERV.
+ elim: k SERV => [|k IHk] SERV; first by apply positive_service_during in SERV.
feed IHk; first by apply ltn_trans with k.+1.
move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
have SERVk1: service_during sched j t1 t.+1 = k.+1.
diff --git a/analysis/facts/model/ideal/service_of_jobs.v b/analysis/facts/model/ideal/service_of_jobs.v
index 093ec21f3223f9a7e2cd52c00410db1db94e5420..09954fe1678ada83baa8ee8ac4207f2ed494ab6f 100644
--- a/analysis/facts/model/ideal/service_of_jobs.v
+++ b/analysis/facts/model/ideal/service_of_jobs.v
@@ -52,7 +52,7 @@ Section IdealModelLemmas.
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t, t1 <= t < t2 /\ is_idle sched t.
Proof.
- intros ? ? SERV.
+ move=> t1 t2 SERV.
destruct (t1 <= t2) eqn:LE; last first.
{ move: LE => /negP/negP; rewrite -ltnNge.
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.
@@ -68,7 +68,7 @@ Section IdealModelLemmas.
exists x; split; first by apply/andP; split.
apply/negPn; apply/negP; intros NIDLE.
unfold is_idle in NIDLE.
- destruct(sched x) eqn:SCHED; last by done.
+ destruct(sched x) as [s|] eqn:SCHED; last by done.
move: SCHED => /eqP SCHED; clear NIDLE; rewrite -scheduled_at_def/= in SCHED.
move: L => /eqP; rewrite sum_nat_eq0_nat filter_predT; move => /allP L.
specialize (L s); feed L.
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
index 3d96f51ad7c02f557509b40d6373ae01160c60c7..810fac8787534ae8ccb97df07db6baa2c452efd6 100644
--- a/analysis/facts/model/preemption.v
+++ b/analysis/facts/model/preemption.v
@@ -99,7 +99,7 @@ Section PreemptionFacts.
move : (H_sched_valid) => [COME_ARR READY].
have MIN := ex_minnP EX.
move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
- destruct mpt.
+ destruct mpt as [|mpt].
- exists 0; repeat split.
+ by apply/andP; split => //; apply MATE.
+ eapply (zero_is_pt arr_seq); eauto 2.
@@ -114,7 +114,7 @@ Section PreemptionFacts.
move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].
- by subst t'.
- by apply ALL; rewrite mem_index_iota; apply/andP; split.
- }
+ }
have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2.
exists mpt.+1; repeat split; try done.
+ apply/andP; split; last by done.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 2d506768f027827a8f534d955b5be24c96435d30..edb636425de2ff531ea2656e3640075ea75d0c11 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -288,8 +288,7 @@ Section RequestBoundFunctions.
t > 0 ->
task_cost tsk <= total_request_bound_function ts t.
Proof.
- move => t GE.
- destruct t; first by done.
+ case=> [//|t] GE.
eapply leq_trans; first by apply task_rbf_1_ge_task_cost; rt_eauto.
rewrite /total_request_bound_function.
erewrite big_rem; last by exact H_tsk_in_ts.
diff --git a/analysis/facts/model/sequential.v b/analysis/facts/model/sequential.v
index c4a79f3a27279167677a296cc76db948a76d5786..dfccca87abb89d4095d64e68e2fd18b3d37b5768 100644
--- a/analysis/facts/model/sequential.v
+++ b/analysis/facts/model/sequential.v
@@ -35,7 +35,7 @@ Section ExecutionOrder.
scheduled_at sched j1 t ->
job_arrival j1 <= job_arrival j2.
Proof.
- intros ? ? t ARR1 ARR2 TSK NCOMPL SCHED.
+ move=> j1 j2 t ARR1 ARR2 TSK NCOMPL SCHED.
rewrite /same_task eq_sym in TSK.
have SEQ := H_sequential_tasks j2 j1 t ARR2 ARR1 TSK.
rewrite leqNgt; apply/negP; intros ARR.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 7e77616af04e0040977499620282505a6d037d2d..b1e40dc36c718e935aded5444b9af10b44e72cf8 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -18,7 +18,7 @@ Section GenericModelLemmas.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
+ Context {ja : JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
@@ -63,7 +63,7 @@ Section GenericModelLemmas.
move => x /andP [/andP [GEi LTi] _].
rewrite big_seq_cond big1 //.
move => j /andP [ARR Ps].
- apply service_before_job_arrival_zero with H0; auto.
+ apply service_before_job_arrival_zero with ja; auto.
eapply in_arrivals_implies_arrived_between in ARR; eauto 2.
by move: ARR => /andP [N1 N2]; apply leq_trans with t.
Qed.
@@ -177,7 +177,7 @@ Section GenericModelLemmas.
service_of_jobs_at sched P jobs t = 0.
Proof.
intros ? ALL.
- induction jobs.
+ elim: jobs ALL => [|a l IHl] ALL.
- by rewrite /service_of_jobs_at big_nil.
- feed IHl.
{ by intros j' IN; apply ALL; rewrite in_cons; apply/orP; right. }
@@ -190,7 +190,6 @@ Section GenericModelLemmas.
by apply not_scheduled_implies_no_service.
Qed.
-
End GenericModelLemmas.
(** In this section, we prove some properties about service
@@ -267,7 +266,7 @@ Section UnitServiceModelLemmas.
apply in_arrivals_implies_arrived_between in ARR; last by done.
move: ARR => /andP [T1 T2].
have F1: forall a b, (a < b) || (a >= b).
- { by intros; destruct (a < b) eqn:EQU; apply/orP;
+ { by move=> a b; destruct (a < b) eqn:EQU; apply/orP;
[by left |right]; apply negbT in EQU; rewrite leqNgt. }
move: (F1 t_compl t1) => /orP [LT | GT].
- rewrite /service_of_jobs /service_during in EQ.
@@ -384,9 +383,9 @@ Section UnitServiceUniProcessorModelLemmas.
intros t.
eapply leq_trans.
{ by apply leq_sum_seq_pred with (P2 := predT); intros. }
- simpl; induction jobs as [ | j js].
+ simpl; elim: jobs H_no_duplicate_jobs => [|j js IHjs] uniq_js.
- by rewrite big_nil.
- - feed IHjs; first by move: H_no_duplicate_jobs; rewrite cons_uniq => /andP [_ U].
+ - feed IHjs; first by move: uniq_js; rewrite cons_uniq => /andP [_ U].
rewrite big_cons.
destruct (service_is_zero_or_one H_unit_service_proc_model sched j t) as [Z | O].
+ by rewrite Z (leqRW IHjs).
@@ -399,16 +398,16 @@ Section UnitServiceUniProcessorModelLemmas.
first apply service_at_implies_scheduled_at.
apply/negP; intros SCHED.
specialize (H_uniprocessor_model _ _ _ _ POS SCHED); subst j'.
- by move: H_no_duplicate_jobs; rewrite cons_uniq => /andP [/negP NIN _].
+ by move: uniq_js; rewrite cons_uniq => /andP [/negP NIN _].
Qed.
-
+
(** Next, we prove that the service received by those jobs is no larger
than their workload. *)
Corollary service_of_jobs_le_length_of_interval:
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ.
Proof.
- intros.
+ move=> t Δ.
have EQ: \sum_(t <= x < t + Δ) 1 = Δ.
{ by rewrite big_const_nat iter_addn mul1n addn0 -{2}[t]addn0 subnDl subn0. }
rewrite -{2}EQ {EQ}.
@@ -423,7 +422,7 @@ Section UnitServiceUniProcessorModelLemmas.
forall (t1 t2 : instant),
service_of_jobs sched P jobs t1 t2 <= t2 - t1.
Proof.
- intros.
+ move=> t1 t2.
have <-: \sum_(t1 <= x < t2) 1 = t2 - t1.
{ by rewrite big_const_nat iter_addn mul1n addn0. }
rewrite /service_of_jobs exchange_big //=.
diff --git a/analysis/facts/model/task_arrivals.v b/analysis/facts/model/task_arrivals.v
index 98aaeca102d4d8550e9c91097cc537f7c9143a4e..f4b8249432f60e7883dac473ee7956e432911714 100644
--- a/analysis/facts/model/task_arrivals.v
+++ b/analysis/facts/model/task_arrivals.v
@@ -265,7 +265,7 @@ Section TaskArrivals.
t >= job_arrival j ->
nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.
Proof.
- intros * ARR TSK IND T_G.
+ move=> n j_def j t ARR TSK IND T_G.
rewrite -IND.
have EQ_IND : index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t).
{ have CAT : exists xs, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t.
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index d5ee84a5e22bea45f05d101b5935c9a352cd254a..77fb5ade22560df07c5377d4ed385b4e21396399 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -86,7 +86,7 @@ Section JobArrivalSeparation.
move: j1 j2 H_j1_of_task H_j2_of_task H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq;
clear H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq H_j1_of_task H_j2_of_task j1 j2.
move: k => s.
- induction s.
+ elim: s => [|s IHs].
{ intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso.
specialize (earlier_arrival_implies_lower_index arr_seq H_valid_arrival_sequence j1 j2) => LT_IND.
feed_n 4 LT_IND => //; first by rewrite TSKj2.
@@ -95,7 +95,7 @@ Section JobArrivalSeparation.
{ intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
specialize (exists_jobs_before_j
arr_seq H_valid_arrival_sequence j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
- destruct s.
+ destruct s as [|s].
- exists 1; repeat split.
by rewrite (consecutive_job_separation j1) //; lia.
- feed BEFORE; first by lia.
diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v
index df1274b7f474b345368695c0b4010cfc7dbc7bad..aad0ed97b57eb92abbcd5c88db2272e56707d6f8 100644
--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
@@ -34,7 +34,7 @@ Section PeriodicArrivalTimes.
job_index arr_seq j = n ->
job_arrival j = task_offset tsk + n * task_period tsk.
Proof.
- induction n.
+ elim=> [|n IHn].
{ intros j ARR TSK_IN ZINDEX.
rewrite mul0n addn0.
exact: first_job_arrival ZINDEX.
@@ -56,7 +56,7 @@ Section PeriodicArrivalTimes.
job_task j = tsk ->
exists n, job_arrival j = task_offset tsk + n * task_period tsk.
Proof.
- intros * ARR TSK.
+ move=> j ARR TSK.
exists (job_index arr_seq j).
specialize (periodic_arrival_times (job_index arr_seq j) j) => J_ARR.
by feed_n 3 J_ARR => //.
@@ -72,11 +72,11 @@ Section PeriodicArrivalTimes.
job_index arr_seq j = n.
Proof.
have F : task_period tsk > 0 by auto.
- induction n.
- + intros * ARR_J TSK ARR.
+ elim=> [|n IHn].
+ + move=> j ARR_J TSK ARR.
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] => //.
by apply periodic_arrival_times in SUCC => //; lia.
- + intros * ARR_J TSK ARR.
+ + move=> j ARR_J TSK ARR.
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model => //.
{ rewrite lt0n; apply /eqP; intro EQ.
apply (first_job_arrival _ H_valid_arrival_sequence tsk) in EQ => //.
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index ff36dfb1a609bde9844e2af69daff119ea6f719a..a3cd67b04df45cbb57551e4e031697dcfb04385f 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -33,10 +33,9 @@ Section TaskArrivalsSize.
(forall n, t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::].
Proof.
- intros * T.
+ move=> t T.
have EMPT_OR_EXISTS : forall xs, xs = [::] \/ exists a, a \in xs.
- { intros *.
- induction xs; first by left.
+ { move=> t0; elim=> [|a xs IHxs]; first by left.
right; exists a.
by apply mem_head.
}
@@ -115,7 +114,7 @@ Section TaskArrivalsSize.
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n.
Proof.
- intros *.
+ move=> n.
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
exists j; repeat split => //.
exact: (periodic_arrival_times arr_seq).
@@ -161,7 +160,7 @@ Section TaskArrivalsSize.
let r := (task_offset tsk + n.+1 * task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
Proof.
- induction n.
+ elim=> [|n IHn].
intros l r; rewrite /l mul0n add0n addn0.
by apply size_task_arrivals_up_to_offset.
intros l r.
diff --git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index 28fc8a4d3f94f74d5f7b00e6089c67fd79bbc831..3d6cf3c653636f08b3d4ee9ce88cbb2868791fa3 100644
--- a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -41,7 +41,7 @@ Section FullyNonPreemptiveModel.
Lemma valid_fully_nonpreemptive_model:
valid_preemption_model arr_seq sched.
Proof.
- intros j; split; [by apply/orP; left | split; [by apply/orP; right | split]].
+ move=> j _; split; [by apply/orP; left | split; [by apply/orP; right | split]].
- move => t; rewrite /job_preemptable /fully_nonpreemptive_job_model Bool.negb_orb -lt0n; move => /andP [POS NCOMPL].
move: (incremental_service_during _ _ _ _ _ POS) => [ft [/andP [_ LT] [SCHED SERV]]].
apply H_nonpreemptive_sched with ft.
@@ -75,7 +75,7 @@ Section FullyNonPreemptiveModel.
Lemma job_max_nps_is_job_cost:
forall j, job_max_nonpreemptive_segment j = job_cost j.
Proof.
- intros.
+ move=> j.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_job_model.
case: (posnP (job_cost j)) => [ZERO|POS].
@@ -84,9 +84,9 @@ Section FullyNonPreemptiveModel.
{ clear; simpl; intros.
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
have ->: forall xs P1 P2, (forall x, x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
- { clear; intros.
+ { clear; move=> t xs P1 P2 H.
apply eq_in_filter.
- intros ? IN. specialize (H _ IN).
+ move=> x IN. specialize (H _ IN).
by destruct (P1 x), (P2 x).
}
rewrite filter_pred1_uniq; first by done.
@@ -98,12 +98,12 @@ Section FullyNonPreemptiveModel.
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
by done.
Qed.
-
+
(** ... and [job_last_nonpreemptive_segment j] is equal to [job_cost j]. *)
Lemma job_last_nps_is_job_cost:
forall j, job_last_nonpreemptive_segment j = job_cost j.
Proof.
- intros.
+ move=> j.
rewrite /job_last_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_job_model.
case: (posnP (job_cost j)) => [ZERO|POS].
@@ -112,9 +112,9 @@ Section FullyNonPreemptiveModel.
{ clear; simpl; intros.
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
have ->: forall xs P1 P2, (forall x, x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
- { clear; intros.
+ { clear; move=> t xs P1 P2 H.
apply eq_in_filter.
- intros ? IN. specialize (H _ IN).
+ move=> x IN. specialize (H _ IN).
by destruct (P1 x), (P2 x).
}
rewrite filter_pred1_uniq; first by done.
@@ -126,7 +126,7 @@ Section FullyNonPreemptiveModel.
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
by done.
Qed.
-
+
End FullyNonPreemptiveModel.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_rt_facts.
@@ -170,4 +170,4 @@ Section NoPreemptionsEquivalence.
}
Qed.
-End NoPreemptionsEquivalence.
+End NoPreemptionsEquivalence.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 8e58895ae723030bf6520fe191cc07cd46ba93e7..cc72a00343a4ecce0eca4424f5d4f14d5d53d93e 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -39,10 +39,10 @@ Section FullyPreemptiveModel.
job_cost j = 0 ->
job_max_nonpreemptive_segment j = 0.
Proof.
- intros.
+ move=> j H1.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
- by rewrite H1; compute.
+ by rewrite H1.
Qed.
(** ... or ε when [job_cost j > 0]. *)
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 451319b8af79ea8ce4667e1dbe02a6bb5f4a3bad..1076ce9d035c357fcf0275e73df50de4461527f1 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -249,7 +249,7 @@ Section RunToCompletionThreshold.
~~ completed_by sched j t' ->
scheduled_at sched j t'.
Proof.
- intros ? ? LE TH COM.
+ move=> t t' LE TH COM.
apply H_valid_preemption_model; first by done.
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
- by apply leq_trans with (service sched j t); last apply service_monotonic.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 39edeba09d937633e38d48e55a8615087ac4e6af..88c966821178f4360b338959de9a93c79b321a84 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -65,7 +65,7 @@ Section TaskRTCThresholdLimitedPreemptions.
{ apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
move: (END _ H_tsk_in_ts) => EQ.
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
- by intros; move: (H_positive_cost); rewrite EQ ltnn.
+ by move=> EQ; move: (H_positive_cost); rewrite EQ ltnn.
}
have EQ: 2 = size [::0; task_cost tsk]; first by done.
rewrite EQ; clear EQ.
@@ -93,14 +93,14 @@ Section TaskRTCThresholdLimitedPreemptions.
by rewrite -(leq_add2r 1) !addn1 prednK //.
}
Qed.
-
+
(** Then, we prove that [task_rtct] function
defines a valid task's run to completion threshold. *)
Lemma limited_valid_task_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
- intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
+ intros j ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
rewrite /job_rtct /task_rtct /limited_preemptions_rtc_threshold
/job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
@@ -139,6 +139,6 @@ Section TaskRTCThresholdLimitedPreemptions.
- by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
- by apply SORT__task; rewrite TSK__j.
Qed.
-
+
End TaskRTCThresholdLimitedPreemptions.
Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 6b7ae3a73e7dc2d84ba308af36575fe8e3a9d99c..a7b08996281c4c27769f37dbb12b76fa5d70c0af 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -41,10 +41,10 @@ Section TaskRTCThresholdFullyNonPreemptive.
job_cost j = 0 ->
job_rtct j = 0.
Proof.
- intros.
+ move=> j cj0.
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
unfold job_rtct.
- by rewrite H3; compute.
+ by rewrite cj0; compute.
Qed.
(** ... and ε otherwise. *)
@@ -54,7 +54,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
arrives_in arr_seq j ->
job_rtct j = ε.
Proof.
- intros ? ARRj POSj; unfold ε in *.
+ move=> j ARRj POSj; unfold ε in *.
unfold job_rtct.
rewrite job_last_nps_is_job_cost.
by rewrite subKn.
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index b46a072cb117c5126d0dee5887d98f0de9f6ee76..61bc5f3d60b72190f40d7a71fa1c32144f817ba9 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -62,7 +62,7 @@ Section LiuAndLaylandReadiness.
Fact basic_readiness_is_work_bearing_readiness :
work_bearing_readiness arr_seq sched.
Proof.
- intros ? ? ARR PEND.
+ intros j ? ARR PEND.
exists j; repeat split => //.
by eapply (H_priority_is_reflexive 0).
Qed.
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index cccc48f08093490e033beac492937c93cc073999..f35d58f026c6e99f7c5b0bf70db24748b8922770 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -43,11 +43,11 @@ Section SequentialTasksReadiness.
Fact sequential_readiness_nonclairvoyance :
nonclairvoyant_readiness sequential_readiness.
Proof.
- intros sched1 sched2 ? ? ID ? LE; rewrite //=.
+ intros sched1 sched2 j h ID t LE; rewrite //=.
erewrite identical_prefix_pending; eauto 2.
destruct (boolP (pending sched2 j t)) as [_ | _] => //=.
destruct (boolP (prior_jobs_complete arr_seq sched2 j t)) as [ALL | NOT_ALL]; apply/eqP.
- - rewrite eqb_id; apply/allP; intros ? IN.
+ - rewrite eqb_id; apply/allP; intros x IN.
move: ALL => /allP ALL; specialize (ALL x IN).
by erewrite identical_prefix_completed_by; eauto 2.
- move: NOT_ALL => /allPn [x IN NCOMP].
@@ -81,7 +81,7 @@ Section SequentialTasksReadiness.
intros j.
have EX: exists k, job_arrival j <= k by (exists (job_arrival j)).
destruct EX as [k LE]; move: j LE.
- induction k; intros ? ? ? ARR PEND.
+ elim: k => [|k IHk] j LE t ARR PEND.
{ destruct (boolP (job_ready sched j t)) as [READY | NREADY].
{ by exists j; repeat split; eauto using (H_priority_is_reflexive 0). }
{ move: NREADY; rewrite //= PEND Bool.andb_true_l => /allPn [jhp IN NCOMP].
diff --git a/analysis/facts/sporadic/arrival_sequence.v b/analysis/facts/sporadic/arrival_sequence.v
index 4c1bd9a01370cb1cef4b0ea9d30b1c45dc0dd8b7..63f2c639467ba268366a9a5e149372924cd4c0c6 100644
--- a/analysis/facts/sporadic/arrival_sequence.v
+++ b/analysis/facts/sporadic/arrival_sequence.v
@@ -69,9 +69,8 @@ Section SporadicArrivals.
move: SIZE_CASE => [Z|[ONE|GTONE]].
- apply size0nil in Z.
by rewrite Z in J_IN_FILTER.
- - repeat (destruct seq; try by done).
- rewrite mem_seq1 in J_IN_FILTER; move : J_IN_FILTER => /eqP J1_S.
- by rewrite J1_S.
+ - case: seq ONE J_IN_FILTER => [//| s [|//]] J_ONE.
+ by rewrite mem_seq1 => /eqP ->.
- exfalso.
apply size_task_arrivals_at_leq_one.
exists j1.
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index 6d0bde3b7f0297f0c655e615457f762d09dad08d..9e7a7751b5de803534a3a9da3ee8a0c8b73f1b0d 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -44,11 +44,10 @@ Section TDMAFacts.
Proof.
rewrite /task_slot_offset /TDMA_cycle big_mkcond.
apply leq_ltn_trans with (n:=\sum_(prev_task <- ts )if prev_task!=task then task_time_slot prev_task else 0).
- - apply leq_sum. intros* T. case (slot_order i task);auto.
+ - apply leq_sum => i T. case (slot_order i task);auto.
- rewrite -big_mkcond (bigD1_seq task)?set_uniq//=.
- rewrite -subn_gt0 -addnBA. rewrite subnn addn0 //.
+ rewrite -subn_gt0 -addnBA // subnn addn0 //.
exact: time_slot_positive.
- easy.
Qed.
(** For a task, the sum of its slot offset and its time slot is
@@ -61,7 +60,7 @@ Section TDMAFacts.
rewrite big_mkcond.
replace (\sum_(i <- ts | i != task) task_time_slot i)
with (\sum_(i <- ts ) if i != task then task_time_slot i else 0).
- apply leq_sum. intros*T. case (slot_order i task);auto.
+ apply leq_sum => i T; case (slot_order i task);auto.
by rewrite -big_mkcond. apply (set_uniq ts).
Qed.
End TimeSlotFacts.
@@ -98,11 +97,11 @@ Section TDMAFacts.
task_slot_offset ts tsk2 >=
task_slot_offset ts tsk1 + task_time_slot tsk1 .
Proof.
- intros* IN1 IN2 ORDER NEQ.
+ move=> tsk1 tsk2 IN1 IN2 ORDER NEQ.
rewrite /task_slot_offset big_mkcond addnC/=.
replace (\sum_(tsk <- ts | slot_order tsk tsk2 && (tsk != tsk2)) task_time_slot tsk)
with (task_time_slot tsk1 + \sum_(tsk <- ts )if slot_order tsk tsk2 && (tsk != tsk1) && (tsk!=tsk2) then task_time_slot tsk else O).
- rewrite leq_add2l. apply leq_sum_seq. intros* IN T.
+ rewrite leq_add2l. apply leq_sum_seq => i IN T.
case (slot_order i tsk1)eqn:SI2;auto. case (i==tsk1)eqn:IT2;auto;simpl.
case (i==tsk2)eqn:IT1;simpl;auto.
- by move/eqP in IT1;rewrite IT1 in SI2;apply slot_order_antisymmetric in ORDER;auto;apply ORDER in SI2;move/eqP in NEQ.
@@ -111,7 +110,7 @@ Section TDMAFacts.
move/eqP /eqP in ORDER. move/eqP in NEQ. rewrite ORDER //=. apply /eqP.
have TS2: (tsk1 != tsk2) = true . apply /eqP;auto. rewrite TS2.
rewrite eqn_add2l. rewrite big_mkcond. apply/eqP. apply eq_bigr;auto.
- intros* T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
+ move=> i T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
Qed.
(** Then, we proved that no two tasks share the same time slot at any time. *)
@@ -123,7 +122,7 @@ Section TDMAFacts.
task_in_time_slot ts tsk2 t ->
tsk1 = tsk2.
Proof.
- intros * IN1 SLOT1 IN2 SLOT2.
+ intros tsk1 tsk2 t IN1 SLOT1 IN2 SLOT2.
rewrite /task_in_time_slot.
set cycle := TDMA_cycle ts.
set O1 := task_slot_offset ts tsk1.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index ee45e95f195f5035b4e866092eafddce1cb9f55c..0f45ac5e058319e36a77c4c63e9826beff48c538 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -689,7 +689,7 @@ Section EDFPrefixInclusion.
identical_prefix (edf_transform_prefix sched h1) (edf_transform_prefix sched h2) h1.
Proof.
move=> h1 h2 LE_h1_h2. rewrite /identical_prefix => t LT_t_h1.
- induction h2; first by move: (leq_trans LT_t_h1 LE_h1_h2).
+ elim: h2 LE_h1_h2 => [|h2 IHh2] LE_h1_h2; first by move: (leq_trans LT_t_h1 LE_h1_h2).
move: LE_h1_h2. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
move: LT. rewrite ltnS => LE_h1_h2.
rewrite [RHS]/edf_transform_prefix /prefix_map -/prefix_map IHh2 //.
diff --git a/analysis/facts/transform/edf_wc.v b/analysis/facts/transform/edf_wc.v
index 9976ec343efb177704da670c62ad3e6fc8dd2a6b..0e0f6286a7cdd8d16c325c3dc3c3033c7d760559 100644
--- a/analysis/facts/transform/edf_wc.v
+++ b/analysis/facts/transform/edf_wc.v
@@ -274,13 +274,14 @@ Section MakeEDFWorkConservationLemmas.
conservation. *)
Lemma mea_maintains_work_conservation :
work_conserving arr_seq sched -> work_conserving arr_seq sched'.
- Proof. rewrite /sched'/make_edf_at => WC_sched. destruct (sched t_edf) eqn:E => //.
- apply fsc_swap_maintains_work_conservation => //.
- - by rewrite scheduled_at_def; apply /eqP => //.
- - apply (scheduled_at_implies_later_deadline sched) => //.
- + rewrite /all_deadlines_met in (H_no_deadline_misses).
- now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
- + by rewrite scheduled_at_def; apply/eqP => //.
+ Proof.
+ rewrite /sched'/make_edf_at => WC_sched. destruct (sched t_edf) as [s|] eqn:E => //.
+ apply fsc_swap_maintains_work_conservation => //.
+ - by rewrite scheduled_at_def; apply /eqP => //.
+ - apply (scheduled_at_implies_later_deadline sched) => //.
+ + rewrite /all_deadlines_met in (H_no_deadline_misses).
+ now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
+ + by rewrite scheduled_at_def; apply/eqP => //.
Qed.
End MakeEDFWorkConservationLemmas.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index eaae5e785cf11f1f623b0c099d9f2746347dac6c..c5d7b93adf088bffda56ce681fd9c5c8089e7248 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -467,8 +467,9 @@ Section AuxiliaryLemmasWorkConservingTransformation.
Proof.
move=> t before_horizon.
rewrite /sched1 /sched2.
- induction h2; first by move: (leq_trans before_horizon H_horizon_order).
- move: H_horizon_order. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
+ elim: h2 H_horizon_order => [|i IHi] horizon_order.
+ by move: (leq_trans before_horizon horizon_order).
+ move: horizon_order. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
move: LT. rewrite ltnS => H_horizon_order_lt.
rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.
rewrite {1}/make_wc_at.
@@ -478,7 +479,7 @@ Section AuxiliaryLemmasWorkConservingTransformation.
rewrite //.
apply swap_candidate_is_in_future.
Qed.
-
+
End PrefixInclusion.
(** Next, we show that repeating the point-wise transformation up to a given horizon
@@ -515,7 +516,7 @@ Section AuxiliaryLemmasWorkConservingTransformation.
rewrite /servp /wc_transform_prefix.
clear serv servp.
apply prefix_map_property_invariance; last by done.
- intros. apply leq_trans with (service sched0 j t)=> //.
+ move=> sched0 ? ?. apply leq_trans with (service sched0 j t)=> //.
by intros; apply mwa_service_bound.
Qed.
diff --git a/behavior/ready.v b/behavior/ready.v
index c13bc91436c01a546be7b717651a723aace0b739..d41858ae42da5e6334e122b9c7c76d436a4d7652 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -80,3 +80,5 @@ Section ValidSchedule.
properties are implied by jobs_must_be_ready_to_execute. *)
End ValidSchedule.
+
+Obligation Tactic := try done.
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 1eb487cef0d4b34fabe56fcb70f4fd215eac40aa..0baccfdf7508c6bbfa1efd132ac43c0f672a2945 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -87,3 +87,5 @@ Definition schedule {Job : JobType} (PState : ProcessorState Job) :=
[scheduled_on] and [service_on] are defined. Instead,
proofs must rely on basic lemmas about processor state classes. *)
Global Opaque scheduled_on service_on.
+
+Obligation Tactic := try done.
diff --git a/implementation/facts/extrapolated_arrival_curve.v b/implementation/facts/extrapolated_arrival_curve.v
index 54858e058728b319486c603ff9873ed1a4a4f45c..a7888284964d626f6eb5c5a2690430de21acd0ff 100644
--- a/implementation/facts/extrapolated_arrival_curve.v
+++ b/implementation/facts/extrapolated_arrival_curve.v
@@ -61,14 +61,16 @@ Section ArrivalCurvePrefixSortedLeq.
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
snd (last (t__d1, v__d1) [seq step <- steps | fst step <= t1]) <= snd (last (t__d2, v__d2) [seq step <- steps | fst step <= t2]).
- { induction steps as [ | [t__c v__c] steps]; first by done.
+ { have steps_sorted := H_sorted_leq; clear H_sorted_leq.
+ elim: steps steps_sorted => [//|[t__c v__c] steps IHsteps] steps_sorted.
simpl; intros *; move => LEv /andP [LTN1 /allP ALL1] /andP [LTN2 /allP ALL2].
- move: (H_sorted_leq); rewrite //= (@path_sorted_inE _ predT leq_steps); first last.
+ move: (steps_sorted); rewrite //= (@path_sorted_inE _ predT leq_steps); first last.
{ by apply/allP. }
{ by intros ? ? ? _ _ _; apply leq_steps_is_transitive. }
move => /andP [ALL SORT].
destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in *.
- { rewrite R1 R2 //=; apply IHsteps; try done. }
+ {
+ rewrite R1 R2 //=; apply IHsteps; try done. }
{ by lia. }
{ rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->; rewrite R2 //=; apply IHsteps; try done.
- by move: LTN1; rewrite /leq_steps => /andP //= [_ LEc].
@@ -94,13 +96,13 @@ Section ArrivalCurvePrefixSortedLeq.
value_at ac_prefix t < value_at ac_prefix (t + ε) ->
exists v, (t + ε, v) \in steps_of ac_prefix.
Proof.
- intros ? LT.
+ move=> t LT.
unfold value_at, step_at in LT.
destruct ac_prefix as [h2 steps]; simpl in LT.
rewrite [in X in _ < X](sorted_split _ _ fst t) in LT.
{ rewrite [in X in _ ++ X](eq_filter (a2 := fun x => fst x == t + ε)) in LT; last first.
{ by intros [a b]; simpl; rewrite -addn1 /ε eqn_leq. }
- { destruct ([seq x <- steps | fst x == t + ε]) eqn:LST.
+ { destruct ([seq x <- steps | fst x == t + ε]) as [|p l] eqn:LST.
{ rewrite LST in LT.
rewrite [in X in X ++ _](eq_filter (a2 := fun x => fst x <= t)) in LT; last first.
{ clear; intros [a b]; simpl.
@@ -118,7 +120,7 @@ Section ArrivalCurvePrefixSortedLeq.
}
}
{ move: (H_sorted_leq); clear H_sorted_leq; rewrite /sorted_leq_steps //= => SORT; clear H_no_inf_arrivals.
- induction steps; [by done | simpl in *].
+ elim: steps SORT => [//|a steps IHsteps] /= SORT.
move: SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move => /andP [LE SORT].
apply IHsteps in SORT.
rewrite path_sortedE; last by intros ? ? ? LE1 LE2; lia.
@@ -146,7 +148,7 @@ Section ArrivalCurvePrefixSortedLtn.
Lemma sorted_ltn_steps_imply_sorted_leq_steps_steps :
sorted_leq_steps ac_prefix.
Proof.
- destruct ac_prefix; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in *.
+ destruct ac_prefix as [d l]; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in *.
clear H_no_inf_arrivals d.
destruct l; simpl in *; first by done.
eapply sub_path; last by apply H_sorted_ltn.
@@ -181,7 +183,7 @@ Section ArrivalCurvePrefixSortedLtn.
intros * IN; destruct ac_prefix as [h steps].
unfold step_at; simpl in *.
apply in_cat in IN; move: IN => [steps__l [steps__r EQ]]; subst steps.
- apply sorted_cat in H_sorted_ltn; destruct H_sorted_ltn; clear H_sorted_ltn; last by apply ltn_steps_is_transitive.
+ apply sorted_cat in H_sorted_ltn; destruct H_sorted_ltn as [H H0]; clear H_sorted_ltn; last by apply ltn_steps_is_transitive.
rewrite filter_cat last_cat (nonnil_last _ _ (0,0)); last by rewrite //= leqnn.
move: H0; rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn => /andP [ALL SORT].
simpl; replace (filter _ _ ) with (@nil (nat * nat)); first by done.
@@ -265,7 +267,7 @@ Section ExtrapolatedArrivalCurve.
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y.
- { clear; intros * LEs LT.
+ { clear; intros s1 s2 m x y LEs LT.
move: LEs; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
{ by subst s2; rename s1 into s; right; split; [ done | lia]. }
{ by left. }
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index dc6d3ae727bcc32b5a6808cd65154044bb5fd2df..f007adccc755f6f6e03adf8e0d876ccd6fb76360 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -173,7 +173,7 @@ Section NPUniprocessorScheduler.
rewrite scheduled_at_def /schedule /uni_schedule /pmc_uni_schedule
/allocation_at /generic_schedule schedule_up_to_def //= in SCHED.
destruct (prev_job_nonpreemptive _) eqn:PREV.
- { destruct t => //; rewrite //= in SCHED, PREV.
+ { destruct t as [|t] => //; rewrite //= in SCHED, PREV.
destruct (schedule_up_to) => //.
move: PREV => /andP [READY _].
move: SCHED=> /eqP SCHED.
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
index 4a76fb63a517a9b79877ad01ffc0a8a0842d399e..1551e92f5816f1d4ac1664f5d8a6be0e1fc380e9 100644
--- a/implementation/facts/ideal_uni/prio_aware.v
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -127,7 +127,7 @@ Section PrioAwareUniprocessorScheduler.
have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
{ apply backlogged_prefix_invariance' with (h := t) => //.
rewrite /identical_prefix /uni_schedule /prefix => t' LT.
- induction t => //.
+ elim: t PREEMPT SCHED_j2 NOT_SCHED_j1 LT => [//|t IHt] PREEMPT SCHED_j2 NOT_SCHED_j1 LT.
rewrite /pmc_uni_schedule/generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
rewrite /prefix scheduled_at_def.
induction t => //.
@@ -141,4 +141,3 @@ Section PrioAwareUniprocessorScheduler.
End Priority.
End PrioAwareUniprocessorScheduler.
-
diff --git a/implementation/facts/maximal_arrival_sequence.v b/implementation/facts/maximal_arrival_sequence.v
index 73856ca8829522332e06b964d14d03dc113e2f0d..d30b102375eb32b17cc742e28265375ef986f3a2 100644
--- a/implementation/facts/maximal_arrival_sequence.v
+++ b/implementation/facts/maximal_arrival_sequence.v
@@ -178,7 +178,7 @@ Section MaximalArrivalSequence.
nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.
Proof.
move=> t h1 h2 /andP[LEQh1 LEQh2].
- induction h2; [by have -> : h1 = 0; lia |].
+ elim: h2 LEQh2 => [|h2 IHh2] LEQh2; [by have -> : h1 = 0; lia |].
rewrite leq_eqVlt in LEQh2.
move: LEQh2 => /orP [/eqP EQ | LT]; first by rewrite EQ.
feed IHh2; first by lia.
@@ -212,7 +212,7 @@ Section MaximalArrivalSequence.
Proof.
move=> t Δ LEQ.
move: (H_valid_arrival_curve tsk H_tsk_in_ts) => [ZERO MONO].
- destruct t.
+ destruct t as [|t].
{ rewrite unlock //= subn0.
rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
/next_max_arrival //= /suffix_sum subn0 unlock subn0.
@@ -245,12 +245,12 @@ Section MaximalArrivalSequence.
replace t1 with (t-Δ); last by lia.
have LEQd: Δ <= t by lia.
generalize Δ LEQd; clear LEQ Δ LEQd.
- induction t; move => Δ LEQ.
+ elim: t => [|t IHt] Δ LEQ.
{ rewrite sub0n.
rewrite number_of_task_arrivals_eq //.
by vm_compute; rewrite unlock. }
{ rewrite number_of_task_arrivals_eq //.
- destruct Δ; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
+ destruct Δ as [|Δ]; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
rewrite subSS.
specialize (IHt Δ).
feed IHt; first by lia.
@@ -263,4 +263,3 @@ Section MaximalArrivalSequence.
Qed.
End MaximalArrivalSequence.
-
diff --git a/implementation/refinements/EDF/fast_search_space.v b/implementation/refinements/EDF/fast_search_space.v
index ec06bad5dd84d826c5b8cccded0693a1f9d43f93..a5d66177c5ecb00ab4df10b501b398f988b22f54 100644
--- a/implementation/refinements/EDF/fast_search_space.v
+++ b/implementation/refinements/EDF/fast_search_space.v
@@ -109,7 +109,7 @@ Section FastSearchSpaceComputationSubset.
set (S := repeat_steps_with_offset _ _) in *.
replace (shift_points_neg _ _) with S; first by done.
symmetry; unfold shift_points_neg, shift_points_pos.
- induction S; first by done.
+ elim: S => [//|a S IHS].
rewrite //= leq_addr //= IHS.
by replace ( _ + _ - _) with a; last lia.
Qed.
@@ -119,7 +119,7 @@ Section FastSearchSpaceComputationSubset.
Lemma search_space_subset_EDF :
forall A, A \in correct_search_space ts tsk L -> A \in search_space_emax_EDF ts tsk L.
Proof.
- intros *; unfold correct_search_space, is_in_search_space.
+ move=> A; unfold correct_search_space, is_in_search_space.
rewrite mem_filter => /andP [/andP [LT /orP [CH|CH]] IN]; unfold search_space_emax_EDF.
{ move: (H_tsk_in_ts) => INTS.
apply in_cat in INTS; destruct INTS as [ts_l [ts_r EQ]].
diff --git a/implementation/refinements/EDF/nonpreemptive_sched.v b/implementation/refinements/EDF/nonpreemptive_sched.v
index fa654fa6cd0ccc2e9a98c99f0d75dc8507b00407..d86dfcfe2d27ef4fbb3ca6e59c1b63977928e2e9 100644
--- a/implementation/refinements/EDF/nonpreemptive_sched.v
+++ b/implementation/refinements/EDF/nonpreemptive_sched.v
@@ -81,7 +81,7 @@ Section Schedule.
replace (_ (_ (_ _ _) _ t) j _) with (service sched j t.+1); last first.
{ rewrite /uni_schedule /pmc_uni_schedule /generic_schedule /service
/service_during /service_at.
- apply eq_big_nat; intros.
+ apply eq_big_nat => i H.
replace (_ (_ _ _) _ t i) with (schedule_up_to (allocation_at arr_seq chp) None i i) => //.
by apply schedule_up_to_prefix_inclusion. }
move=> SERV_COST SERV_ZERO; apply /andP.
@@ -102,7 +102,7 @@ Section Schedule.
nonpreemptive_schedule (uni_schedule arr_seq).
Proof.
rewrite /nonpreemptive_schedule.
- induction t'; first by move=> t'; have->: t = 0 by lia.
+ move=> j t; elim=> [|t' IHt']; first by move=> t'; have->: t = 0 by lia.
move=> LEQ SCHED NCOMP.
destruct (ltngtP t t'.+1) as [LT | _ | EQ] => //; last by rewrite -EQ.
feed_n 3 IHt'=> //.
diff --git a/implementation/refinements/EDF/refinements.v b/implementation/refinements/EDF/refinements.v
index 02c70b146e4f81f0862d1b366021537ae11b11ae..17f7cfe9b59679faf0782036e2263da2ba9c71ec 100644
--- a/implementation/refinements/EDF/refinements.v
+++ b/implementation/refinements/EDF/refinements.v
@@ -12,7 +12,7 @@ Section Definitions.
Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
!div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
Context `{!eq_of (seq T)}.
- Context `{!eq_of (@task_T T)}.
+ Context {eq_of2 : eq_of (@task_T T)}.
(** We define a generic version of total request-bound function of
higher-or-equal priority task, ... *)
@@ -125,11 +125,11 @@ Global Instance refine_search_space_emax_EDF :
(search_space_emax_EDF (map taskT_to_task ts) (taskT_to_task tsk))
(search_space_emax_EDF_N ts tsk).
Proof.
- intros ? ?.
+ move=> ts tsk.
unfold search_space_emax_EDF, search_space_emax_EDF_N.
rewrite refinesE => L L' RL; apply refinesP.
have F: forall xs f, \cat_(x <- xs) f x = flatten (map f xs).
- { clear; induction xs as [ | x xs]; intros.
+ { clear=> T T0; elim=> [|x xs IHxs] f.
- by rewrite big_nil.
- by rewrite big_cons //= IHxs. }
rewrite F; clear F.
@@ -166,7 +166,7 @@ Global Instance refine_total_rbf' :
(total_request_bound_function (map taskT_to_task ts))
(total_rbf_T ts) | 0.
Proof.
- intros; rewrite refinesE; intros δ δ' Rδ.
+ move=> ts; rewrite refinesE => δ δ' Rδ.
move: refine_task_set' => RTS.
rewrite refinesE in RTS.
specialize (RTS ts ts (unifyxx _)); simpl in RTS.
diff --git a/implementation/refinements/FP/nonpreemptive_sched.v b/implementation/refinements/FP/nonpreemptive_sched.v
index a8e95535c63a1f50f13225bd39207681699c3d15..2dc3ce8e5063307c2fcc1824ba4de169e378dddc 100644
--- a/implementation/refinements/FP/nonpreemptive_sched.v
+++ b/implementation/refinements/FP/nonpreemptive_sched.v
@@ -77,7 +77,7 @@ Section Schedule.
set chp:= choose_highest_prio_job; set sut:= schedule_up_to.
replace (_ (_ (_ _ _) _ t) j t.+1) with (service sched j t.+1); last first.
{ rewrite /uni_schedule /pmc_uni_schedule /generic_schedule /service
- /service_during /service_at; apply eq_big_nat; intros.
+ /service_during /service_at; apply eq_big_nat => i H.
replace (_ (_ _ _) _ t i) with (sut (allocation_at arr_seq chp) None i i) => //.
by apply schedule_up_to_prefix_inclusion. }
move=> SC SZ; apply /andP.
@@ -103,7 +103,7 @@ Section Schedule.
nonpreemptive_schedule (uni_schedule arr_seq).
Proof.
rewrite /nonpreemptive_schedule.
- induction t'; first by move=> t'; have->: t = 0 by lia.
+ move=> j t; elim=> [|t' IHt']; first by move=> t'; have->: t = 0 by lia.
move=> LEQ SCHED NCOMP.
destruct (ltngtP t t'.+1) as [LT | _ | EQ] => //; last by rewrite -EQ.
feed_n 3 IHt'=> //.
diff --git a/implementation/refinements/FP/refinements.v b/implementation/refinements/FP/refinements.v
index b2ff698b85e94252a3a5de2b5b8801f77e7df541..31cdbb32ccdfbad722582ab8b010e0c54a61e1ba 100644
--- a/implementation/refinements/FP/refinements.v
+++ b/implementation/refinements/FP/refinements.v
@@ -15,7 +15,7 @@ Section Definitions.
Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
!div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
Context `{!eq_of (seq T)}.
- Context `{!eq_of (@task_T T)}.
+ Context {eq_of2 : eq_of (@task_T T)}.
(** We define a generic version of higher-or-equal priority task, ... *)
Definition hep_task_T tsk_o tsk := (task_priority_T tsk <= @task_priority_T T tsk_o)%C.
@@ -139,7 +139,7 @@ Global Instance refine_total_hep_rbf' :
(total_hep_rbf (map taskT_to_task ts) (taskT_to_task tsk))
(total_hep_rbf_T ts tsk) | 0.
Proof.
- intros; rewrite refinesE; intros δ δ' Rδ.
+ move=> ts tsk; rewrite refinesE => δ δ' Rδ.
move: refine_task_set' => RTS.
rewrite refinesE in RTS.
specialize (RTS ts ts (unifyxx _)); simpl in RTS.
diff --git a/implementation/refinements/arrival_bound.v b/implementation/refinements/arrival_bound.v
index fb352f2983f542ee17419484ab71d925b8b8dc50..ad47b718f2eb8e34329ef65a29bc62167b8976a8 100644
--- a/implementation/refinements/arrival_bound.v
+++ b/implementation/refinements/arrival_bound.v
@@ -208,7 +208,7 @@ Section Refinements.
destruct evec as [h st].
apply prod_R_pair_R.
- by compute.
- - simpl; clear h; induction st.
+ - simpl; clear h; elim: st => [|a st IHst].
+ apply list_R_nil_R.
+ simpl; apply list_R_cons_R; last by done.
destruct a; unfold tb2tn, tmap; simpl.
@@ -221,7 +221,7 @@ Section Refinements.
refines ( list_R (prod_R Rnat Rnat) )%rel xs xs' ->
refines ( bool_R )%rel (sorted ltn_steps xs) (sorted ltn_steps_T xs').
Proof.
- induction xs as [ | x xs]; intros * Rxs.
+ elim=> [|x xs IHxs] xs' Rxs.
{ destruct xs' as [ | x' xs']; first by tc.
by rewrite refinesE in Rxs; inversion Rxs. }
{ destruct xs' as [ | x' xs']; first by rewrite refinesE in Rxs; inversion Rxs.
@@ -240,7 +240,7 @@ Section Refinements.
refines ( list_R (prod_R Rnat Rnat) )%rel xs xs' ->
refines ( bool_R )%rel (sorted leq_steps xs) (sorted leq_steps_T xs').
Proof.
- induction xs as [ | x xs]; intros * Rxs.
+ elim=> [|x xs IHxs] xs' Rxs.
{ destruct xs' as [ | x' xs']; first by tc.
by rewrite refinesE in Rxs; inversion Rxs. }
{ destruct xs' as [ | x' xs']; first by rewrite refinesE in Rxs; inversion Rxs.
@@ -267,9 +267,8 @@ Section Refinements.
apply RL; clear RL.
- by apply refinesP; refines_apply.
- apply filter_R.
- + intros [n1 n2] [n1' n2'] Rnn.
- inversion Rnn; subst; clear Rnn X0; rename X into Rn1.
- by rewrite //=; apply refinesP; refines_apply.
+ + move=> _ _ [n1 n1' Rn1 _ _ _] /=.
+ by apply: refinesP; apply: refines_apply.
+ unfold steps_of, steps_of_T.
by apply refinesP; refines_apply.
Qed.
@@ -280,11 +279,8 @@ Section Refinements.
Proof.
rewrite refinesE => evec evec' Revec.
destruct evec as [h st], evec' as [h' st'].
- inversion Revec; subst; rename X into Rh; rename X0 into Rst.
- rewrite /time_steps_of /time_steps_of_T //=.
- apply refinesP; eapply refine_map.
- - by rewrite refinesE; apply Rst.
- - by apply refines_fst_R.
+ case: Revec => n1 n1' Rn1 n2 n2' Rn2.
+ by apply: refinesP; apply: refines_apply.
Qed.
(** Next, we prove the refinement for the [extrapolated_arrival_curve] function. *)
@@ -302,20 +298,17 @@ Section Refinements.
Proof.
rewrite refinesE => arrival_curve_prefix arrival_curve_prefix' Rarrival_curve_prefix.
destruct arrival_curve_prefix as [h steps], arrival_curve_prefix' as [h' steps'].
- inversion_clear Rarrival_curve_prefix; rename X into Rh, X0 into Rsteps.
- unfold Rtask_ab, fun_hrel, task_abT_to_task_ab, ACPrefixT_to_ACPrefix.
- simpl.
+ case: Rarrival_curve_prefix => {}h {}h' Rh {}steps {}steps' Rsteps.
+ rewrite /Rtask_ab /fun_hrel /task_abT_to_task_ab /ACPrefixT_to_ACPrefix /=.
have ->: nat_of_bin h' = h by rewrite -Rh.
have ->: m_tb2tn steps' = steps; last by done.
- clear h h' Rh; move: steps' Rsteps; induction steps; intros.
+ clear h h' Rh; elim: steps steps' Rsteps => [|a steps IHsteps] steps' Rsteps.
- by destruct steps'; [done | inversion Rsteps].
- - destruct steps'; first by inversion Rsteps.
- inversion_clear Rsteps; rename X into Rh, X0 into Rsteps.
- apply/eqP; rewrite //= eqseq_cons; apply/andP; split.
- + destruct a, p; unfold tb2tn, tmap; simpl; apply/eqP.
- apply prod_RE in Rh.
- by compute in Rh; destruct Rh; subst.
- + by apply/eqP; apply: IHsteps.
+ - destruct steps' as [|p steps']; first by inversion Rsteps.
+ inversion_clear Rsteps as [|? ? Rap ? ? Rstep].
+ rewrite /m_tb2tn/= /tb2tn/tmap/=.
+ congr cons; first by case: Rap => _ {}a <- _ b <-.
+ exact: IHsteps.
Qed.
(** Next, we define some useful equality functions to guide the typeclass engine. *)
@@ -348,12 +341,12 @@ Section Refinements.
have -> : ((h1, evec1) == (h2, evec2))%C = ((h1 == h2) && (evec1 == evec2))%C by constructor.
apply andb_R.
apply refinesP; refines_apply.
- clear h1 h2; move: evec2; induction evec1 as [| h1 evec1]; first by intros [].
- simpl; intros [ | h2 evec2]; first by done.
+ clear h1 h2; move: evec2; elim: evec1 => [[] //|h1 evec1 IHevec1].
+ case=> [//|h2 evec2].
rewrite //= !eqseq_cons.
apply andb_R; last by apply IHevec1.
- destruct h1, h2; simpl.
- rewrite /tb2tn /tmap; simpl.
+ move: h1 h2 => [n n0] [n1 n2].
+ rewrite /tb2tn /tmap /=.
replace ((n, n0) == (n1, n2)) with ((n == n1) && (n0 == n2)) by constructor.
replace ((nat_of_bin n, nat_of_bin n0) == (nat_of_bin n1, nat_of_bin n2)) with
((nat_of_bin n == nat_of_bin n1) && (nat_of_bin n0 == nat_of_bin n2)) by constructor.
diff --git a/implementation/refinements/arrival_curve.v b/implementation/refinements/arrival_curve.v
index ca61002ec0b815b7cf415c5a1d03fb0b939f1525..21903a485a75c26f32c129b24b9c6fee0daf96bd 100644
--- a/implementation/refinements/arrival_curve.v
+++ b/implementation/refinements/arrival_curve.v
@@ -68,15 +68,7 @@ Section Facts.
(** Consider a task [tsk]. *)
Variable tsk : Task.
- (** First, we show that [valid_arrivals] matches [valid_arrivals_dec]. *)
- Lemma valid_arrivals_P :
- reflect (valid_arrivals tsk) (valid_arrivals tsk).
- Proof.
- destruct tsk, task_arrival.
- all: unfold valid_arrivals, valid_arrivals; try by apply idP.
- Qed.
-
- (** Next, we show that a task is either periodic, sporadic, or bounded by
+ (** We show that a task is either periodic, sporadic, or bounded by
an arrival-curve prefix. *)
Lemma arrival_cases :
is_periodic_arrivals tsk
@@ -105,7 +97,7 @@ Section Theory.
positive_horizon positive_horizon_T.
Proof.
unfold positive_horizon, positive_horizon_T.
- apply refines_abstr; intros.
+ apply: refines_abstr => a b X.
unfold horizon_of, horizon_of_T.
destruct a as [h s], b as [h' s']; simpl.
rewrite refinesE; rewrite refinesE in X; inversion_clear X.
@@ -168,7 +160,7 @@ Section Theory.
(valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk) | 0.
Proof.
- intros ?.
+ move=> tsk.
have Rtsk := refine_task'.
rewrite refinesE in Rtsk.
specialize (Rtsk tsk tsk (unifyxx _)); simpl in Rtsk.
@@ -182,13 +174,13 @@ Section Theory.
{ unfold ArrivalCurvePrefix in *.
refines_apply.
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].
- inversion Rab; refines_apply.
- move: H1; clear; move: st'.
- rewrite refinesE; induction st; intros [|s st']; try done.
- - by intros _; rewrite //=; apply list_R_nil_R.
- - intros ?; inversion H1; rewrite //=.
- apply list_R_cons_R; last by apply IHst.
- destruct s, a; unfold tb2tn, tmap; simpl.
+ inversion Rab as [(H0, H1)]; refines_apply.
+ rewrite refinesE.
+ move: H1; clear; elim: st st' => [|s st IHst] [|s' st'] //.
+ - by move=> _; apply: list_R_nil_R.
+ - move=> H1; inversion H1 as [(H0, H2)].
+ apply: list_R_cons_R; last by apply IHst.
+ destruct s', s; unfold tb2tn, tmap; simpl.
by apply refinesP; refines_apply. }
Qed.
@@ -215,11 +207,11 @@ Section Theory.
by rewrite refinesE; inversion Rab; subst. }
{ apply refinesP; refines_apply.
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].
- inversion Rab; refines_apply.
+ inversion Rab as [(H0, H1)]; refines_apply.
move: H1; clear; move: st'.
- rewrite refinesE; induction st; intros [ |s st']; try done.
+ rewrite refinesE; elim: st => [|a st IHst] [ |s st'] //.
- by intros _; rewrite //=; apply list_R_nil_R.
- - intros ?; inversion H1; rewrite //=.
+ - intros H1; inversion H1; rewrite //=.
apply list_R_cons_R; last by apply IHst.
destruct s, a; unfold tb2tn, tmap; simpl.
by apply refinesP; refines_apply. } }
@@ -257,11 +249,11 @@ Section Theory.
move=> arrival_curve_prefix arrival_curve_prefixT δ δ' Rδ Rab.
refines_apply.
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].
- inversion Rab; refines_apply.
+ inversion Rab as [(H0, H1)]; refines_apply.
move: H1; clear; move: st'.
- rewrite refinesE; induction st; intros [ |s st']; try done.
+ rewrite refinesE; elim: st => [|a st IHst] [ |s st'] //.
- by intros _; rewrite //=; apply list_R_nil_R.
- - intros ?; inversion H1; rewrite //=.
+ - intros H1; inversion H1; rewrite //=.
apply list_R_cons_R; last by apply IHst.
destruct s, a; unfold tb2tn, tmap; simpl.
by apply refinesP; refines_apply.
@@ -325,8 +317,8 @@ Section Theory.
all: try (inversion Rab; fail).
all: try (inversion Rab; subst; apply refinesP; refines_apply; fail).
destruct e as [h?], eT as [? st];[apply refinesP; refines_apply; inversion Rab; tc].
- inversion Rab; subst.
- induction st; first by rewrite //= refinesE; apply list_R_nil_R.
+ inversion Rab as [(H__, Hst)]; subst.
+ elim: st Rab Hst => [|a st IHst] Rab H1; first by rewrite //= refinesE; apply list_R_nil_R.
destruct a; rewrite refinesE.
apply list_R_cons_R; first by apply refinesP; unfold tb2tn,tmap; refines_apply.
by apply refinesP, IHst.
@@ -354,7 +346,7 @@ Section Theory.
all: try (inversion Rab; subst; refines_apply; fail).
destruct e as [h?], eT as [? st]; refines_apply; first by inversion Rab; subst; tc.
inversion Rab; subst.
- induction st; first by rewrite //= refinesE; apply list_R_nil_R.
+ elim: st Rab => [|a st IHst] Rab; first by rewrite //= refinesE; apply list_R_nil_R.
destruct a; rewrite //= refinesE.
apply list_R_cons_R; first by apply refinesP; unfold tb2tn,tmap; refines_apply.
by apply refinesP, IHst.
diff --git a/implementation/refinements/arrival_curve_prefix.v b/implementation/refinements/arrival_curve_prefix.v
index a153016bf77457958a37f223d87df3213efda0da..540dd8a49f0ee4f4f39dc594e120b4587cf88620 100644
--- a/implementation/refinements/arrival_curve_prefix.v
+++ b/implementation/refinements/arrival_curve_prefix.v
@@ -45,7 +45,7 @@ Section ValidArrivalCurvePrefixFacts.
intros st IN; unfold get_time_steps_of_task in *.
move: (H_valid_task_set) => VAL; specialize (VAL _ H_tsk_in_ts).
unfold valid_arrivals in VAL; unfold get_arrival_curve_prefix in *.
- destruct (task_arrival tsk).
+ destruct (task_arrival tsk) as [a|a|a].
{ by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
move: IN; rewrite mem_seq1 => /eqP EQ; subst. }
{ by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
@@ -70,7 +70,7 @@ Section ValidArrivalCurvePrefixFacts.
forall A offs,
A \in repeat_steps_with_offset tsk offs -> A > 0.
Proof.
- intros * IN.
+ intros A offs IN.
move: IN => /flatten_mapP [o INo IN].
move: IN => /mapP [st IN EQ]; subst A.
rewrite addn_gt0; apply/orP; left.
diff --git a/implementation/refinements/fast_search_space_computation.v b/implementation/refinements/fast_search_space_computation.v
index bc9585d95321379c0235e38e99c7dc82cbada5f6..091829317dca0a8b60346e2e3feabbb4ecc60a58 100644
--- a/implementation/refinements/fast_search_space_computation.v
+++ b/implementation/refinements/fast_search_space_computation.v
@@ -58,7 +58,7 @@ Section FastSearchSpaceComputation.
- destruct get_time_steps_of_task; rewrite //= -index_mem in IN.
by rewrite /last0; simpl (last 0 _); rewrite index_last. }
{ exfalso. (* h is at least the last step *)
- destruct get_time_steps_of_task eqn:TS => //.
+ destruct get_time_steps_of_task as [|d l] eqn:TS => //.
have IN: last0 (d::l) \in d::l by rewrite /last0 //=; apply mem_last.
unfold large_horizon, get_time_steps_of_task in *.
rewrite EQ in TS; rewrite TS in LARGEh.
@@ -66,7 +66,6 @@ Section FastSearchSpaceComputation.
by rewrite /get_horizon_of_task EQ in LT1; lia. }
Qed.
-
(** Next, we show that for each offset [A] in the search space for fixed-priority
tasks, either (1) [A+ε] is zero or a multiple of the horizon, offset by
one of the time steps of the arrival curve prefix, or (2) [A+ε] is
@@ -128,7 +127,7 @@ Section FastSearchSpaceComputation.
A \in search_space_arrival_curve_prefix_FP tsk L.
Proof.
move: (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts) => [evec [EMAX VALID]].
- intros * LT DIV; rewrite /search_space_arrival_curve_prefix_FP.
+ intros A LT DIV; rewrite /search_space_arrival_curve_prefix_FP.
destruct VALID as [POSh [LARGEh [NOINF [BUR SORT]]]].
replace A with (A + ε - ε); last by lia.
rewrite subn1; apply map_f.
@@ -156,7 +155,7 @@ Section FastSearchSpaceComputation.
A + ε = i * get_horizon_of_task tsk + t ->
A \in search_space_arrival_curve_prefix_FP tsk L.
Proof.
- move: (H_valid_task_set) => VALID; intros * LT IN EQ; rewrite /search_space_arrival_curve_prefix_FP.
+ move: (H_valid_task_set) => VALID; intros i t A LT IN EQ; rewrite /search_space_arrival_curve_prefix_FP.
replace A with (A + ε - ε); last by lia.
rewrite subn1; apply map_f.
set (h := get_horizon_of_task tsk) in *.
@@ -187,7 +186,7 @@ Section FastSearchSpaceComputation.
have -> : vec (A %% h) = vec h.
{ rewrite /vec /value_at.
have -> : ((step_at evec (A %% h)) = (step_at evec h)) => //.
- rewrite (pred_Sn A) -addn1 modn_pred; [|repeat destruct h=> //|lia].
+ rewrite (pred_Sn A) -addn1 modn_pred; [|repeat destruct h as [|h]=> //|lia].
rewrite /step_at DIV.
have -> : [seq step <- steps_of evec | step.1 <= h] = steps_of evec.
{ apply /all_filterP /allP => [step IN]; apply ltnW; subst h.
@@ -199,7 +198,8 @@ Section FastSearchSpaceComputation.
move: LTH; rewrite /get_horizon_of_task EMAX => VALID.
specialize (VALID step.1).
feed VALID; first by rewrite /get_time_steps_of_task EMAX; apply (map_f fst).
- by destruct (horizon_of evec). }
+ by destruct (horizon_of evec).
+ }
rewrite -mulSnr {1}(pred_Sn A) divn_pred -(addn1 A) DIV subn1 prednK //=.
move: DIV => /dvdnP [k EQk]; rewrite EQk.
by destruct k;[rewrite /ε in EQk; lia | rewrite mulnK]. }
diff --git a/implementation/refinements/refinements.v b/implementation/refinements/refinements.v
index dc21360209098230e398e3aa1435742e32d8109a..670e6ee98496203fc8c007f9d9e190426be62d35 100644
--- a/implementation/refinements/refinements.v
+++ b/implementation/refinements/refinements.v
@@ -172,7 +172,7 @@ Lemma posBinNatNotZero:
forall p, ~ (nat_of_bin (N.pos p)) = O.
Proof.
rewrite -[0]bin_of_natK.
- intros ? EQ.
+ intros p EQ.
have BJ := @Bijective _ _ nat_of_bin bin_of_nat.
feed_n 2 BJ.
{ by intros ?; rewrite bin_of_natE; apply nat_of_binK. }
@@ -204,7 +204,7 @@ Lemma refine_ltn :
Rnat b b' ->
bool_R (a < b) (a' < b')%C.
Proof.
- intros * Ra Rb.
+ move=> a a' b b' Ra Rb.
replace (@lt_op N lt_N a' b') with (@leq_op N leq_N (1 + a')%N b');
first by apply refinesP; refines_apply.
unfold leq_op, leq_N, lt_op, lt_N.
@@ -319,24 +319,19 @@ Global Instance refine_last :
forall {A B : Type} (rA : A -> B -> Type),
refines (rA ==> list_R rA ==> rA)%rel last last.
Proof.
- intros *; rewrite refinesE => d d' Rd xs xs' Rxs.
- move: d d' Rd xs' Rxs; induction xs; intros.
+ move=> A B rA; rewrite refinesE => d d' Rd xs xs' Rxs.
+ elim: xs d d' Rd xs' Rxs => [|a xs IHxs] d d' Rd xs' Rxs.
- by destruct xs'; last inversion Rxs.
- - destruct xs'; first by inversion Rxs.
- inversion Rxs; subst; clear Rxs; rename X1 into Rab, X4 into Rxs.
- by simpl; apply IHxs.
+ - case: xs' Rxs => [|b xs'] Rxs; first by inversion Rxs.
+ exact: last_R.
Qed.
(** Next, we prove a refinement for the [size] function. *)
Global Instance refine_size A C (rAC : A -> C -> Type) :
refines (list_R rAC ==> Rnat)%rel size size_T.
Proof.
- rewrite refinesE => h.
- induction h; intros h' Rh; first by destruct h'; last inversion Rh.
- destruct h'; first by inversion Rh.
- inversion_clear Rh.
- apply IHh in X4; clear IHh; simpl.
- by have H := Rnat_S; rewrite refinesE in H; specialize (H _ _ X4).
+ apply: refines_abstr => s s'; rewrite !refinesE.
+ by elim=> [//|a a' Ra {}s {}s' Rs IHs] /=; apply: refinesP.
Qed.
(** Next, we prove a refinement for the [iota] function when applied
@@ -346,9 +341,9 @@ Lemma iotaTsuccN :
iota_T a (N.succ (Pos.pred_N p)) = a :: iota_T (succN a) (Pos.pred_N p).
Proof.
move=> a p.
- destruct (N.succ (Pos.pred_N p)) eqn:EQ; first by move: (N.neq_succ_0 (Pos.pred_N p)).
+ destruct (N.succ (Pos.pred_N p)) as [|p0] eqn:EQ; first by move: (N.neq_succ_0 (Pos.pred_N p)).
move: (posBinNatNotZero p0) => /eqP EQn0.
- destruct (nat_of_bin (N.pos p0)) eqn:EQn; first by done.
+ destruct (nat_of_bin (N.pos p0)) as [|n] eqn:EQn; first by done.
have -> : n = Pos.pred_N p; last by rewrite //= /succN /add_N /add_op N.add_comm.
apply /eqP.
rewrite -eqSS -EQn -EQ -addn1.
@@ -360,7 +355,7 @@ Qed.
Global Instance refine_iota :
refines (Rnat ==> Rnat ==> list_R Rnat)%rel iota iota_T.
Proof.
- rewrite refinesE => a a' Ra b; move: a a' Ra; induction b; intros a a' Ra b' Rb.
+ rewrite refinesE => a a' Ra b; move: a a' Ra; elim: b => [|b IHb] a a' Ra b' Rb.
{ destruct b'; first by rewrite //=; apply list_R_nil_R.
by compute in Rb; apply posBinNatNotZero in Rb. }
{ destruct b'; first by compute in Rb; destruct b.
@@ -403,7 +398,7 @@ Global Instance refine_abstract :
forall xs,
refines (list_R Rnat)%rel (map nat_of_bin xs) xs | 0.
Proof.
- induction xs; first by rewrite refinesE; simpl; apply list_R_nil_R.
+ elim=> [|a xs IHxs]; first by rewrite refinesE; simpl; apply list_R_nil_R.
rewrite //= refinesE; rewrite refinesE in IHxs.
by apply list_R_cons_R; last by done.
Qed.
@@ -418,7 +413,7 @@ Qed.
Lemma refine_foldr_lemma :
refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> list_R Rnat ==> Rnat)%rel foldr foldr.
Proof.
- rewrite refinesE => f f' Rf d d' Rd xs; induction xs as [ | x xs]; intros xs' Rxs.
+ rewrite refinesE => f f' Rf d d' Rd; elim=> [|x xs IHxs] xs' Rxs.
{ by destruct xs' as [ | x' xs']; [ done | inversion Rxs ]. }
{ destruct xs' as [ | x' xs']; first by inversion Rxs.
inversion Rxs; subst.
@@ -442,7 +437,7 @@ Section GenericLists.
refines ( rT ==> bool_R )%rel R R' ->
refines Rnat (\sum_(x <- xs | R x) F x) (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x']).
Proof.
- intros * Rxs Rf Rr.
+ move=> R R' F F' rT Rxs Rf Rr.
have ->: \sum_(x <- xs | R x) F x = foldr addn 0 [seq F x | x <- xs & R x].
{ by rewrite foldrE big_map big_filter. }
refines_apply.
@@ -461,7 +456,7 @@ Section GenericLists.
refines ( rT ==> Rnat )%rel F F' ->
refines Rnat (\sum_(x <- xs) F x) (foldr +%C 0%C [seq F' x' | x' <- xs']).
Proof.
- intros * Rxs Rf.
+ move=> F F' rT Rxs Rf.
have ->: \sum_(x <- xs) F x = foldr addn 0 [seq F x | x <- xs] by rewrite foldrE big_map.
refines_apply.
by apply refine_foldr_lemma.
@@ -479,7 +474,7 @@ Section GenericLists.
refines ( rT ==> bool_R )%rel R R' ->
refines Rnat (\max_(x <- xs | R x) F x) (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x']).
Proof.
- intros * Rxs Rf Rr.
+ move=> R R' F F' rT Rxs Rf Rr.
have ->: \max_(x <- xs | R x) F x = foldr maxn 0 [seq F x | x <- xs & R x]
by rewrite foldrE big_map big_filter.
refines_apply.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index f8dc6e48ab8ea8d5bfbf366621014500a2087277..7108c8012ecb1d291ef3bfe4e74e83832f2bc213 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -36,7 +36,9 @@ Section State.
given state [s] iff [s] is [Some j]. *)
service_on j s (_ : unit) := if s == Some j then 1 else 0;
|}.
- Next Obligation. by rewrite /nat_of_bool; case: ifP H => // ? /negP[]. Qed.
+ Next Obligation.
+ by move=> j s ?; rewrite /nat_of_bool; case: ifP => // ? /negP[].
+ Qed.
End State.
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index 1131457e485d32f435eb7f16496653d20ea02f87..5298f4f4867ecd582e1ba7f576b63351c209469d 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -64,11 +64,7 @@ Section Schedule.
scheduled_on := multiproc_scheduled_on;
service_on := multiproc_service_on
|}.
- Next Obligation.
- move: j s r H.
- move=> j mps cpu.
- by apply: service_in_implies_scheduled_in.
- Qed.
+ Next Obligation. by move=> ? ? ?; apply: service_in_implies_scheduled_in. Qed.
(** From the instance [multiproc_state], we get the function [service_in].
The service received by a given job [j] in a given multiprocessor state
diff --git a/model/processor/spin.v b/model/processor/spin.v
index 7bbbe392ff6098769fb5890c460f1f96f6aa3c02..14bf807e6dd76f0b8e371ce4daea193a2ab52759 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -54,10 +54,5 @@ Section State.
scheduled_on := spin_scheduled_on;
service_on := spin_service_on
|}.
- Next Obligation.
- move: r H.
- case: s=>//= j' _.
- rewrite /nat_of_bool.
- by case: ifP.
- Qed.
+ Next Obligation. by move=> j [] //= j' _ /negbTE ->. Qed.
End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index 73a19bbd7d5f935a3f90115266c9bfe601771dbe..fef498707f97ff9cf4f423040ea93ef62063d055 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -51,10 +51,6 @@ Section State.
scheduled_on := varspeed_scheduled_on;
service_on := varspeed_service_on
|}.
- Next Obligation.
- move: r H.
- case: s=>//= j' v _.
- by case: ifP.
- Qed.
+ Next Obligation. by move=> j [] //= j' v _; case: ifP. Qed.
End State.
diff --git a/model/readiness/jitter.v b/model/readiness/jitter.v
index 728f2609335502b556d2ddb2e8f9d1ccfc94c5c2..816cf6cb19e043ad0b31bcef9db0b26399132bee 100644
--- a/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -40,7 +40,7 @@ Section ReadinessOfJitteryJobs.
job_ready sched j t := is_released j t && ~~ completed_by sched j t
}.
Next Obligation.
- move: H2 => /andP [REL UNFINISHED].
+ move=> sched j t /andP[REL UNFINISHED].
rewrite /pending. apply /andP. split => //.
move: REL. rewrite /is_released /has_arrived.
by apply: leq_trans; rewrite leq_addr.
diff --git a/model/readiness/sequential.v b/model/readiness/sequential.v
index e199be6e7dfd8cbdf3515772ddba13d95b023929..98ec49cc71d562ae8ab7a4184f292e2d7f622436 100644
--- a/model/readiness/sequential.v
+++ b/model/readiness/sequential.v
@@ -30,8 +30,8 @@ Section SequentialTasksReadiness.
#[local,program] Instance sequential_ready_instance : JobReady Job PState :=
{
job_ready sched j t := pending sched j t &&
- prior_jobs_complete arr_seq sched j t
+ prior_jobs_complete arr_seq sched j t;
}.
- Next Obligation. by move: H2 => /andP[]. Qed.
+ Next Obligation. by move=> sched j t /andP[]. Qed.
End SequentialTasksReadiness.
diff --git a/model/readiness/suspension.v b/model/readiness/suspension.v
index 0a9020b77534b4a3a528f42e142044c54b5e4620..b801ff78cf24fb970a33cfbb036df0a134cf6885 100644
--- a/model/readiness/suspension.v
+++ b/model/readiness/suspension.v
@@ -49,7 +49,7 @@ Section ReadinessOfSelfSuspendingJobs.
&& ~~ completed_by sched j t
}.
Next Obligation.
- move: H2 => /andP [PASSED UNFINISHED].
+ move=> sched j t /andP[PASSED UNFINISHED].
rewrite /pending. apply /andP. split => //.
move: PASSED. rewrite /suspension_has_passed /has_arrived => /andP [ARR _].
by apply: leq_trans ARR; rewrite leq_addr.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 55cf50e14139311c54a0159d19ece655069fe5b0..67d9386f735ddd957356fcd9a14786dccee02cf6 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -200,7 +200,8 @@ Section AbstractRTAforFPwithArrivalCurves.
Proof.
move => j ARR TSK POS.
edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 BI]]]]; rt_eauto.
- { intros; rewrite {2}H_fixed_point leq_add //.
+ {
+ intros; rewrite {2}H_fixed_point leq_add //.
rewrite /workload_of_higher_or_equal_priority_jobs /total_hep_rbf
/total_hep_request_bound_function_FP
/workload_of_jobs /hep_job /FP_to_JLFP.
@@ -232,7 +233,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Lemma instantiated_task_interference_is_bounded :
task_interference_is_bounded_by arr_seq sched tsk (fun t A R => IBF_other R).
Proof.
- intros ? ? ? ? ARR TSK ? NCOMPL BUSY; simpl.
+ intros j R0 t1 t2 ARR TSK ? NCOMPL BUSY; simpl.
move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 0cca1937ba541eb15e9871f5ce4b5cb19e50fdb2..a11602f47d0b84e6816a5ff4747d933a01a5979e 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -18,7 +18,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
- Context `{TaskCost Task}.
+ Context {tc : TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
@@ -136,7 +136,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp:
response_time_bounded_by tsk R.
Proof.
- move: (posnP (@task_cost _ H tsk)) => [ZERO|POS].
+ move: (posnP (@task_cost _ tc tsk)) => [ZERO|POS].
{ intros j ARR TSK.
have ZEROj: job_cost j = 0.
{ move: (H_valid_job_cost j ARR) => NEQ.
diff --git a/util/bigcat.v b/util/bigcat.v
index 98a919e363004bb9af1d936b72d9efb721ede0ed..685f07591deffd4dab9051844d4c77883f85ee27 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -43,12 +43,11 @@ Section BigCatNatLemmas.
x \in f i /\ m <= i < n.
Proof.
intros x m n IN.
- induction n; first by rewrite big_geq // in IN.
+ elim: n IN => [|n IHn] IN; first by rewrite big_geq // in IN.
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
rewrite big_nat_recr // /= mem_cat in IN.
move: IN => /orP [HEAD | TAIL].
- - apply IHn in HEAD; destruct HEAD; exists x0.
- move: H => [H /andP [H0 H1]].
+ - move: (IHn HEAD) => [x0 [H /andP[H0 H1]]]; exists x0.
split; first by done.
by apply/andP; split; last by apply ltnW.
- exists n; split; first by done.
@@ -94,7 +93,7 @@ Section BigCatNatLemmas.
case (leqP n1 n2) => [LE | GT]; last by rewrite big_geq // ltnW.
rewrite -[n2](addKn n1).
rewrite -addnBA //; set delta := n2 - n1.
- induction delta; first by rewrite addn0 big_geq.
+ elim: delta => [|delta IHdelta]; first by rewrite addn0 big_geq.
rewrite addnS big_nat_recr /=; last by apply leq_addr.
rewrite cat_uniq; apply/andP; split; first by apply IHdelta.
apply /andP; split; last by apply H_uniq_seq.
@@ -155,11 +154,11 @@ Section BigCatNatLemmas.
forall {X : Type} (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat),
[seq x <- \cat_(t1 <= t < t2) F t | P x] = \cat_(t1 <= t < t2)[seq x <- F t | P x].
Proof.
- intros.
+ move=> X F P t1 t2.
specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
+ have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
move: EX => [Δ EQ]; subst t2.
- induction Δ.
+ elim: Δ T1_LT => [|Δ IHΔ] T1_LT.
{ by rewrite addn0 !big_geq => //. }
{ rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
rewrite filter_cat IHΔ => //.
@@ -174,11 +173,11 @@ Section BigCatNatLemmas.
\sum_(t1 <= t < t2) size (F t) =
size (\cat_(t1 <= t < t2) F t).
Proof.
- intros.
+ move=> X F t1 t2.
specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
- have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
move: EX => [Δ EQ]; subst t2.
- induction Δ.
+ elim: Δ T1_LT => [|Δ IHΔ] T1_LT.
{ by rewrite addn0 !big_geq => //. }
{ rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
by rewrite size_cat IHΔ => //; lia. }
@@ -208,7 +207,7 @@ Section BigCatLemmas.
y \in \cat_(x <- s) f x.
Proof.
move=> x y s INs INfx.
- induction s; first by done.
+ elim: s INs => [//|z s IHs] INs.
rewrite big_cons mem_cat.
move:INs; rewrite in_cons => /orP[/eqP HEAD | CONS].
- by rewrite -HEAD; apply /orP; left.
@@ -222,8 +221,7 @@ Section BigCatLemmas.
y \in \cat_(x <- s) f x ->
exists x, x \in s /\ y \in f x.
Proof.
- induction s; first by rewrite big_nil.
- move=> y.
+ elim=> [|a s IHs] y; first by rewrite big_nil.
rewrite big_cons mem_cat => /orP[HEAD | CONS].
- exists a.
by split => //; apply mem_head.
@@ -240,7 +238,7 @@ Section BigCatLemmas.
\cat_(xs <- xss) [seq x <- f xs | P x] .
Proof.
move=> xss P.
- induction xss.
+ elim: xss => [|a xss IHxss].
- by rewrite !big_nil.
- by rewrite !big_cons filter_cat IHxss.
Qed.
@@ -264,7 +262,7 @@ Section BigCatLemmas.
uniq xs ->
uniq (\cat_(x <- xs) (f x)).
Proof.
- induction xs; first by rewrite big_nil.
+ elim=> [|a xs IHxs]; first by rewrite big_nil.
rewrite cons_uniq => /andP [NINxs UNIQ].
rewrite big_cons cat_uniq.
apply /andP; split; first by apply H_uniq_f.
@@ -315,7 +313,7 @@ Section BigCatLemmas.
\cat_(x <- xs) [seq x' <- f x | g x' == y] = f y.
Proof.
move=> y xs IN UNI.
- induction xs as [ | x' xs]; first by done.
+ elim: xs IN UNI => [//|x' xs IHxs] IN UNI.
move: IN; rewrite in_cons => /orP [/eqP EQ| IN].
{ subst; rewrite !big_cons.
have -> : [seq x <- f x' | g x == x'] = f x'.
@@ -363,7 +361,7 @@ Section BigCatNestedCount.
count P (\cat_(x <- xs) \cat_(y <- ys) F x y) =
count P (\cat_(y <- ys) \cat_(x <- xs) F x y).
Proof.
- induction xs as [|x0 seqX IHxs]; induction ys as [|y0 seqY IHys]; intros.
+ elim=> [|x0 seqX IHxs]; elim=> [|y0 seqY IHys].
{ by rewrite !big_nil. }
{ by rewrite big_cons count_cat -IHys !big_nil. }
{ by rewrite big_cons count_cat IHxs !big_nil. }
@@ -375,5 +373,3 @@ Section BigCatNestedCount.
Qed.
End BigCatNestedCount.
-
-
diff --git a/util/div_mod.v b/util/div_mod.v
index 611d2166beeb8f4ac0bd9734ddb1a38bcebd720d..7ae5144d73b5dc7cb1ba0853a9ed97bb3f95736d 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -12,7 +12,7 @@ Section DivMod.
t1 %/ h = t2 %/ h ->
t1 %% h <= t2 %% h.
Proof.
- intros * LT EQ.
+ move=> t1 t2 h LT EQ.
destruct (posnP h) as [Z | POSh].
{ by subst; rewrite !modn0. }
{ have EX: exists k, t1 + k = t2.
@@ -33,7 +33,7 @@ Section DivMod.
x %/ y < (x + 1) %/ y ->
y %| (x + 1).
Proof.
- intros ? ? LT.
+ move=> x y LT.
destruct (posnP y) as [Z | POS]; first by subst y.
move: LT; rewrite divnD // -addn1 -addnA leq_add2l addn_gt0 => /orP [ONE | LE].
{ by destruct y as [ | []]. }
@@ -123,7 +123,7 @@ Section DivFloorCeil.
rewrite ltn_divRL //.
apply: (leq_trans _ LEQ).
move: (leq_trunc_div m d) => LEQm.
- destruct (ltngtP (m %/ d * d) m) => //.
+ destruct (ltngtP (m %/ d * d) m) as [| |e] => //.
move: e => /eqP EQ; rewrite -dvdn_eq in EQ.
by rewrite EQ in Mm.
Qed.
@@ -135,7 +135,7 @@ Section DivFloorCeil.
T > 0 -> Δ >= T ->
div_ceil (Δ - T) T < div_ceil Δ T.
Proof.
- intros * POS LE. rewrite /div_ceil.
+ move=> Δ T POS LE. rewrite /div_ceil.
have lkc: (Δ - T) %/ T < Δ %/ T.
{ rewrite divnBr; last by auto.
rewrite divnn POS.
@@ -194,7 +194,7 @@ Section DivFloorCeil.
b > 0 ->
a < a %/ b * b + b.
Proof.
- intros * POS.
+ move=> a b POS.
specialize (divn_eq a b) => DIV.
rewrite [in X in X < _]DIV.
rewrite ltn_add2l.
@@ -209,7 +209,7 @@ Section DivFloorCeil.
c > b ->
(a + c - b) %% c = if a %% c >= b then (a %% c - b) else (a %% c + c - b).
Proof.
- intros * BC.
+ move=> a b c BC.
have POS : c > 0 by lia.
have G : a %% c < c by apply ltn_pmod.
case (b <= a %% c) eqn:CASE; rewrite -addnBA; auto; rewrite -modnDml.
diff --git a/util/lcmseq.v b/util/lcmseq.v
index a5e7309769f4c2c42a809543886f48c8d246bb2d..8c577cd9af2e9da117dbd0e69fef0d8b9694db96 100644
--- a/util/lcmseq.v
+++ b/util/lcmseq.v
@@ -9,7 +9,7 @@ Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.
Lemma int_divides_lcm_in_seq:
forall (x : nat) (xs : seq nat), x %| lcml (x :: xs).
Proof.
- induction xs.
+ move=> x xs; induction xs.
- by apply dvdn_lcml.
- rewrite /lcml -cat1s foldr_cat /foldr.
by apply dvdn_lcml.
@@ -20,7 +20,7 @@ Lemma lcm_seq_divides_lcm_super:
forall (x : nat) (xs : seq nat),
lcml xs %| lcml (x :: xs).
Proof.
- induction xs; first by auto.
+ move=> x xs; induction xs; first by auto.
rewrite /lcml -cat1s foldr_cat /foldr.
by apply dvdn_lcmr.
Qed.
@@ -48,8 +48,7 @@ Lemma all_pos_implies_lcml_pos:
(forall x, x \in xs -> x > 0) ->
lcml xs > 0.
Proof.
- intros * POS.
- induction xs; first by easy.
+ elim=> [//|x xs IHxs] POS.
rewrite /lcml -cat1s //= lcmn_gt0.
apply/andP; split => //.
- by apply POS; rewrite in_cons eq_refl.
diff --git a/util/list.v b/util/list.v
index 0bc7957115c70ef0cad4a2d3cc4efd0eb8897755..dde492e290bf59551aef0d73c0fe3c217ed91eed 100644
--- a/util/list.v
+++ b/util/list.v
@@ -19,9 +19,7 @@ Section Last0.
forall x xs,
xs <> [::] ->
last0 (x::xs) = last0 xs.
- Proof.
- by induction xs; last unfold last0.
- Qed.
+ Proof. by move=> x; elim. Qed.
(** Similarly, let [xs_r] be a non-empty sequence and [xs_l] be any sequence,
we prove that [last0 (xs_l ++ xs_r) = last0 xs_r]. *)
@@ -30,7 +28,7 @@ Section Last0.
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r.
Proof.
- induction xs_l; intros ? NEQ; first by done.
+ elim=> [//|xs xs_l IHxs_l] n NEQ.
simpl; rewrite last0_cons.
- by apply IHxs_l.
- by intros C; apply: NEQ; destruct xs_l.
@@ -50,10 +48,9 @@ Section Last0.
last0 xs = x ->
exists xsh, xsh ++ [::x] = xs.
Proof.
- intros ? ? NEQ LAST.
- induction xs; first by done.
+ move=> x; elim=> [//|a xs IHxs] NEQ LAST.
destruct xs.
- - exists [::]; by compute in LAST; subst a.
+ - by exists [::]; move: LAST; rewrite /last0 /= => ->.
- feed_n 2 IHxs; try by done.
destruct IHxs as [xsh EQ].
by exists (a::xsh); rewrite //= EQ.
@@ -69,7 +66,7 @@ Section Last0.
P x ->
last0 [seq x <- xs | P x] = x.
Proof.
- clear; intros ? ? ? NEQ LAST PX.
+ clear; intros x xs P NEQ LAST PX.
destruct (last0_ex_cat x xs NEQ LAST) as [xsh EQ]; subst xs.
rewrite filter_cat last0_cat.
all:rewrite //= PX //=.
@@ -82,14 +79,7 @@ Section Max0.
(** First we prove that [max0 (x::xs)] is equal to [max {x, max0 xs}]. *)
Lemma max0_cons : forall x xs, max0 (x :: xs) = maxn x (max0 xs).
- Proof.
- have L: forall xs s x, foldl maxn s (x::xs) = maxn x (foldl maxn s xs).
- { induction xs; intros.
- - by rewrite maxnC.
- - by rewrite //= in IHxs; rewrite //= maxnC IHxs [maxn s a]maxnC IHxs maxnA [maxn s x]maxnC.
- }
- by intros; unfold max; apply L.
- Qed.
+ Proof. by move=> x xs; rewrite /max0 !foldlE /= !big_cons maxnCA. Qed.
(** Next, we prove that if all the numbers of a seq [xs] are equal
to a constant [k], then [max0 xs = k]. *)
@@ -99,15 +89,14 @@ Section Max0.
(forall x, x \in xs -> x = k) ->
max0 xs = k.
Proof.
- intros ? ? SIZE ALL.
- induction xs; first by done.
- destruct xs.
+ move=> k; elim=> [//|a xs IHxs] SIZE ALL.
+ destruct xs as [|b xs].
- rewrite /max0 //= max0n; apply ALL.
by rewrite in_cons; apply/orP; left.
- rewrite max0_cons IHxs; [ | by done | ].
+ by rewrite [a]ALL; [ rewrite maxnn | rewrite in_cons; apply/orP; left].
- + intros; apply ALL.
- move: H; rewrite in_cons; move => /orP [/eqP EQ | IN].
+ + move=> x H; apply ALL.
+ rewrite in_cons; move: H => /orP [/eqP EQ | IN].
* by subst x; rewrite !in_cons; apply/orP; right; apply/orP; left.
* by rewrite !in_cons; apply/orP; right; apply/orP; right.
Qed.
@@ -116,8 +105,8 @@ Section Max0.
Lemma in_max0_le :
forall xs x, x \in xs -> x <= max0 xs.
Proof.
- induction xs; first by intros ?.
- intros x; rewrite in_cons; move => /orP [/eqP EQ | IN]; subst.
+ elim=> [//|a xs IHxs] x.
+ rewrite in_cons; move => /orP [/eqP EQ | IN]; subst.
- by rewrite !max0_cons leq_maxl.
- apply leq_trans with (max0 xs); first by eauto.
by rewrite max0_cons; apply leq_maxr.
@@ -129,8 +118,8 @@ Section Max0.
xs <> [::] ->
max0 xs \in xs.
Proof.
- induction xs; first by done.
- intros _; destruct xs.
+ elim=> [//|a xs IHxs] _.
+ destruct xs as [|n xs].
- destruct a; simpl; first by done.
by rewrite /max0 //= max0n in_cons eq_refl.
- rewrite max0_cons.
@@ -154,7 +143,9 @@ Section Max0.
forall x1 x2 xs,
x1 <= x2 ->
max0 (x1::x2::xs) = max0 (x2::xs).
- Proof. by intros; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC. Qed.
+ Proof.
+ by move=> x1 x2 ? ?; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC.
+ Qed.
(** We prove that [max0] of a sequence [xs]
is equal to [max0] of sequence [xs] without 0s. *)
@@ -162,7 +153,7 @@ Section Max0.
forall xs,
max0 ([seq x <- xs | 0 < x]) = max0 xs.
Proof.
- induction xs; first by done.
+ elim=> [//|a xs IHxs].
simpl; destruct a; simpl.
- by rewrite max0_cons max0n.
- by rewrite !max0_cons IHxs.
@@ -176,10 +167,9 @@ Section Max0.
have EX: exists len, size xs <= len.
{ by exists (size xs). }
move: EX => [len LE].
- generalize dependent xs; induction len.
+ generalize dependent xs; elim: len => [|n IHlen] xs LE.
- by intros; move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
- - intros ? SIZE.
- move: SIZE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.
+ - move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.
destruct xs as [ | x1 xs]; first by inversion EQ.
destruct xs as [ | x2 xs]; first by rewrite /max leq_max; apply/orP; right.
have ->: last0 [:: x1, x2 & xs] = last0 [:: x2 & xs] by done.
@@ -206,21 +196,20 @@ Section Max0.
}
move: EX => [len [LE1 LE2]].
generalize dependent xs; generalize dependent ys.
- induction len; intros.
+ elim: len => [ | len IHlen] xs LE1 ys LE2.
{ by move: LE1 LE2; rewrite !leqn0 !size_eq0; move => /eqP E1 /eqP E2; subst. }
- { destruct xs, ys; try done.
+ { move: xs ys LE1 LE2 => [ |x xs] [//|y ys] LE1 LE2 H.
{ have L: forall xs, (forall n, xs [| n |] = 0) -> max0 xs = 0.
- { clear; intros.
- induction xs; first by done.
+ { clear; elim=> [//|x xs IHxs] H.
rewrite max0_cons.
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
rewrite geq_max; apply/andP; split.
- by specialize (H 0); simpl in H; rewrite H.
- rewrite leqn0; apply/eqP; apply: IHxs.
- by intros; specialize (H n.+1); simpl in H.
+ by move=> n; specialize (H n.+1); simpl in H.
}
rewrite L; first by done.
- intros; specialize (H n0).
+ move=> n0; specialize (H n0).
by destruct n0; simpl in *; apply/eqP; rewrite -leqn0.
}
{ rewrite !max0_cons geq_max; apply/andP; split.
@@ -228,7 +217,7 @@ Section Max0.
by specialize (H 0); simpl in H.
+ rewrite leq_max; apply/orP; right.
apply IHlen; try (by rewrite ltnS in LE1, LE2).
- by intros; specialize (H n1.+1); simpl in H.
+ by move=> n1; specialize (H n1.+1); simpl in H.
}
}
Qed.
@@ -244,10 +233,10 @@ Section RemList.
forall {X : eqType} (x y : X) (xs : seq X),
x \in rem y xs -> x \in xs.
Proof.
- intros; induction xs; simpl in H.
+ move=> X x y; elim=> [|a xs IHxs] /= H.
{ by rewrite in_nil in H. }
{ rewrite in_cons; apply/orP.
- destruct (a == y) eqn:EQ.
+ destruct (a == y) eqn:EQ.
{ by move: EQ => /eqP EQ; subst a; right. }
{ move: H; rewrite in_cons; move => /orP [/eqP H | H].
- by subst a; left.
@@ -255,7 +244,7 @@ Section RemList.
}
}
Qed.
-
+
(** Similarly, we prove that if [x <> y] and [x] lies in [xs],
then [x] lies in [xs] excluding [y]. *)
Lemma in_neq_impl_rem_in :
@@ -264,20 +253,18 @@ Section RemList.
x != y ->
x \in rem y xs.
Proof.
- induction xs.
- { intros ?; by done. }
- { rewrite in_cons => /orP [/eqP EQ | IN]; intros NEQ.
- { rewrite -EQ //=.
- move: NEQ; rewrite -eqbF_neg => /eqP ->.
- by rewrite in_cons; apply/orP; left.
- }
- { simpl; destruct (a == y) eqn:AD; first by done.
- rewrite in_cons; apply/orP; right.
- by apply IHxs.
- }
+ move=> X x y; elim=> [//|a xs IHxs].
+ rewrite in_cons => /orP [/eqP EQ | IN]; intros NEQ.
+ { rewrite -EQ //=.
+ move: NEQ; rewrite -eqbF_neg => /eqP ->.
+ by rewrite in_cons; apply/orP; left.
+ }
+ { simpl; destruct (a == y) eqn:AD; first by done.
+ rewrite in_cons; apply/orP; right.
+ by apply IHxs.
}
Qed.
-
+
(** We prove that if we remove an element [x] for which [P x] from a
filter, then the size of the filter decreases by [1]. *)
Lemma filter_size_rem :
@@ -286,7 +273,7 @@ Section RemList.
P x ->
size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.
Proof.
- intros; induction xs; first by inversion H.
+ move=> X x + P + H0; elim=> [|a xs IHxs] H; first by inversion H.
move: H; rewrite in_cons; move => /orP [/eqP H | H]; subst.
{ by simpl; rewrite H0 -[X in X = _]addn1 eq_refl. }
{ specialize (IHxs H); simpl in *.
@@ -322,7 +309,7 @@ Section AdditionalLemmas.
forall x xs n,
n > 0 ->
nth 0 (x :: xs) n = nth 0 xs n.-1.
- Proof. by intros; destruct n. Qed.
+ Proof. by move=> ? ? []. Qed.
(** We prove that a sequence [xs] of size [n.+1] can be destructed
into a sequence [xs_l] of size [n] and an element [x] such that
@@ -332,12 +319,12 @@ Section AdditionalLemmas.
size xs = n.+1 ->
exists x xs__c, xs = xs__c ++ [:: x] /\ size xs__c = n.
Proof.
- intros ? ? ? SIZE.
- revert xs SIZE; induction n; intros.
- - destruct xs; first by done.
+ intros X n xs SIZE.
+ elim: n xs SIZE => [|n IHn] xs SIZE.
+ - destruct xs as [|x xs]; first by done.
destruct xs; last by done.
by exists x, [::]; split.
- - destruct xs; first by done.
+ - destruct xs as [|x xs]; first by done.
specialize (IHn xs).
feed IHn; first by simpl in SIZE; apply eq_add_S in SIZE.
destruct IHn as [x__n [xs__n [EQ__n SIZE__n]]]; subst xs.
@@ -346,22 +333,21 @@ Section AdditionalLemmas.
rewrite size_cat //= in SIZE; rewrite addn1 in SIZE; apply eq_add_S in SIZE.
by apply eq_S.
Qed.
-
+
(** Next, we prove that [x ∈ xs] implies that [xs] can be split
into two parts such that [xs = xsl ++ [::x] ++ [xsr]]. *)
Lemma in_cat :
forall {X : eqType} (x : X) (xs : list X),
x \in xs -> exists xsl xsr, xs = xsl ++ [::x] ++ xsr.
Proof.
- intros ? ? ? SUB.
- induction xs; first by done.
+ move=> X x; elim=> [//|a xs IHxs] SUB.
move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
- by subst; exists [::], xs.
- feed IHxs; first by done.
clear IN; move: IHxs => [xsl [xsr EQ]].
by subst; exists (a::xsl), xsr.
- Qed.
-
+ Qed.
+
(** We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence
of [ys] implies that the size of [xs] is at most the size of [ys]. *)
Lemma subseq_leq_size :
@@ -370,13 +356,13 @@ Section AdditionalLemmas.
(forall x, x \in xs -> x \in ys) ->
size xs <= size ys.
Proof.
- intros ? ? ? UNIQ SUB.
+ intros X xs ys UNIQ SUB.
have EXm: exists m, size ys <= m; first by exists (size ys).
move: EXm => [m SIZEm].
move: xs ys SIZEm UNIQ SUB.
- induction m; intros.
+ elim: m => [|m IHm] xs ys SIZEm UNIQ SUB.
{ move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
- destruct xs; first by done.
+ destruct xs as [|s xs]; first by done.
specialize (SUB s).
by feed SUB; [rewrite in_cons; apply/orP; left | done].
}
@@ -413,7 +399,8 @@ Section AdditionalLemmas.
(exists idx, idx < size xs /\ nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys.
Proof.
- induction xs as [ | x1 xs]; intros * EQ [idx [LT [NTHx NTHy]]]; first by done.
+ move=> X Y xs ys x x__d y y__d.
+ elim: xs ys => [|x1 xs IHxs] ys EQ [idx [LT [NTHx NTHy]]] //.
destruct ys as [ | y1 ys]; first by done.
rewrite //= in_cons; apply/orP.
destruct idx as [ | idx]; [left | right].
@@ -434,7 +421,7 @@ Section AdditionalLemmas.
(exists ys, size xs = size ys /\ all P_bool (zip xs ys) == true) ->
(forall x, x \in xs -> exists y, P_prop x y).
Proof.
- intros * EQ TR x IN.
+ move=> X Y P_bool P_prop xs EQ TR x IN.
destruct TR as [ys [SIZE ALL]].
set (idx := index x xs).
have x__d : Y by destruct xs, ys.
@@ -458,11 +445,11 @@ Section AdditionalLemmas.
(forall x, x \in xs -> x \in ys) ->
(forall x, x \in ys -> x \in xs).
Proof.
- intros ? ? ? UNIQ SUB.
+ intros X xs ys UNIQ SUB.
have EXm: exists m, size ys <= m; first by exists (size ys).
move: EXm => [m SIZEm].
move: SIZEm UNIQ SUB; move: xs ys.
- induction m; intros ? ? SIZEm UNIQx UNIQy EQ SUB a IN.
+ elim: m => [|m IHm] xs ys SIZEm UNIQx UNIQy EQ SUB a IN.
{ by move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys. }
{ destruct xs as [ | x xs].
{ by move: EQ; simpl => /eqP; rewrite eq_sym size_eq0 => /eqP EQ; subst ys. }
@@ -486,7 +473,7 @@ Section AdditionalLemmas.
}
}
Qed.
-
+
(** We prove that if no element of a sequence [xs] satisfies a
predicate [P], then [filter P xs] is equal to an empty
sequence. *)
@@ -495,8 +482,7 @@ Section AdditionalLemmas.
(forall x, x \in xs -> ~~ P x) ->
filter P xs = [::].
Proof.
- intros * ALLF.
- induction xs; first by done.
+ move=> X xs P; elim: xs => [//|a xs IHxs] ALLF.
rewrite //= IHxs; last first.
+ by intros; apply ALLF; rewrite in_cons; apply/orP; right.
+ destruct (P a) eqn:EQ; last by done.
@@ -526,7 +512,7 @@ Section AdditionalLemmas.
forall {X : eqType} (n : nat) (d : X) (xs : seq X),
nth d xs n = d \/ nth d xs n \in xs.
Proof.
- intros; destruct (leqP (size xs) n).
+ move=> x n d xs; destruct (leqP (size xs) n).
- by left; apply nth_default.
- by right; apply mem_nth.
Qed.
@@ -543,7 +529,7 @@ Section AdditionalLemmas.
(* get an element of [T] so that we can use nth *)
have HEAD: exists x, ohead xs = Some x by elim: xs GT1 UNIQ => // a l _ _ _; exists a => //.
move: (HEAD) => [x0 _].
- have GT0: 0 < size xs by apply ltn_trans with (n := 1).
+ have GT0 : 0 < size xs by exact: ltn_trans GT1.
exists (nth x0 xs 0).
exists (nth x0 xs 1).
repeat split; try apply mem_nth => //.
@@ -577,13 +563,13 @@ Section Sorted.
sorted (fun x y => f x <= f y) xs ->
[seq x <- xs | P x] = [seq x <- xs | P x & f x <= t] ++ [seq x <- xs | P x & f x > t].
Proof.
- clear; induction xs; intros * SORT; simpl in *; first by done.
+ clear; move=> X xs P f t; elim: xs => [//|a xs IHxs] /= SORT.
have TR : transitive (T:=X) (fun x y : X => f x <= f y).
{ intros ? ? ? LE1 LE2; lia. }
destruct (P a) eqn:Pa, (leqP (f a) t) as [R1 | R1]; simpl.
{ erewrite IHxs; first by reflexivity.
by eapply path_sorted; eauto. }
- { erewrite (IHxs P f t); last by eapply path_sorted; eauto.
+ { erewrite IHxs; last by eapply path_sorted; eauto.
replace ([seq x <- xs | P x & f x <= t]) with (@nil X); first by done.
symmetry; move: SORT; rewrite path_sortedE // => /andP [ALL SORT].
apply filter_in_pred0; intros ? IN; apply/negP; intros H; move: H => /andP [Px LEx].
@@ -600,15 +586,16 @@ Section Sorted.
transitive R ->
sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2.
Proof.
- induction xs1; intros ? TR SORT; split; try by done.
- { simpl in *; move: SORT; rewrite //= path_sortedE // all_cat => /andP [/andP [ALL1 ALL2] SORT].
- by rewrite //= path_sortedE //; apply/andP; split; last apply IHxs1 with (xs2 := xs2).
+ move=> X R; elim=> [//|a xs1 IHxs1] xs2 TR SORT; split.
+ { move: SORT; rewrite /= path_sortedE// all_cat => /andP[/andP[ALL1 ALL2] SORT].
+ rewrite path_sortedE//; apply/andP; split=> //.
+ exact: (proj1 (IHxs1 _ _ SORT)).
}
{ simpl in *; move: SORT; rewrite //= path_sortedE // all_cat => /andP [/andP [ALL1 ALL2] SORT].
by apply IHxs1.
}
Qed.
-
+
End Sorted.
(** Additional lemmas about [last]. *)
@@ -620,10 +607,7 @@ Section Last.
forall {X : eqType} (xs : seq X) (d1 d2 : X),
xs != [::] ->
last d1 xs = last d2 xs.
- Proof.
- induction xs; first by done.
- by intros * _; destruct xs.
- Qed.
+ Proof. by move=> X xs d1 d2; elim: xs => [//|a xs IHxs] _. Qed.
(** We show that if a sequence [xs] contains an element that
satisfies a predicate [P], then the last element of [filter P xs]
@@ -633,8 +617,8 @@ Section Last.
has P xs ->
last d (filter P xs) \in xs.
Proof.
- induction xs; first by done.
- move => d P /hasP [x IN Px]; move: IN; rewrite in_cons => /orP [/eqP EQ | IN].
+ move=> X; elim=> [//|a xs IHxs] d P /hasP [x + Px].
+ rewrite in_cons => /orP [/eqP EQ | IN].
{ simpl; subst a; rewrite Px; simpl.
destruct (has P xs) eqn:HAS.
{ by rewrite in_cons; apply/orP; right; apply IHxs. }
@@ -649,7 +633,7 @@ Section Last.
all: by apply/hasP; exists x.
}
Qed.
-
+
End Last.
@@ -672,8 +656,7 @@ Section RemAllList.
forall {X : eqType} (x : X) (xs : seq X),
~ (x \in rem_all x xs).
Proof.
- intros ? ? ? IN.
- induction xs; first by done.
+ move=> X x; elim=> [//|a xs IHxs] IN.
apply: IHxs.
simpl in IN; destruct (a == x) eqn:EQ; first by done.
move: IN; rewrite in_cons; move => /orP [/eqP EQ2 | IN]; last by done.
@@ -685,9 +668,7 @@ Section RemAllList.
forall {X : eqType} (a x : X) (xs : seq X),
a \in rem_all x xs -> a \in xs.
Proof.
- intros X a x xs IN.
- induction xs; first by done.
- simpl in IN.
+ intros X a x; elim=> [//|a0 xs IHxs] /= IN.
destruct (a0 == x) eqn:EQ.
- by rewrite in_cons; apply/orP; right; eauto.
- move: IN; rewrite in_cons; move => /orP [EQ2|IN].
@@ -702,8 +683,8 @@ Section RemAllList.
(forall y, y \in xs -> x < y) ->
rem_all x xs = xs.
Proof.
- intros ? ? MIN; induction xs; first by done.
- simpl; have -> : (a == x) = false.
+ move=> x; elim=> [//|a xs IHxs] MIN /=.
+ have -> : (a == x) = false.
{ apply/eqP/eqP; rewrite neq_ltn; apply/orP; right.
by apply MIN; rewrite in_cons; apply/orP; left.
}
@@ -728,10 +709,9 @@ Section IotaRange.
n_le <= n ->
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le).
Proof.
- intros * LE.
+ move=> n_le m n LE.
interval_to_duration n_le n k.
- rewrite iotaD.
- by replace (_ + _ - _) with k; last lia.
+ by rewrite iotaD; replace (_ + _ - _) with k; last lia.
Qed.
(** Next, we prove that [index_iota a b = a :: index_iota a.+1 b]
@@ -741,10 +721,10 @@ Section IotaRange.
a < b ->
index_iota a b = a :: index_iota a.+1 b.
Proof.
- intros ? ? LT; unfold index_iota.
+ move=> a b LT; unfold index_iota.
destruct b; first by done.
rewrite ltnS in LT.
- by rewrite subSn //.
+ by rewrite subSn //.
Qed.
(** We prove that one can remove duplicating element from the
@@ -754,10 +734,8 @@ Section IotaRange.
[seq Ï <- range 0 k | Ï \in x :: x :: xs] =
[seq Ï <- range 0 k | Ï \in x :: xs].
Proof.
- intros.
- apply eq_filter; intros ?.
- repeat rewrite in_cons.
- by destruct (x0 == x), (x0 \in xs).
+ move=> x xs k; apply: eq_filter => x0.
+ by rewrite !in_cons; destruct (x0 == x), (x0 \in xs).
Qed.
(** Consider [a], [b], and [x] s.t. [a ≤ x < b],
@@ -768,13 +746,13 @@ Section IotaRange.
a <= x < b ->
[seq Ï <- index_iota a b | Ï == x] = [::x].
Proof.
- intros ? ? ?.
+ move=> x a b.
have EX : exists k, b - a <= k.
{ exists (b-a); by simpl. }
destruct EX as [k BO].
- revert x a b BO; induction k; move => x a b BO /andP [GE LT].
+ revert x a b BO; elim: k => [|k IHk] => x a b BO /andP [GE LT].
{ by exfalso; move: BO; rewrite leqn0 subn_eq0; move => BO; lia. }
- { destruct a.
+ { destruct a as [|a].
{ destruct b; first by done.
rewrite index_iota_lt_step //; simpl.
destruct (0 == x) eqn:EQ.
@@ -792,7 +770,7 @@ Section IotaRange.
- by rewrite IHk //; lia.
}
Qed.
-
+
(** As a corollary we prove that filter of [iota_index a b]
with predicate [(_ ∈ [::x])] yields [::x]. *)
Corollary index_iota_filter_singl :
@@ -800,7 +778,7 @@ Section IotaRange.
a <= x < b ->
[seq Ï <- index_iota a b | Ï \in [:: x]] = [::x].
Proof.
- intros ? ? ? NEQ.
+ move=> x a b NEQ.
rewrite -{2}(index_iota_filter_eqx _ a b) //.
apply eq_filter; intros ?.
by repeat rewrite in_cons; rewrite in_nil Bool.orb_false_r.
@@ -819,13 +797,13 @@ Section IotaRange.
intros a b x xs LT.
apply eq_in_filter.
intros y; rewrite mem_index_iota; move => /andP [LE GT].
- induction xs as [ | y' xs]; first by done.
+ elim: xs => [//|y' xs IHxs].
rewrite in_cons IHxs; simpl; clear IHxs.
destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.
- by exfalso; move: EQ1 EQ2 => /eqP EQ1 /eqP EQ2; subst; lia.
- by move: EQ1 => /eqP EQ1; subst; rewrite in_cons eq_refl.
- by rewrite in_cons EQ1.
- Qed.
+ Qed.
(** We prove that if an element [x] is a min of a sequence [xs],
then [iota_index a b] filtered with predicate [(_ ∈ x::xs)] is
@@ -842,7 +820,7 @@ Section IotaRange.
have EX : exists k, b - a <= k.
{ exists (b-a); by simpl. } destruct EX as [k BO].
revert x xs a b B MIN BO.
- induction k; move => x xs a b /andP [LE GT] MIN BO.
+ elim: k => [ |k IHk] x xs a b /andP [LE GT] MIN BO.
- by move_neq_down BO; lia.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
+ subst.
@@ -897,10 +875,10 @@ Section IotaRange.
idx < size ([seq x <- index_iota a b | P x]) ->
x < nth 0 [seq x <- index_iota a b | P x] idx.
Proof.
- clear; intros ? ? ? ? ?.
+ clear=> x a b idx P.
have EX : exists k, b - a <= k.
{ exists (b-a); by simpl. } destruct EX as [k BO].
- revert x a b idx P BO; induction k.
+ revert x a b idx P BO; elim: k => [|k IHk].
- move => x a b idx P BO LT1 LT2.
move: BO; rewrite leqn0; move => /eqP BO.
by rewrite /index_iota BO in LT2; simpl in LT2.
@@ -916,7 +894,7 @@ Section IotaRange.
* apply IHk; try lia.
by rewrite index_iota_lt_step // //= PA //= in LT2.
Qed.
-
+
End IotaRange.
(** A sequence [xs] is a prefix of another sequence [ys] iff
diff --git a/util/minmax.v b/util/minmax.v
index e6f975189bf5a3a3da23dac70dd329276ec5f13e..cef2860f20f9a211523a1423be77559d95ee5fd1 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -10,7 +10,7 @@ Section ExtraLemmas.
Lemma leq_bigmax_cond_seq :
forall {X : eqType} (F : X -> nat) (P : pred X) (xs : seq X) (x : X),
x \in xs -> P x -> F x <= \max_(i <- xs | P i) F i.
- Proof. by intros * IN Px; rewrite (big_rem x) //= Px leq_maxl. Qed.
+ Proof. by move=> X F P xs x IN Px; rewrite (big_rem x) //= Px leq_maxl. Qed.
(** Next, we show that the fact [max { F i | ∀ i ∈ xs, P i} <= m] for
some [m] is equivalent to the fact that [∀ x ∈ xs, P x -> F x <= m]. *)
@@ -36,7 +36,7 @@ Section ExtraLemmas.
(forall x, x \in xs -> P x -> F1 x <= F2 x) ->
\max_(x <- xs | P x) F1 x <= \max_(x <- xs | P x) F2 x.
Proof.
- intros * ALL; apply /bigmax_leq_seqP; intros * IN Px.
+ move=> X F1 F2 P xs ALL; apply /bigmax_leq_seqP => x IN Px.
specialize (ALL x); feed_n 2 ALL; try done.
rewrite (big_rem x) //=; rewrite Px.
by apply leq_trans with (F2 x); [ | rewrite leq_maxl].
@@ -50,9 +50,9 @@ Section ExtraLemmas.
\max_(i < n) i < n.
Proof.
intros [ | n] POS; first by rewrite ltn0 in POS.
- clear POS; induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
- rewrite big_ord_recr /=.
- by rewrite /maxn IHn.
+ clear POS.
+ elim: n => [|n IHn]; first by rewrite big_ord_recr /= big_ord0 maxn0.
+ by rewrite big_ord_recr /= /maxn IHn.
Qed.
(** We state the next lemma in terms of _ordinals_. Given a natural
@@ -66,10 +66,10 @@ Section ExtraLemmas.
\max_(i < n | P i) i < n.
Proof.
intros n P i0 Pi.
- destruct n; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
+ destruct n as [|n]; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
rewrite big_mkcond.
apply leq_ltn_trans with (n := \max_(i < n.+1) i).
- - apply/bigmax_leqP; ins.
+ - apply/bigmax_leqP => i _.
destruct (P i); last by done.
by apply leq_bigmax_cond.
- by apply bigmax_ord_ltn_identity.
@@ -83,12 +83,12 @@ Section ExtraLemmas.
P i0 ->
P (\max_(i < n | P i) i).
Proof.
- intros * Pi0.
- induction n.
+ intros n P i0 Pi0.
+ elim: n i0 Pi0 => [|n IHn] i0 Pi0.
{ by destruct i0 as [i0 P0]; move: (P0) => P1; rewrite ltn0 in P1. }
{ rewrite big_mkcond big_ord_recr /=.
destruct (P n) eqn:Pn.
- { destruct n; first by rewrite big_ord0 maxn0.
+ { destruct n as [|n]; first by rewrite big_ord0 maxn0.
unfold maxn at 1.
destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
| true => @nat_of_ord (S n) i
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 5cb772d091fb071e8e973cbc6c33d72eb2862c78..7e34d0835e78d0cba24b5bec0f730ff1eddcaefb 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -47,10 +47,10 @@ Section NondecreasingSequence.
forall a b P,
increasing_sequence [seq x <- index_iota a b | P x].
Proof.
- clear; intros ? ? ?.
+ clear=> a b P.
have EX : exists k, b - a <= k.
{ by exists (b-a). } destruct EX as [k BO].
- revert a b P BO; induction k.
+ revert a b P BO; elim: k => [ |k IHk].
{ move => a b P BO n1 n2.
move: BO; rewrite leqn0; move => /eqP BO.
rewrite /index_iota BO; simpl.
@@ -101,6 +101,7 @@ Section NondecreasingSequence.
nondecreasing_sequence xs ->
first0 xs = 0.
Proof.
+ move=> xs.
destruct xs as [ | x xs]; first by done.
destruct x as [ | x]; first by done.
rewrite in_cons; move => /orP [/eqP EQ | IN] ND; first by done.
@@ -112,7 +113,7 @@ Section NondecreasingSequence.
by simpl; rewrite ltnS index_mem. }
by simpl in ND; rewrite NTH in ND.
Qed.
-
+
(** If [x1::x2::xs] is a non-decreasing sequence, then either
[x1 = x2] or [x1 < x2]. *)
Lemma nondecreasing_sequence_2cons_leVeq:
@@ -120,12 +121,12 @@ Section NondecreasingSequence.
nondecreasing_sequence (x1 :: x2 :: xs) ->
x1 = x2 \/ x1 < x2.
Proof.
- intros ? ? ? ND.
+ move=> x1 x2 xs ND.
destruct (ltngtP x1 x2) as [LT | GT | EQ]; auto.
move_neq_down GT.
by specialize (ND 0 1); apply ND.
Qed.
-
+
(** We prove that if [x::xs] is a non-decreasing sequence,
then [xs] also is a non-decreasing sequence. *)
Lemma nondecreasing_sequence_cons:
@@ -185,7 +186,7 @@ Section NondecreasingSequence.
nondecreasing_sequence (x :: xs) ->
(forall y, y \in xs -> x <= y).
Proof.
- intros ? ? ND ? IN.
+ intros x xs ND y IN.
have IDX := nth_index 0 IN.
specialize (ND 0 (index y xs).+1).
move: (IN) => IDL; rewrite -index_mem in IDL.
@@ -217,10 +218,7 @@ Section NondecreasingSequence.
xs[|n|] < x < xs[|n.+1|] ->
~~ (x \in xs).
Proof.
- intros ? ? ? STR ?; apply/negP; intros ?.
- move: H0 => /nthP. intros GG.
- specialize (GG 0).
- move: GG => [ind LE HHH].
+ move=> xs x n STR H; apply/negP => /nthP => /(_ 0) [ind LE HHH].
subst x; rename ind into x.
destruct (n.+1 < size xs) eqn:Bt; last first.
{ move: Bt => /negP /negP; rewrite -leqNgt; move => Bt.
@@ -249,7 +247,7 @@ Section NondecreasingSequence.
}
by move: LT; rewrite ltnNge; move => /negP LT; apply: LT.
Qed.
-
+
(** Alternatively, consider an arbitrary natural number x that is
bounded by the first and the last element of a sequence
[xs]. Then there is an index n such that [xs[n] <= x < x[n+1]]. *)
@@ -261,15 +259,15 @@ Section NondecreasingSequence.
n.+1 < size xs /\
xs[|n|] <= x < xs[|n.+1|].
Proof.
- intros ? ? SIZE LAST.
+ move=> xs x SIZE LAST.
have EX: exists n, size xs <= n by exists (size xs). move: EX => [n LE].
- destruct n; first by destruct xs.
- destruct n; first by destruct xs; last destruct xs.
+ destruct n as [ |n]; first by destruct xs.
+ destruct n as [ |n]; first by destruct xs as [ |? xs]; last destruct xs.
generalize dependent xs.
- induction n; intros.
- { by destruct xs; [ | destruct xs; [ | destruct xs; [exists 0 | ] ] ]. }
- { destruct xs; [ | destruct xs; [ | ]]; try by done.
- destruct xs; first by (exists 0).
+ elim: n => [ |n IHn] xs SIZE LAST LE.
+ { by destruct xs as [ |? xs]; [ | destruct xs as [ |? xs]; [ | destruct xs; [exists 0 | ] ] ]. }
+ { destruct xs as [ |n0 xs]; [ | destruct xs as [ |n1 xs]; [ | ]]; try by done.
+ destruct xs as [ |n2 xs]; first by (exists 0).
destruct (leqP n1 x) as [NEQ|NEQ]; last first.
{ exists 0; split; auto. move: LAST => /andP [LAST _].
by apply/andP; split. }
@@ -297,9 +295,9 @@ Section NondecreasingSequence.
(x \in xs) ->
x <= last0 xs.
Proof.
- intros ? ? STR IN.
+ move=> xs x STR IN.
have NEQ: forall x y, x = y \/ x != y.
- { clear; intros.
+ { clear=> t x y.
destruct (x == y) eqn:EQ.
- by left; apply/eqP.
- by right.
@@ -319,7 +317,7 @@ Section NondecreasingSequence.
- by rewrite prednK.
}
Qed.
-
+
End NonDecreasingSequence.
(** * Properties of [Undup] of Non-Decreasing Sequence *)
@@ -331,7 +329,7 @@ Section NondecreasingSequence.
forall {X : eqType} (x : X) (xs : seq X),
undup (x::x::xs) = undup (x::xs).
Proof.
- intros; rewrite {2 3}[cons] lock //= -lock.
+ move=> X x xs; rewrite {2 3}[cons] lock //= -lock.
rewrite in_cons eq_refl; simpl.
by destruct (x \in xs).
Qed.
@@ -344,7 +342,7 @@ Section NondecreasingSequence.
nondecreasing_sequence (x1::x2::xs) ->
undup (x1::x2::xs) = x1 :: undup (x2::xs).
Proof.
- intros; rewrite {2 3 4}[cons] lock //= -lock.
+ move=> x1 x2 xs H H0; rewrite {2 3 4}[cons] lock //= -lock.
rewrite in_cons.
have -> : (x1 == x2) = false.
{ by apply/eqP/eqP; rewrite neq_ltn; rewrite H. }
@@ -363,7 +361,7 @@ Section NondecreasingSequence.
nondecreasing_sequence xs ->
last0 (undup xs) = last0 xs.
Proof.
- induction xs as [ | x1 xs]; first by done.
+ elim=> [//|x1 xs IHxs].
intros ND; destruct xs as [ |x2 xs]; first by done.
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ ND) as [EQ|LT].
+ subst; rename x2 into x.
@@ -372,7 +370,7 @@ Section NondecreasingSequence.
by eapply nondecreasing_sequence_cons; eauto 2.
+ rewrite nodup_sort_2cons_lt // last0_cons.
rewrite IHxs //; eauto using nondecreasing_sequence_cons.
- by intros ?; apply undup_nil in H.
+ by move/undup_nil.
Qed.
(** Non-decreasing sequence remains non-decreasing after application of [undup]. *)
@@ -381,10 +379,10 @@ Section NondecreasingSequence.
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs).
Proof.
- intros ?.
+ move=> xs.
have EX: exists len, size xs <= len.
{ by exists (size xs). } destruct EX as [n BO].
- revert xs BO; induction n.
+ revert xs BO; elim: n => [ |n IHn].
- by intros xs; rewrite leqn0 size_eq0; move => /eqP EQ; subst xs.
- intros [ |x1 [ | x2 xs]] Size NonDec; try done.
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].
@@ -392,12 +390,12 @@ Section NondecreasingSequence.
by rewrite nodup_sort_2cons_eq; apply IHn; eauto using nondecreasing_sequence_cons.
+ rewrite nodup_sort_2cons_lt //.
apply nondecreasing_sequence_add_min.
- intros ? ?.
+ move=> y H.
eapply nondecreasing_sequence_cons_min with (y := y) in NonDec; auto.
rewrite -mem_undup; eauto using nondecreasing_sequence_cons.
by apply IHn; eauto using nondecreasing_sequence_cons.
Qed.
-
+
(** We also show that the penultimate element of a sequence [undup xs]
is bounded by the penultimate element of sequence [xs]. *)
Lemma undup_nth_le:
@@ -406,16 +404,17 @@ Section NondecreasingSequence.
undup xs [| (size (undup xs)).-2 |] <= xs [| (size xs).-2 |].
Proof.
Opaque undup.
- intros ?.
+ move=> xs.
have EX: exists len, size xs <= len by (exists (size xs)).
destruct EX as [n BO].
- revert xs BO; induction n.
+ revert xs BO; elim: n => [ |n IHn].
- by intros xs; rewrite leqn0 size_eq0; move => /eqP EQ; subst xs.
- intros [ |x1 [ | x2 xs]] Size NonDec; try done.
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].
* subst; rename x2 into x.
rewrite nodup_sort_2cons_eq //.
- eapply leq_trans. apply IHn. by done. eapply nondecreasing_sequence_cons; eauto.
+ eapply leq_trans.
+ apply IHn. by done. eapply nondecreasing_sequence_cons; eauto.
destruct xs as [ | x1 xs]; first by done.
by rewrite [in X in _ <= X]nth0_cons //.
* rewrite nodup_sort_2cons_lt //; simpl.
@@ -425,11 +424,11 @@ Section NondecreasingSequence.
by apply NonDec; apply/andP; split; simpl.
-- rewrite nth0_cons //.
eapply leq_trans; first apply IHn; eauto using nondecreasing_sequence_cons.
- destruct xs.
+ destruct xs as [ |? xs].
++ by exfalso.
- ++ destruct xs; simpl in *; auto.
+ ++ by destruct xs.
Qed.
-
+
End Undup.
(** * Properties of Distances *)
@@ -452,13 +451,13 @@ Section NondecreasingSequence.
distances (xs ++ [:: a; b])
= distances (xs ++ [:: a]) ++ [:: b - a].
Proof.
- intros.
+ move=> a b xs.
have EX: exists n, size xs <= n by (exists (size xs)).
destruct EX as [n LE].
- revert xs LE; induction n; intros.
+ elim: n xs LE => [ |n IHn] xs LE.
- by move: LE; rewrite leqn0 size_eq0; move => /eqP LE; subst.
- - destruct xs as [ | x0]; first by unfold distances.
- destruct xs as [ | x1]; first by unfold distances.
+ - destruct xs as [ | x0 xs]; first by unfold distances.
+ destruct xs as [ | x1 xs]; first by unfold distances.
have -> : distances ([:: x0, x1 & xs] ++ [:: a; b]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b]).
{ by simpl; rewrite distances_unfold_2cons. }
rewrite IHn; last by simpl in *; rewrite -(leq_add2r 1) !addn1.
@@ -477,7 +476,7 @@ Section NondecreasingSequence.
intros x xs POS.
have EX: exists n, size xs <= n by (exists (size xs)).
destruct EX as [n LE].
- revert x xs LE POS; induction n; intros.
+ elim: n x xs LE POS => [ |n IHn] x xs LE POS.
- by move: LE; rewrite leqn0 size_eq0; move => /eqP LE; subst.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP LEN' | LE]; last first.
+ by rewrite ltnS in LE; apply IHn.
@@ -486,10 +485,7 @@ Section NondecreasingSequence.
rewrite -catA.
rewrite distances_unfold_2app_last.
destruct xs; first by done.
- rewrite IHn.
- * by rewrite /last0 last_cat.
- * by rewrite LEN.
- * by done.
+ by rewrite IHn // ?LEN // /last0 last_cat.
Qed.
(** We prove that the difference between any two neighboring elements is
@@ -503,14 +499,14 @@ Section NondecreasingSequence.
rewrite leq_eqVlt; apply/orP; left; apply/eqP.
have EX: exists n, size xs <= n by (exists (size xs)).
move: EX => [n LE]; move: xs id LE.
- induction n; intros.
+ elim: n => [ |n IHn] xs id LE.
{ move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
by rewrite !nth_default.
}
{ move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT]; last first.
{ by apply IHn; rewrite ltnS in LT. }
- destruct xs; first by done.
- destruct xs; first by destruct id; [simpl |rewrite !nth_default].
+ destruct xs as [ | n0 xs]; first by done.
+ destruct xs as [ | n1 xs]; first by destruct id; [simpl |rewrite !nth_default].
have ->: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].
{ by rewrite /distances //= drop0. }
destruct id; first by done.
@@ -518,7 +514,7 @@ Section NondecreasingSequence.
by move: EQ => /eqP; rewrite //= eqSS => /eqP EQ; rewrite -EQ.
}
{ have Lem: forall xs x, x \in xs -> x <= max0 xs.
- { clear; induction xs; intros ? IN; first by done.
+ { clear; elim=> [//|a xs IHxs] x IN.
rewrite max0_cons leq_max; apply/orP.
move: IN; rewrite in_cons; move => /orP [/eqP EQ| IN].
- by left; subst.
@@ -542,12 +538,12 @@ Section NondecreasingSequence.
intros xs.
have EX: exists len, size xs <= len by (exists (size xs)).
move: EX => [len LE]; move: xs LE.
- induction len; intros.
+ elim: len => [ |len IHlen] xs LE n.
{ by move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst; destruct n. }
move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.
destruct xs as [ | x1 xs]; first by done.
destruct xs as [ | x2 xs]; first by destruct n as [ | [ | ]].
- destruct n; first by done.
+ destruct n as [ |n]; first by done.
have ->: distances [:: x1, x2 & xs] [|n.+1|] = distances [::x2 & xs] [| n |].
{ have ->: distances [:: x1, x2 & xs] = (x2 - x1) :: distances [::x2 & xs]; last by done.
{ by rewrite /distances //= drop0. }
@@ -567,7 +563,7 @@ Section NondecreasingSequence.
intros xs.
have EX: exists len, size xs <= len by (exists (size xs)).
move: EX => [len LE]; move: xs LE.
- induction len; intros * LE SIZE.
+ elim: len => [ |len IHlen] xs LE SIZE.
{ by move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst. }
{ move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.
destruct xs as [ | x1 xs]; first by inversion EQ.
@@ -587,7 +583,7 @@ Section NondecreasingSequence.
Lemma distances_of_iota_ε:
forall n x, x \in distances (index_iota 0 n) -> x = ε.
Proof.
- intros n x IN; induction n.
+ move=> n x; elim: n => [ |n IHn] IN.
- by unfold index_iota, distances in IN.
- destruct n; first by unfold distances, index_iota in IN.
move: IN; rewrite -addn1 /index_iota subn0 iotaD add0n.
@@ -598,7 +594,7 @@ Section NondecreasingSequence.
rewrite -addn1 iotaD /last0 last_cat add0n addn1 // subSnn in_cons;
move => /orP [/eqP EQ|F]; subst.
Qed.
-
+
End Distances.
(** * Properties of Distances of Non-Decreasing Sequence *)
@@ -629,7 +625,7 @@ Section NondecreasingSequence.
have EQ: exists Δ, indy = indx + Δ; [by exists (indy - indx); lia | move: EQ => [Δ EQ]; subst indy].
have F: exists ind, indx <= ind < indx + Δ /\ xs[|ind|] < xs[|ind.+1|].
{ subst x y; clear SIZEx SIZEy; revert xs indx LTind SIZE LT.
- induction Δ; intros; first by lia.
+ elim: Δ => [ |Δ IHΔ] xs indx LTind SIZE LT; first by lia.
destruct (posnP Δ) as [ZERO|POS].
{ by subst Δ; exists indx; split; [rewrite addn1; apply/andP | rewrite addn1 in LT]; auto. }
have ALT: xs[|indx + Δ|] == xs[|indx + Δ.+1|] \/ xs[|indx + Δ|] < xs[|indx + Δ.+1|].
@@ -683,15 +679,15 @@ Section NondecreasingSequence.
nondecreasing_sequence xs ->
max0 (distances xs) <= last0 xs.
Proof.
- intros.
+ move=> xs H.
have SIZE: size xs < 2 \/ 2 <= size xs.
{ by destruct (size xs) as [ | n]; last destruct n; auto. }
move: SIZE => [LT | SIZE2].
- { by destruct xs; last destruct xs. }
+ { by destruct xs as [ |? xs]; last destruct xs. }
apply leq_trans with (last0 xs - first0 xs); last by apply leq_subr.
have F: forall xs c, (forall x, x \in xs -> x <= c) -> max0 xs <= c.
- { clear; intros.
- induction xs; first by done.
+ { clear; move=> xs c H.
+ elim: xs H => [//|a xs IHxs] H.
rewrite max0_cons geq_max; apply/andP; split.
+ by apply H; rewrite in_cons; apply/orP; left.
+ by apply IHxs; intros; apply H; rewrite in_cons; apply/orP; right.
@@ -715,7 +711,7 @@ Section NondecreasingSequence.
- by rewrite leq_eqVlt; apply/orP; left.
- rewrite /first0 -nth0. apply H.
rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
- destruct idx; first by move: EQ; rewrite /first0 -nth0; move => /eqP.
+ destruct idx as [ |idx]; first by move: EQ; rewrite /first0 -nth0; move => /eqP.
apply/andP; split; first by done.
by apply ltn_trans with idx.+2.
}
@@ -733,7 +729,7 @@ Section NondecreasingSequence.
intros xs.
have EX: exists len, size xs <= len by (exists (size xs)).
destruct EX as [n BO].
- revert xs BO; induction n; intros ? Len k Bound NonDec.
+ elim: n xs BO => [ |n IHn] xs Len k Bound NonDec.
{ move: Len; rewrite leqn0 size_eq0; move => /eqP T; subst.
by rewrite filter_pred0.
}
@@ -762,7 +758,7 @@ Section NondecreasingSequence.
by rewrite {1}range_iota_filter_step // distances_unfold_2cons {1}range_iota_filter_step //.
}
Qed.
-
+
(** Let [xs] again be a non-decreasing sequence. We prove that
distances of sequence [undup xs] coincide with
sequence of positive distances of [xs]. *)
@@ -771,12 +767,12 @@ Section NondecreasingSequence.
nondecreasing_sequence xs ->
[seq d <- distances xs | 0 < d] = distances (undup xs).
Proof.
- intros ? NonDec.
+ move=> xs NonDec.
rewrite -(distances_iota_filtered _ (max0 xs)); [ | by apply in_max0_le | by done].
enough ([seq Ï <- index_iota 0 (max0 xs).+1 | Ï \in xs] = (undup xs)) as IN; first by rewrite IN.
have EX: exists len, size xs <= len.
{ exists (size xs); now simpl. } destruct EX as [n BO].
- revert xs NonDec BO; induction n.
+ elim: n xs NonDec BO => [ |n IHn].
- by intros xs _; rewrite leqn0 size_eq0 => /eqP ->; rewrite filter_pred0.
- intros [ |x1 [ | x2 xs]].
+ by rewrite filter_pred0.
@@ -797,7 +793,6 @@ Section NondecreasingSequence.
by rewrite IHn //; eauto using nondecreasing_sequence_cons.
Qed.
-
(** Consider two non-decreasing sequences [xs] and [ys] and assume that
(1) first element of [xs] is at most the first element of [ys] and
(2) distances-sequences of [xs] is dominated by distances-sequence of
@@ -818,10 +813,11 @@ Section NondecreasingSequence.
{ exists (maxn (size xs) (size ys)).
by split; rewrite leq_max; apply/orP; [left | right].
} move: EX => [len [LE1 LE2]].
- generalize dependent xs; generalize dependent ys.
- induction len.
- { by intros; move: LE1 LE2; rewrite !leqn0 !size_eq0 => /eqP -> /eqP ->. }
- { intros ? LycSIZE ? LxSIZE FLE Sxs Sys SIZEEQ STRxs STRys LE n.
+ generalize dependent xs; generalize dependent ys.
+ elim: len => [ |len IHlen].
+ { move=> ys + xs + H H0 h1 H2 H3 H4 H5 n.
+ by rewrite !leqn0 !size_eq0 => /eqP -> /eqP ->. }
+ { intros ys LycSIZE xs LxSIZE FLE Sxs Sys SIZEEQ STRxs STRys LE n.
destruct xs as [ | x1 xs], ys as [ | y1 ys]; try by done.
destruct xs as [ | x2 xs], ys as [ | y2 ys]; try by done.
have F: x2 <= y2.
@@ -835,7 +831,7 @@ Section NondecreasingSequence.
- by apply leq_trans with y2; auto using leq_addr.
}
destruct xs as [ | x3 xs], ys as [ | y3 ys]; try by done.
- { by destruct n; [ | destruct n]. }
+ { by destruct n as [ |n]; [ | destruct n]. }
destruct n; first by done.
simpl; apply IHlen; try done.
- by apply/eqP; rewrite -(eqn_add2r 1) !addn1; apply/eqP.
@@ -847,7 +843,7 @@ Section NondecreasingSequence.
apply (STRys m1.+1 m2.+1); apply/andP; split.
+ by rewrite ltnS.
+ by rewrite -(ltn_add2r 1) !addn1 in B2.
- - by intros; specialize (LE n0.+1); simpl in LE.
+ - by move=> n0; specialize (LE n0.+1); simpl in LE.
}
Qed.
diff --git a/util/search_arg.v b/util/search_arg.v
index 116da8c36d2dd0f4a90c8c65778f361f0e31d6eb..5484c3ab7c715aa6843894748dc2d12fb2cf63a7 100644
--- a/util/search_arg.v
+++ b/util/search_arg.v
@@ -48,7 +48,7 @@ Section ArgSearch.
forall a b,
search_arg a b = None <-> forall x, a <= x < b -> ~~ P (f x).
Proof.
- split.
+ move=> a b; split.
{ (* if *)
elim: b => [ _ | b' HYP]; first by move=> _ /andP [_ FALSE] //.
rewrite /search_arg -/search_arg.
@@ -95,7 +95,7 @@ Section ArgSearch.
exists y, search_arg a b = Some y.
Proof.
move=> a b H_exists.
- destruct (search_arg a b) eqn:SEARCH; first by exists n.
+ destruct (search_arg a b) as [n|] eqn:SEARCH; first by exists n.
move: SEARCH. rewrite search_arg_none => NOT_exists.
exfalso.
move: H_exists => [x [RANGE Pfx]].
@@ -214,7 +214,7 @@ Section ExMinn.
P (ex_minn ex) ->
exists n, P n /\ pred n /\ (forall n', pred n' -> n <= n').
Proof.
- intros.
+ move=> P pred ex.
exists (ex_minn ex); repeat split; auto.
all: have MIN := ex_minnP ex; move: MIN => [n Pn MIN]; auto.
Qed.
@@ -226,8 +226,8 @@ Section ExMinn.
forall (P : nat -> bool) (exP : exists n, P n) (c : nat),
P c ->
ex_minn exP <= c.
- Proof.
- intros ? ? ? EX.
+ Proof.
+ move=> P exP c EX.
rewrite leqNgt; apply/negP; intros GT.
pattern (ex_minn (P:=P) exP) in GT;
apply prop_on_ex_minn in GT; move: GT => [n [LT [Pn MIN]]].
diff --git a/util/sum.v b/util/sum.v
index dbc969c9aa515eac60eebbcc12cb2ec95050af09..2e6341f825d6347fa2e595b24a83567294e0f414 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -242,17 +242,14 @@ Section SumsOverRanges.
\sum_(t <= x < t + Δ) f x < Δ ->
exists x, t <= x < t + Δ /\ f x = 0.
Proof.
- induction Δ; intros; first by rewrite ltn0 in H.
- destruct (f (t + Δ)) eqn: EQ.
+ move=> f t; elim=> [|Δ IHΔ] H; first by rewrite ltn0 in H.
+ destruct (f (t + Δ)) as [|n] eqn: EQ.
{ exists (t + Δ); split; last by done.
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS]. }
{ move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move => H.
- feed IHΔ.
+ have {}/IHΔ [z [/andP[LE GE] ZERO]] : \sum_(t <= t' < t + Δ) f t' < Δ.
{ by apply leq_ltn_trans with (\sum_(t <= i < t + Δ) f i + n); first rewrite leq_addr. }
- move: IHΔ => [z [/andP [LE GE] ZERO]].
- exists z; split; last by done.
- apply/andP; split; first by done.
- by rewrite ltnS ltnW. }
+ by exists z; split=> //; rewrite LE/= ltnS ltnW. }
Qed.
(** Next, we prove that the summing over the difference of two functions is
@@ -292,10 +289,10 @@ Section SumOfTwoIntervals.
Lemma big_sum_eq_in_eq_sized_intervals:
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t.
Proof.
- induction d; first by rewrite !addn0 !big_geq.
+ elim: d equal_before_d => [|n IHn] eq; first by rewrite !addn0 !big_geq.
rewrite !addnS !big_nat_recr => //; try by lia.
- rewrite IHn //=; last by move=> g G_LTl; apply (equal_before_d g); lia.
- by rewrite equal_before_d.
+ rewrite IHn //=; last by move=> g G_LTl; apply (eq g); lia.
+ by rewrite eq.
Qed.
End SumOfTwoIntervals.
diff --git a/util/supremum.v b/util/supremum.v
index 78bdec9d80a2c15fcea5929432f1c08dcddbe13c..deac9d82516ca33882f6b2c59708c2ba3ba8df85 100644
--- a/util/supremum.v
+++ b/util/supremum.v
@@ -48,7 +48,7 @@ Section SelectSupremum.
elim: s IN; first by done.
move=> a l _ _.
rewrite supremum_unfold.
- destruct (supremum l); rewrite /choose_superior //.
+ destruct (supremum l) as [s|]; rewrite /choose_superior //.
by destruct (R a s).
Qed.
@@ -59,7 +59,7 @@ Section SelectSupremum.
elim: s; first by done.
move => a l IH.
rewrite supremum_unfold /choose_superior.
- by destruct (supremum l); try destruct (R a s).
+ by destruct (supremum l) as [s|]; try destruct (R a s).
Qed.
(** Next, we observe that the value found by [supremum] comes indeed from the
@@ -73,12 +73,12 @@ Section SelectSupremum.
elim => // a l IN_TAIL IN.
rewrite in_cons; apply /orP.
move: IN; rewrite supremum_unfold.
- destruct (supremum l); rewrite /choose_superior.
+ destruct (supremum l) as [s|]; rewrite /choose_superior.
{ elim: (R a s) => EQ.
- left; apply /eqP.
by injection EQ.
- right; by apply IN_TAIL. }
- { left. apply /eqP.
+ { move=> IN; left. apply /eqP.
by injection IN. }
Qed.
@@ -112,7 +112,7 @@ Section SelectSupremum.
{ rewrite in_cons => /orP [/eqP EQy | INy]; last first.
- have R_by: R b y
by apply IH => //; apply supremum_in.
- apply H_R_transitive with (y := b) => //.
+ apply: H_R_transitive R_by.
destruct (R s1 b) eqn:R_s1b;
by injection SOME_z => <-.
- move: IN_z_s; rewrite in_cons => /orP [/eqP EQz | INz];
diff --git a/util/unit_growth.v b/util/unit_growth.v
index 73bbc9f9f12f25bd109cea01d100fe80b0ddb83e..4141bbc8531d08632109005ce55fdeb9e78dc397 100644
--- a/util/unit_growth.v
+++ b/util/unit_growth.v
@@ -41,7 +41,7 @@ Section Lemmas.
{ by apply/andP; split; last by rewrite addnBA // addKn. }
by rewrite subnKC in DELTA.
}
- induction delta.
+ elim=> [|delta IHdelta].
{ rewrite addn0; move => /andP [GE0 LT0].
by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
}