From 8573b097f5f8394dec85957cd725020cee9faed1 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Wed, 8 Jun 2016 13:03:28 +0200
Subject: [PATCH] Add tactics to compute [exists] and [forall]
---
Makefile | 4 +-
implementation/apa/bertogna_edf_example.v | 56 ++++--------
implementation/apa/bertogna_fp_example.v | 55 ++++--------
util/all.v | 2 +-
util/counting.v | 2 +-
util/exists.v | 72 ---------------
util/ord_quantifier.v | 101 ++++++++++++++++++++++
7 files changed, 135 insertions(+), 157 deletions(-)
delete mode 100644 util/exists.v
create mode 100644 util/ord_quantifier.v
diff --git a/Makefile b/Makefile
index f874e7c18..0824af975 100644
--- a/Makefile
+++ b/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\
diff --git a/implementation/apa/bertogna_edf_example.v b/implementation/apa/bertogna_edf_example.v
index d8fdf6fe5..c922446a9 100644
--- a/implementation/apa/bertogna_edf_example.v
+++ b/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. *)
diff --git a/implementation/apa/bertogna_fp_example.v b/implementation/apa/bertogna_fp_example.v
index 1a1452a67..e2dc3f547 100644
--- a/implementation/apa/bertogna_fp_example.v
+++ b/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.
diff --git a/util/all.v b/util/all.v
index 886d33c93..0bb353a09 100644
--- a/util/all.v
+++ b/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.
diff --git a/util/counting.v b/util/counting.v
index 3e6fe473a..e087732f8 100644
--- a/util/counting.v
+++ b/util/counting.v
@@ -1,4 +1,4 @@
-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. *)
diff --git a/util/exists.v b/util/exists.v
deleted file mode 100644
index 1376b4dfb..000000000
--- a/util/exists.v
+++ /dev/null
@@ -1,72 +0,0 @@
-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]. *)
-Section OrdExists.
-
- Lemma exists_ord0:
- forall (T: eqType) P,
- [exists x in 'I_0, P x] = false.
- Proof.
- intros T 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,
- [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.
- apply/idP/idP.
- {
- move => /exists_inP EX; destruct EX as [x IN Px].
- destruct x as [x LT].
- remember LT as LT'; clear HeqLT'.
- rewrite ltnS leq_eqVlt in LT; move: LT => /orP [/eqP EQ | LT].
- {
- apply/orP; right.
- unfold ord_max; subst x.
- apply eq_trans with (y := P (Ordinal LT')); last by done.
- by f_equal; apply ord_inj.
- }
- {
- apply/orP; left.
- apply/exists_inP; exists (Ordinal LT); first by done.
- apply eq_trans with (y := P (Ordinal LT')); last by done.
- by f_equal; apply ord_inj.
- }
- }
- {
- intro OR; apply/exists_inP.
- move: OR => /orP [/exists_inP EX | MAX].
- {
- by destruct EX as [x IN Px]; exists (widen_ord (leqnSn n) x).
- }
- by exists ord_max.
- }
- Qed.
-
-End OrdExists.
-
-(*Section Computation.
-
- 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.
-
- Program Definition compute_exists_ordinal := compute_exists (m.-1) _.
- Next Obligation.
- by rewrite -(ltn_add2r 1) 2!addn1 prednK //.
- Qed.
-
-End Computation.*)
\ No newline at end of file
diff --git a/util/ord_quantifier.v b/util/ord_quantifier.v
new file mode 100644
index 000000000..26aa8af30
--- /dev/null
+++ b/util/ord_quantifier.v
@@ -0,0 +1,101 @@
+Require Import rt.util.tactics.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
+
+(* Lemmas about the exists for Ordinals: [exists x, P x]. *)
+Section OrdExists.
+
+ Lemma exists_ord0:
+ forall P,
+ [exists x in 'I_0, P x] = false.
+ Proof.
+ 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 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 n P.
+ apply/idP/idP.
+ {
+ move => /exists_inP EX; destruct EX as [x IN Px].
+ destruct x as [x LT].
+ remember LT as LT'; clear HeqLT'.
+ rewrite ltnS leq_eqVlt in LT; move: LT => /orP [/eqP EQ | LT].
+ {
+ apply/orP; right.
+ unfold ord_max; subst x.
+ apply eq_trans with (y := P (Ordinal LT')); last by done.
+ by f_equal; apply ord_inj.
+ }
+ {
+ apply/orP; left.
+ apply/exists_inP; exists (Ordinal LT); first by done.
+ apply eq_trans with (y := P (Ordinal LT')); last by done.
+ by f_equal; apply ord_inj.
+ }
+ }
+ {
+ intro OR; apply/exists_inP.
+ move: OR => /orP [/exists_inP EX | MAX].
+ {
+ by destruct EX as [x IN Px]; exists (widen_ord (leqnSn n) x).
+ }
+ by exists ord_max.
+ }
+ Qed.
+
+End OrdExists.
+
+(* Lemmas about the forall for Ordinals: [exists x, P x]. *)
+Section OrdForall.
+
+ 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.
+
+ 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 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
--
GitLab