Commit a5cc6b86 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Clean-up Vbase tactics

parent 266c9014
......@@ -238,8 +238,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
apply/(zipP (fun x y => snd x <= snd y)); try (by ins).
by ins; apply leqnn.
by apply/(zipP (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
......@@ -507,7 +506,6 @@ Module ResponseTimeIterationEDF.
try (by done);
[ by apply all_le_reflexive
| by apply all_le_transitive
| by apply leqnSn
| by apply bertogna_edf_comp_iteration_preserves_order
| by apply bertogna_edf_comp_iteration_preserves_minimum].
Qed.
......
......@@ -402,8 +402,7 @@ Module ResponseTimeIterationFP.
{
apply leq_trans with (n := W task_cost task_period i R x1); first by apply geq_minl.
exploit (VALID i); [by rewrite mem_rcons in_cons IN orbT | ins; des].
by apply W_monotonic; try (by ins);
[by apply GE_COST | by apply leqnn].
by apply W_monotonic; try by ins; apply GE_COST.
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1); first by apply geq_minr.
......
......@@ -497,9 +497,8 @@ Module InterferenceBoundEDF.
by apply job_interference_seq_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
(R := R_k);
try (by done); last by apply leqnn.
rewrite -> cumulative_service_after_job_rt_zero with
(job_cost0 := job_cost) (R := R_k); try (by done).
rewrite addn0; apply extend_sum; first by apply leqnn.
by rewrite leq_add2l; apply H_R_k_le_deadline.
}
......@@ -515,8 +514,8 @@ Module InterferenceBoundEDF.
by apply job_interference_seq_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R:=R_k);
try (by done); last by apply leqnn.
rewrite -> cumulative_service_after_job_rt_zero with
(job_cost0 := job_cost) (R:=R_k); try (by done).
rewrite addn0.
apply leq_trans with (n := (\sum_(t1 <= t < a_fst + R_k) 1) +
\sum_(a_fst + R_k <= t < a_fst + D_k) 1).
......@@ -800,9 +799,9 @@ Module InterferenceBoundEDF.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
......@@ -875,8 +874,7 @@ Module InterferenceBoundEDF.
rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
first by rewrite SIZE ltnS leqNgt NK in NUM.
by move: NK => /eqP NK; rewrite NK.
[by rewrite SIZE ltnS leqNgt NK in NUM | by done].
Qed.
(* After proving the bounds of the middle and last jobs, we do the same for
......
......@@ -78,7 +78,7 @@ Module WorkloadBound.
rewrite leq_eqVlt in LTp; move: LTp => /orP LTp; des;
last by rewrite ltnS in LTp; apply (leq_trans H_period_positive) in LTp.
{
move: LTp => /eqP LTp; rewrite LTp 2!modn1 2!divn1.
rewrite LTp 2!modn1 2!divn1.
rewrite leq_add2l leq_mul2r; apply/orP; right.
by rewrite leq_sub2r // leq_add2l.
}
......@@ -253,7 +253,7 @@ Module WorkloadBound.
Proof.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
repeat split; [by apply/eqP | | by done].
repeat split; [by done | | by done].
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
......@@ -432,8 +432,7 @@ Module WorkloadBound.
[| by apply workload_bound_response_time_of_first_job_inside_interval
| by apply ltnW].
rewrite -{2}[\sum_(_ <= _ < _) _]addn0 /= leq_add2l leqn0; apply/eqP.
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
try (by done); last by apply leqnn.
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk); try (by done).
apply H_response_time_bound; last by done.
exploit workload_bound_all_jobs_from_tsk.
by apply mem_nth; instantiate (1 := 0); rewrite H_at_least_two_jobs.
......@@ -544,9 +543,9 @@ Module WorkloadBound.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
(* Prove that n_k is at least the number of the middle jobs *)
......
......@@ -292,8 +292,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
apply/(zipP (fun x y => snd x <= snd y)); try (by ins).
by ins; apply leqnn.
by apply/(zipP (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
......@@ -562,7 +561,6 @@ Module ResponseTimeIterationEDF.
try (by done);
[ by apply all_le_reflexive
| by apply all_le_transitive
| by apply leqnSn
| by apply bertogna_edf_comp_iteration_preserves_order
| by apply bertogna_edf_comp_iteration_preserves_minimum].
Qed.
......
......@@ -407,8 +407,7 @@ Module ResponseTimeIterationFP.
apply leq_trans with (n := W_jitter task_cost task_period task_jitter i R x1);
first by apply geq_minl.
exploit (VALID i); first by rewrite mem_rcons in_cons; apply/orP; right.
by ins; des; apply W_monotonic; try (by ins);
[by apply GE_COST | by apply leqnn].
by ins; des; apply W_monotonic; try (by ins); apply GE_COST.
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1); first by apply geq_minr.
......
......@@ -527,8 +527,8 @@ Module InterferenceBoundEDFJitter.
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
(R := J_k + R_k);
try (by done); rewrite ?addnA //; last by apply leqnn.
rewrite addn0; apply extend_sum; first by apply leqnn.
rewrite ?addnA //.
rewrite addn0; apply extend_sum; first by done.
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
......@@ -552,7 +552,7 @@ Module InterferenceBoundEDFJitter.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R:=J_k + R_k);
try (by done); rewrite ?addnA //; last by apply leqnn.
rewrite ?addnA //.
rewrite addn0.
apply leq_trans with (n := (\sum_(a_i <= t < a_fst + J_k + R_k) 1) +
\sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1).
......@@ -884,9 +884,9 @@ Module InterferenceBoundEDFJitter.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
......@@ -964,7 +964,7 @@ Module InterferenceBoundEDFJitter.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
first by rewrite SIZE ltnS leqNgt NK in NUM.
by move: NK => /eqP NK; rewrite NK.
by rewrite NK.
Qed.
(* After proving the bounds of the middle and last jobs, we do the same for
......
......@@ -79,7 +79,7 @@ Module WorkloadBoundJitter.
rewrite leq_eqVlt in LTp; move: LTp => /orP LTp; des;
last by rewrite ltnS in LTp; apply (leq_trans H_period_positive) in LTp.
{
move: LTp => /eqP LTp; rewrite LTp 2!modn1 2!divn1.
rewrite LTp 2!modn1 2!divn1.
rewrite leq_add2l leq_mul2r; apply/orP; right.
by rewrite leq_sub2r // leq_add2l.
}
......@@ -257,7 +257,7 @@ Module WorkloadBoundJitter.
Proof.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
repeat split; [by apply/eqP | | by done].
repeat split; [by done | | by done].
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
......@@ -562,9 +562,9 @@ Module WorkloadBoundJitter.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
(* Prove that n_k is at least the number of the middle jobs *)
......
......@@ -239,8 +239,7 @@ Module ResponseTimeIterationEDF.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
apply/(zipP (fun x y => snd x <= snd y)); try (by ins).
by ins; apply leqnn.
by apply/(zipP (fun x y => snd x <= snd y)).
Qed.
(* ... and transitive. *)
......@@ -508,7 +507,6 @@ Module ResponseTimeIterationEDF.
try (by done);
[ by apply all_le_reflexive
| by apply all_le_transitive
| by apply leqnSn
| by apply bertogna_edf_comp_iteration_preserves_order
| by apply bertogna_edf_comp_iteration_preserves_minimum].
Qed.
......
......@@ -618,9 +618,9 @@ Module InterferenceBoundEDF.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
Lemma interference_bound_edf_slack_le_delta:
......
......@@ -186,7 +186,7 @@ Module WorkloadBound.
Proof.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
repeat split; [by apply/eqP | | by done].
repeat split; [by done | | by done].
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
......@@ -396,9 +396,9 @@ Module WorkloadBound.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.
by rewrite INnth INnth0.
}
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
by rewrite subh3 // addnC -INnth.
Qed.
(* Next, we prove that n_k covers every scheduled job, ... *)
......
......@@ -75,25 +75,25 @@ Module ConcreteArrivalSequence.
unfold arrives_at, arr_seq, periodic_arrival_sequence in *.
rewrite 2!mem_pmap in ARR ARR'.
move: ARR ARR' => /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
unfold add_job in *; desf; simpl in *; subst.
clear INj'.
move: Heq Heq0 => /dvdnP DIV' /dvdnP DIV; des.
rewrite DIV DIV' -mulSnr.
rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
unfold add_job in SOMEj, SOMEj'; desf; simpl in *;
move: Heq0 Heq => /dvdnP [k DIV] /dvdnP [k' DIV'].
{
move: DIFF => /orP [/eqP CASE1 | /eqP CASE2].
- by exfalso; apply CASE1; repeat f_equal.
- by rewrite EQ in CASE2.
rewrite DIV DIV' -mulSnr.
rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
{
exfalso; move: DIFF => /negP DIFF; apply DIFF.
by subst; rewrite EQ.
}
subst; rewrite leq_mul2r; apply/orP; right.
by rewrite ltn_mul2r in LESS; move: LESS => /andP [_ LT].
}
rewrite leq_mul2r; apply/orP; right.
rewrite ltn_neqAle; apply/andP; split.
{
apply/eqP; red; intro EQ; subst.
by rewrite ltnn in LESS.
assert (LT: arr < arr'). by rewrite ltn_neqAle; apply/andP.
clear LE DIFF; subst tsk_j' arr arr'.
rewrite ltn_mul2r in LT; move: LT => /andP [_ LT].
by apply leq_trans with (n := k.+1 * task_period tsk_j);
[by rewrite mulSnr | by rewrite leq_mul2r; apply/orP; right].
}
rewrite leqNgt; apply/negP; red; intro LT.
rewrite ltnNge in LESS; move: LESS => /negP LESS; apply LESS.
by subst; rewrite leq_mul2r; apply/orP; right; apply ltnW.
Qed.
(* ... and if the task set has no duplicates, the same applies to
......
......@@ -75,25 +75,25 @@ Module ConcreteArrivalSequence.
unfold arrives_at, arr_seq, periodic_arrival_sequence in *.
rewrite 2!mem_pmap in ARR ARR'.
move: ARR ARR' => /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
unfold add_job in *; desf; simpl in *; subst.
clear INj'.
move: Heq Heq0 => /dvdnP DIV' /dvdnP DIV; des.
rewrite DIV DIV' -mulSnr.
rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
unfold add_job in SOMEj, SOMEj'; desf; simpl in *;
move: Heq0 Heq => /dvdnP [k DIV] /dvdnP [k' DIV'].
{
move: DIFF => /orP [/eqP CASE1 | /eqP CASE2].
- by exfalso; apply CASE1; repeat f_equal.
- by rewrite EQ in CASE2.
rewrite DIV DIV' -mulSnr.
rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
{
exfalso; move: DIFF => /negP DIFF; apply DIFF.
by subst; rewrite EQ.
}
subst; rewrite leq_mul2r; apply/orP; right.
by rewrite ltn_mul2r in LESS; move: LESS => /andP [_ LT].
}
rewrite leq_mul2r; apply/orP; right.
rewrite ltn_neqAle; apply/andP; split.
{
apply/eqP; red; intro EQ; subst.
by rewrite ltnn in LESS.
assert (LT: arr < arr'). by rewrite ltn_neqAle; apply/andP.
clear LE DIFF; subst tsk_j' arr arr'.
rewrite ltn_mul2r in LT; move: LT => /andP [_ LT].
by apply leq_trans with (n := k.+1 * task_period tsk_j);
[by rewrite mulSnr | by rewrite leq_mul2r; apply/orP; right].
}
rewrite leqNgt; apply/negP; red; intro LT.
rewrite ltnNge in LESS; move: LESS => /negP LESS; apply LESS.
by subst; rewrite leq_mul2r; apply/orP; right; apply ltnW.
Qed.
(* ... and if the task set has no duplicates, the same applies to
......
......@@ -100,9 +100,6 @@ Module ArrivalSequence.
if (j \in arr_seq t) is true then
Some (Build_JobIn arr_seq j t _)
else None.
Next Obligation.
by done.
Qed.
(* Now we define the list of JobIn that arrive at time t as the partial
map of is_JobIn. *)
......
......@@ -244,7 +244,7 @@ Module Interference.
rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
{
rewrite -addn1 addnC; apply leq_add; last by done.
rewrite EQtsk0 eq_refl BACK andTb.
rewrite EQtsk0 BACK andTb.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
unfold scheduled, scheduled_on.
by apply/exists_inP; exists x; [by done | by rewrite SCHED].
......@@ -252,7 +252,7 @@ Module Interference.
{
unfold jobs_scheduled_between.
rewrite mem_undup.
apply mem_bigcat_nat with (j := t); first by done.
apply mem_bigcat_nat with (j := t); first by auto.
unfold jobs_scheduled_at.
apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
by unfold make_sequence; rewrite SCHED mem_seq1 eq_refl.
......
......@@ -175,26 +175,24 @@ Module Interference.
}
rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
{
rewrite EQtsk0 eq_refl BACK SCHEDULED andbT big_mkcond.
rewrite EQtsk0 BACK SCHEDULED andbT big_mkcond.
rewrite (eq_bigr (fun x => 0));
first by rewrite big_const_seq iter_addn mul0n addn0 addn0.
intros j1 _; desf; [rewrite andTb | by done].
intros j1 _; desf; try by done.
apply/eqP; rewrite eqb0; apply/negP; unfold not; intro SCHEDULED'.
exploit (H_no_intratask_parallelism j0 j1 t); try (by done).
by move: Heq0 => /eqP EQtsk; rewrite EQtsk.
by intros EQj; rewrite EQj eq_refl in Heq.
exploit (H_no_intratask_parallelism j0 j1 t); try by eauto.
}
{
rewrite mem_undup.
apply mem_bigcat_nat with (j := t); first by done.
apply mem_bigcat_nat with (j := t); first by auto.
apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
by rewrite SCHED mem_seq1 eq_refl.
by rewrite SCHED mem_seq1.
}
}
{
rewrite big_mkcond (eq_bigr (fun x => 0));
first by rewrite big_const_seq iter_addn mul0n addn0.
intros i _; desf.
intros i _; desf; rewrite // ?BACK ?andFb //.
unfold task_is_scheduled in BACK.
apply negbT in BACK; rewrite negb_exists in BACK.
move: BACK => /forallP BACK.
......@@ -206,7 +204,7 @@ Module Interference.
unfold schedules_job_of_tsk in BACK; unfold scheduled_on.
destruct (sched x t) eqn:SCHED; last by ins.
apply/negP; unfold not; move => /eqP BUG; inversion BUG; subst.
by move: Heq => /eqP Heq; rewrite Heq eq_refl in BACK.
by move: BACK => /negP BACK; apply BACK.
}
by rewrite NOTSCHED andbF.
}
......@@ -235,7 +233,7 @@ Module Interference.
rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
{
rewrite -addn1 addnC; apply leq_add; last by done.
rewrite EQtsk0 eq_refl BACK andTb.
rewrite EQtsk0 BACK andTb.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
unfold scheduled, scheduled_on.
by apply/exists_inP; exists x; [by done | by rewrite SCHED].
......@@ -243,10 +241,10 @@ Module Interference.
{
unfold jobs_scheduled_between.
rewrite mem_undup.
apply mem_bigcat_nat with (j := t); first by done.
apply mem_bigcat_nat with (j := t); first by auto.
unfold jobs_scheduled_at.
apply mem_bigcat_ord with (j := x); first by apply ltn_ord.
by unfold make_sequence; rewrite SCHED mem_seq1 eq_refl.
by unfold make_sequence; rewrite SCHED mem_seq1.
}
Qed.
......
......@@ -11,11 +11,7 @@
(** Symbols starting with [vlib__] are internal. *)
Require Import Logic.Eqdep.
Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import String.
Require Import ssreflect ssrbool ssrnat eqtype.
Open Scope bool_scope.
Open Scope list_scope.
......@@ -27,28 +23,8 @@ Unset Strict Implicit.
(** * Axioms *)
(* ************************************************************************** *)
Require ClassicalFacts.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.
Ltac exten := apply functional_extensionality.
(* ************************************************************************** *)
(** * Coersion of [bool] into [Prop] *)
(* ************************************************************************** *)
(** Coersion of bools into Prop *)
Coercion is_true (b : bool) : Prop := b = true.
(** Hints for auto *)
Lemma vlib__true_is_true : true.
Proof. reflexivity. Qed.
Lemma vlib__not_false_is_true : ~ false.
Proof. discriminate. Qed.
Hint Resolve vlib__true_is_true vlib__not_false_is_true.
(* ************************************************************************** *)
(** * Very basic automation *)
(* ************************************************************************** *)
......@@ -84,274 +60,13 @@ Ltac edone := try eassumption; trivial; hnf; intros;
Tactic Notation "by" tactic(tac) := (tac; done).
Tactic Notation "eby" tactic(tac) := (tac; edone).
(* ************************************************************************** *)
(** * Boolean reflection *)
(* ************************************************************************** *)
(** These definitions are ported from ssr-bool. *)
(** Negation lemmas *)
Section NegationLemmas.
Variables (b c : bool).
Lemma negbT : b = false -> negb b.
Proof. by case b. Qed.
Lemma negbTE: negb b -> b = false.
Proof. by case b. Qed.
Lemma negbF : b -> negb b = false.
Proof. by case b. Qed.
Lemma negbFE: negb b = false -> b.
Proof. by case b. Qed.
Lemma negbNE: negb (negb b) -> b.
Proof. by case b. Qed.
Lemma negbLR : b = negb c -> negb b = c.
Proof. by case c; intro X; rewrite X. Qed.
Lemma negbRL : negb b = c -> b = negb c.
Proof. by case b; intro X; rewrite <- X. Qed.
Lemma contra : (c -> b) -> negb b -> negb c.
Proof. by case b; case c. Qed.
End NegationLemmas.
(** Lemmas for ifs, which allow reasoning about the condition without
repeating it inside the proof. *)
Section BoolIf.
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
Inductive if_spec : A -> bool -> Set :=
| IfSpecTrue : b -> if_spec vT true
| IfSpecFalse : b = false -> if_spec vF false.
Lemma ifP : if_spec (if b then vT else vF) b.
Proof. by case_eq b; constructor. Qed.
Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.
Lemma if_neg : (if negb b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.
Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.
Lemma if_arg : forall fT fF : A -> B,
(if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.
End BoolIf.
(** The reflection predicate *)
Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
(** Internal reflection lemmas *)
Section ReflectCore.
Variables (P : Prop) (b : bool) (Hb : reflect P b) (Q : Prop) (c : bool).
Lemma introNTF : (if c then ~ P else P) -> negb b = c.
Proof. by case c; case Hb. Qed.
Lemma introTF : (if c then P else ~ P) -> b = c.
Proof. by case c; case Hb. Qed.
Lemma elimNTF : negb b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma elimTF : b = c -> if c then P else ~ P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
Proof. by case Hb; auto. Qed.
Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
Proof. by case Hb; [intros ? _ H ? | intros ? H _]; case H. Qed.
End ReflectCore.
(** Internal negated reflection lemmas *)
Section ReflectNegCore.
Variables (P : Prop) (b : bool) (Hb : reflect P (negb b)) (Q : Prop) (c : bool).
Lemma introTFn : (if c then ~ P else P) -> b = c.
Proof. by intro X; apply (introNTF Hb) in X; rewrite <- X; case b. Qed.
Lemma elimTFn : b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; apply (elimNTF Hb); case b. Qed.
Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
Proof. by rewrite <- if_neg; apply equivPif. Qed.
Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
Proof. by rewrite <- if_neg; apply xorPif. Qed.
End ReflectNegCore.
(** User-oriented reflection lemmas *)
Section Reflect.
Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (negb b')).
Lemma introT : P -> b.
Proof. by apply (introTF Pb (c:=true)). Qed.
Lemma introF : ~ P -> b = false.