Add tactics to compute [exists] and [forall]

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/exists.v ./util/induction.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/bertogna_fp_example.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/parallel/bertogna_edf_example.v ./implementation/parallel/task.v ./implementation/parallel/schedule.v ./implementation/parallel/bertogna_fp_example.v ./implementation/parallel/job.v ./implementation/parallel/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/bertogna_fp_example.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/task.v ./implementation/apa/schedule.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/job.v ./implementation/apa/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/interference_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/apa/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/constrained_deadlines.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/constrained_deadlines.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/apa/time.v ./model/apa/schedulability.v ./model/apa/task.v ./model/apa/task_arrival.v ./model/apa/platform.v ./model/apa/schedule.v ./model/apa/priority.v ./model/apa/affinity.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/constrained_deadlines.v ./model/apa/workload.v ./model/apa/job.v ./model/apa/arrival_sequence.v ./model/apa/response_time.v -o Makefile 
+# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/induction.v ./util/ord_quantifier.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/bertogna_fp_example.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/parallel/bertogna_edf_example.v ./implementation/parallel/task.v ./implementation/parallel/schedule.v ./implementation/parallel/bertogna_fp_example.v ./implementation/parallel/job.v ./implementation/parallel/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/bertogna_fp_example.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/task.v ./implementation/apa/schedule.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/job.v ./implementation/apa/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/interference_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/apa/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/constrained_deadlines.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/constrained_deadlines.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/apa/time.v ./model/apa/schedulability.v ./model/apa/task.v ./model/apa/task_arrival.v ./model/apa/platform.v ./model/apa/schedule.v ./model/apa/priority.v ./model/apa/affinity.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/constrained_deadlines.v ./model/apa/workload.v ./model/apa/job.v ./model/apa/arrival_sequence.v ./model/apa/response_time.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -106,8 +106,8 @@ VFILES:=util/fixedpoint.v\
   util/sorting.v\
   util/tactics.v\
   util/bigord.v\
-  util/exists.v\
   util/induction.v\
+  util/ord_quantifier.v\
   util/sum.v\
   util/divround.v\
   util/counting.v\

implementation/apa/bertogna_edf_example.v

@@ -107,52 +107,26 @@ Module ResponseTimeAnalysisEDF.
         by rewrite unlock; compute.
       } rewrite STEPS; clear STEPS.
 
-      have cpu0P: 0 < 2 by done.
-      have cpu1P: 1 < 2 by done.
-
-      have cpu_compute :
-        forall (P: processor num_cpus -> bool),
-          [exists x, P x] =
-            if (P (cpu 0 cpu0P)) then true else
-              if P (cpu 1 cpu1P) then true else false.
-      {
-        unfold num_cpus in *; intros P.
-        destruct (P (cpu 0 cpu0P)) eqn:P0;
-          first by apply/existsP; exists (cpu 0 cpu0P).
-        destruct (P (cpu 1 cpu1P)) eqn:P1;
-          first by apply/existsP; exists (cpu 1 cpu1P).
-        apply negbTE; rewrite negb_exists; apply/forallP.
-        intros x; destruct x as [x LE]; apply negbT.
-        have GE0 := leq0n x.
-        rewrite leq_eqVlt in GE0; move: GE0 => /orP [/eqP EQ0 | GE1];
-          first by rewrite -P0; f_equal; apply ord_inj.
-        rewrite leq_eqVlt in GE1; move: GE1 => /orP [/eqP EQ1 | GE2];
-          first by rewrite -P1; f_equal; apply ord_inj.
-        have LE' := LE.
-        apply leq_ltn_trans with (m := 2) in LE'; last by done.
-        by rewrite ltnn in LE'.
-      }
-
-      Ltac f :=
+      Local Ltac f :=
         unfold edf_rta_iteration; simpl;
         unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W, edf_specific_interference_bound, different_task_in, affinity_intersects; simpl;
         rewrite !addnE !set_card !big_cons ?big_nil /=.
 
-      
+      Local Ltac g := destruct master_key; f; simpl_exists_ord.      
       rewrite [edf_rta_iteration]lock; simpl.
-      unfold locked at 13; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 12; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 11; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 10; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 9; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 8; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 7; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 6; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 5; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 4; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 3; destruct master_key; f; rewrite !cpu_compute /=.
-      unfold locked at 2; destruct master_key; f; rewrite !cpu_compute /=.
-      by unfold locked at 1; destruct master_key; f; rewrite !cpu_compute /=.
+      unfold locked at 13; g.
+      unfold locked at 12; g.
+      unfold locked at 11; g.
+      unfold locked at 10; g.
+      unfold locked at 9; g.
+      unfold locked at 8; g.
+      unfold locked at 7; g.
+      unfold locked at 6; g.
+      unfold locked at 5; g.
+      unfold locked at 4; g.
+      unfold locked at 3; g.
+      unfold locked at 2; g.
+      by unfold locked at 1; g.
     Qed.
 
     (* Let arr_seq be the periodic arrival sequence from ts. *)

implementation/apa/bertogna_fp_example.v

@@ -131,32 +131,6 @@ Module ResponseTimeAnalysisFP.
       rewrite big_nil div0n addn0 /=.
       unfold div_floor; rewrite !set_card /=.   
 
-      have cpu0P: 0 < 2 by done.
-      have cpu1P: 1 < 2 by done.
-
-      have cpu_compute :
-        forall (P: processor num_cpus -> bool),
-          [exists x, P x] =
-            if (P (cpu 0 cpu0P)) then true else
-              if P (cpu 1 cpu1P) then true else false.
-      {
-        unfold num_cpus in *; intros P.
-        destruct (P (cpu 0 cpu0P)) eqn:P0;
-          first by apply/existsP; exists (cpu 0 cpu0P).
-        destruct (P (cpu 1 cpu1P)) eqn:P1;
-          first by apply/existsP; exists (cpu 1 cpu1P).
-        apply negbTE; rewrite negb_exists; apply/forallP.
-        intros x; destruct x as [x LE]; apply negbT.
-        have GE0 := leq0n x.
-        rewrite leq_eqVlt in GE0; move: GE0 => /orP [/eqP EQ0 | GE1];
-          first by rewrite -P0; f_equal; apply ord_inj.
-        rewrite leq_eqVlt in GE1; move: GE1 => /orP [/eqP EQ1 | GE2];
-          first by rewrite -P1; f_equal; apply ord_inj.
-        have LE' := LE.
-        apply leq_ltn_trans with (m := 2) in LE'; last by done.
-        by rewrite ltnn in LE'.
-      }
-
       set I2 := total_interference_bound_fp task_cost task_period
                         task_affinity tsk2 alpha2  [:: (tsk1, 3)].
 
@@ -164,28 +138,28 @@ Module ResponseTimeAnalysisFP.
       {
         unfold I2, total_interference_bound_fp; rewrite big_cons big_nil.
         unfold higher_priority_task_in; simpl.
-        by rewrite /affinity_intersects cpu_compute /= addn0; compute.
+        by rewrite /affinity_intersects; simpl_exists_ord; compute.
       }
       rewrite H1 !divn1 !addn1; clear H1.
       assert (H1: I2 3 (RM task_period) = 2).
       {
         unfold I2, total_interference_bound_fp; rewrite big_cons big_nil.
         unfold higher_priority_task_in; simpl.
-        by rewrite /affinity_intersects cpu_compute /= addn0; compute.
+        by rewrite /affinity_intersects; simpl_exists_ord; compute.
       }
       rewrite H1 !addn2; clear H1.
       assert (H1: I2 4 (RM task_period) = 3).
       {
         unfold I2, total_interference_bound_fp; rewrite big_cons big_nil.
         unfold higher_priority_task_in; simpl.
-        by rewrite /affinity_intersects cpu_compute /= addn0; compute.
+        by rewrite /affinity_intersects; simpl_exists_ord; compute.
       }
       rewrite H1 !addn3; clear H1.
       assert (H1: I2 5 (RM task_period) = 3).
       {
         unfold I2, total_interference_bound_fp; rewrite big_cons big_nil.
         unfold higher_priority_task_in; simpl.
-        by rewrite /affinity_intersects cpu_compute /= addn0; compute.
+        by rewrite /affinity_intersects; simpl_exists_ord; compute.
       }
       rewrite H1 !addn3; clear H1.
       have H2: 4 < 5 by compute.
@@ -206,35 +180,36 @@ Module ResponseTimeAnalysisFP.
             rewrite /total_interference_bound_fp /interference_bound_generic
                     /W /max_jobs /div_floor !big_cons big_nil /= /higher_priority_task_in /=
                     /affinity_intersects.
+
         set x9 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I9: x9 = 1 by unfold x9; g; rewrite ?cpu_compute /=; compute.
+        have I9: x9 = 1 by unfold x9; g; simpl_exists_ord; compute.
         rewrite I9 iterSr.
         set x8 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I8: x8 = 2 by unfold x8; g; rewrite ?cpu_compute /=; compute.
+        have I8: x8 = 2 by unfold x8; g; simpl_exists_ord; compute.
         rewrite I8 iterSr.
         set x7 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I7: x7 = 3 by unfold x7; g; rewrite ?cpu_compute /=; compute.
+        have I7: x7 = 3 by unfold x7; g; simpl_exists_ord; compute.
         rewrite I7 iterSr.
         set x6 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I6: x6 = 3 by unfold x6; g; rewrite ?cpu_compute /=; compute.
+        have I6: x6 = 3 by unfold x6; g; simpl_exists_ord; compute.
         rewrite I6 iterSr.
         set x5 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I5: x5 = 3 by unfold x5; g; rewrite ?cpu_compute /=; compute.
+        have I5: x5 = 3 by unfold x5; g; simpl_exists_ord; compute.
         rewrite I5 iterSr.
         set x4 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I4: x4 = 3 by unfold x4; g; rewrite ?cpu_compute /=; compute.
+        have I4: x4 = 3 by unfold x4; g; simpl_exists_ord; compute.
         rewrite I4 iterSr.
         set x3 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I3: x3 = 3 by unfold x3; g; rewrite ?cpu_compute /=; compute.
+        have I3: x3 = 3 by unfold x3; g; simpl_exists_ord; compute.
         rewrite I3 iterSr.
         set x2 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I2: x2 = 3 by unfold x2; g; rewrite ?cpu_compute /=; compute.
+        have I2: x2 = 3 by unfold x2; g; simpl_exists_ord; compute.
         rewrite I2 iterSr.
         set x1 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I1: x1 = 3 by unfold x1; g; rewrite ?cpu_compute /=; compute.
+        have I1: x1 = 3 by unfold x1; g; simpl_exists_ord; compute.
         rewrite I1 iterSr /=.
         set x0 := total_interference_bound_fp _ _ _ _ _ _ _ _.
-        have I0: x0 = 3 by unfold x0; g; rewrite ?cpu_compute /=; compute.
+        have I0: x0 = 3 by unfold x0; g; simpl_exists_ord; compute.
         by rewrite I0; compute.
       }
       by rewrite H4.

util/all.v

@@ -6,7 +6,7 @@ Require Export rt.util.bigcat.
 Require Export rt.util.bigord.
 Require Export rt.util.counting.
 Require Export rt.util.divround.
-Require Export rt.util.exists.
+Require Export rt.util.ord_quantifier.
 Require Export rt.util.fixedpoint.
 Require Export rt.util.induction.
 Require Export rt.util.list.

util/counting.v

-Require Import rt.util.tactics rt.util.exists.
+Require Import rt.util.tactics rt.util.ord_quantifier.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (* Additional lemmas about counting. *)

util/exists.v → util/ord_quantifier.v

 Require Import rt.util.tactics.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
 
-(* Lemmas about the finite existential for Ordinals: [exists x, P x]. *)
+(* Lemmas about the exists for Ordinals: [exists x, P x]. *)
 Section OrdExists.
 
   Lemma exists_ord0:
-    forall (T: eqType) P,
+    forall P,
       [exists x in 'I_0, P x] = false.
   Proof.
-    intros T P.
+    intros P.
     apply negbTE; rewrite negb_exists; apply/forall_inP.
     intros x; destruct x as [x LT].
     by exfalso; rewrite ltn0 in LT.
   Qed.
 
   Lemma exists_recr:
-    forall (T: eqType) n P,
+    forall n P,
       [exists x in 'I_n.+1, P x] =
       [exists x in 'I_n, P (widen_ord (leqnSn n) x)] || P (ord_max).
   Proof.
-    intros t n P.
+    intros n P.
     apply/idP/idP.
     {
       move => /exists_inP EX; destruct EX as [x IN Px].
@@ -51,22 +51,51 @@ Section OrdExists.
 
 End OrdExists.
 
-(*Section Computation.
+(* Lemmas about the forall for Ordinals: [exists x, P x]. *)
+Section OrdForall.
 
-  Variable m: nat.
-  Hypothesis H_m_positive: m > 0.
-
-  Variable P: 'I_m -> bool.
-
-  Program Fixpoint compute_exists n (Q: n < m) :=
-    match n with
-    | 0 => P (@Ordinal m 0 _)
-    | S n => P (@Ordinal m (S n) _) || compute_exists n _
-    end.
+  Lemma forall_ord0:
+    forall P,
+      [forall x in 'I_0, P x].
+  Proof.
+    intros P; apply/forall_inP.
+    by intros x IN0; destruct x.
+  Qed.
 
-  Program Definition compute_exists_ordinal := compute_exists (m.-1) _.
-  Next Obligation.
-    by rewrite -(ltn_add2r 1) 2!addn1 prednK //.
+  Lemma forall_recr:
+    forall n P,
+      [forall x in 'I_n.+1, P x] =
+      [forall x in 'I_n, P (widen_ord (leqnSn n) x)] && P (ord_max).
+  Proof.
+    intros n P.
+    apply/idP/idP.
+    {
+      move => /forall_inP ALL.
+      apply/andP; split; last by apply ALL.
+      by apply/forall_inP; intros x IN; apply ALL.
+    }
+    {
+      move => /andP [/forall_inP ALL MAX].
+      apply/forall_inP; intros x IN.
+      destruct x as [x LT].
+      unfold ord_max in *.
+      remember LT as LT'; clear HeqLT'.
+      rewrite ltnS leq_eqVlt in LT; move: LT => /orP [/eqP EQ | LT].
+      {
+        subst n.
+        apply/eqP; rewrite -MAX; apply/eqP.
+        by unfold ord_max; apply f_equal, ord_inj.
+      }
+      {
+        feed (ALL (Ordinal LT)); first by done.
+        apply/eqP; rewrite -ALL; apply/eqP.
+        by apply f_equal, ord_inj.
+      }
+    }
   Qed.
 
-End Computation.*)
\ No newline at end of file
+End OrdForall.
+
+(* Tactics for simplifying exists and forall. *)
+Ltac simpl_exists_ord := rewrite !exists_recr !exists_ord0 /=.
+Ltac simpl_forall_ord := rewrite !forall_recr !forall_ord0 /=.
\ No newline at end of file