Commit d985591a authored by Felipe Cerqueira's avatar Felipe Cerqueira

Organize util/ directory

parent a5cc6b86
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/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 ./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/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.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/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
# coq_makefile -R . rt ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.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/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/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 ./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/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.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/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
#
.DEFAULT_GOAL := all
......@@ -52,7 +52,7 @@ COQDOCLIBS?=-R . rt
OPT?=
COQDEP?=$(COQBIN)coqdep -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQCHKFLAGS?=-o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(COQBIN)coqc
GALLINA?=$(COQBIN)gallina
......@@ -80,10 +80,22 @@ endif
# #
######################
VFILES:=util/ssromega.v\
util/lemmas.v\
util/Vbase.v\
VFILES:=util/fixedpoint.v\
util/ssromega.v\
util/bigcat.v\
util/nat.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\
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_edf_theory.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.basic.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.schedulability.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.jitter.bertogna_edf_theory.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.interference
rt.model.jitter.workload rt.model.jitter.schedulability
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.jitter.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.platform_fp
rt.model.jitter.workload rt.model.jitter.schedulability rt.model.jitter.priority
......
Add LoadPath "../../" as rt.
Require Import rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.arrival_sequence rt.model.jitter.schedule
rt.model.jitter.interference rt.model.jitter.priority.
Require Import rt.analysis.jitter.workload_bound.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.schedule rt.model.jitter.priority rt.model.jitter.workload
rt.model.jitter.interference.
Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.task_arrival rt.model.jitter.response_time
rt.model.jitter.schedulability rt.model.jitter.workload.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.parallel.bertogna_edf_theory.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.analysis.parallel.bertogna_fp_theory.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.platform_fp
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.parallel.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.interference.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.schedulability.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase.
Require Import rt.util.all.
Require Import rt.model.basic.arrival_sequence rt.model.basic.job
rt.model.basic.task rt.model.basic.task_arrival.
Require Import rt.implementation.basic.task rt.implementation.basic.job.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task
rt.model.basic.schedule rt.model.basic.schedulability
rt.model.basic.priority rt.model.basic.platform.
......
Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.Vbase.
Require Import rt.model.basic.time rt.util.all.
Require Import rt.implementation.basic.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.arrival_sequence rt.model.basic.schedule
rt.model.basic.platform rt.model.basic.priority.
Require Import Program ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
......
Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.Vbase.
Require Import rt.model.basic.time rt.util.all.
Require Import rt.model.basic.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase.
Require Import rt.util.all.
Require Import rt.model.jitter.arrival_sequence rt.model.jitter.job
rt.model.jitter.task rt.model.jitter.task_arrival.
Require Import rt.implementation.jitter.task rt.implementation.jitter.job.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task
rt.model.jitter.schedule rt.model.jitter.schedulability
rt.model.jitter.priority rt.model.jitter.platform.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase.
Require Import rt.util.all.
Require Import rt.implementation.jitter.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.arrival_sequence rt.model.jitter.schedule
rt.model.jitter.platform rt.model.jitter.priority.
Require Import Program ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase.
Require Import rt.util.all.
Require Import rt.model.jitter.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.model.basic.job rt.model.basic.task rt.model.basic.time.
Require Import rt.util.all rt.model.basic.job rt.model.basic.task rt.model.basic.time.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* Definitions and properties of job arrival sequences. *)
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.workload.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference
rt.model.basic.arrival_sequence rt.model.basic.platform.
......
Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.model.basic.task rt.util.lemmas.
Require Import rt.model.basic.time rt.model.basic.task.
Require Import ssrnat ssrbool eqtype.
(* Properties of different types of job: *)
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival rt.model.basic.interference.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.interference
rt.model.basic.priority rt.model.basic.platform.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
Require Import ssreflect ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule.
Require Import ssreflect eqtype ssrbool ssrnat seq bigop.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas
Require Import rt.util.all
rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../../" as rt.
Require Import rt.model.basic.time rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.time rt.util.all.
Require Import ssrnat ssrbool eqtype fintype seq.
(* Attributes of a valid sporadic task. *)
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
Require Import ssreflect ssrbool eqtype ssrnat seq.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.response_time
rt.model.basic.schedulability.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.workload.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference
rt.model.jitter.arrival_sequence rt.model.jitter.platform.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.task_arrival rt.model.jitter.interference
rt.model.jitter.priority rt.model.jitter.platform.
......
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.arrival_sequence.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Add LoadPath ".." as rt.
Require Export rt.util.tactics.
Require Export rt.util.notation.
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.fixedpoint.
Require Export rt.util.induction.
Require Export rt.util.list.
Require Export rt.util.nat.
Require Export rt.util.powerset.
Require Export rt.util.sorting.
Require Export rt.util.ssromega.
Require Export rt.util.sum.
\ No newline at end of file
Add LoadPath ".." as rt.
Require Import rt.util.tactics rt.util.notation rt.util.bigord.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about the big concatenation operator. *)
Section BigCatLemmas.
Lemma mem_bigcat_nat:
forall (T: eqType) x m n j (f: _ -> list T),
m <= j < n ->
x \in (f j) ->
x \in \cat_(m <= i < n) (f i).
Proof.
intros T x m n j f LE IN; move: LE => /andP LE; des.
rewrite -> big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].
rewrite mem_cat; apply/orP; right.
destruct n; first by rewrite ltn0 in LE0.
rewrite big_nat_recl; last by ins.
by rewrite mem_cat; apply/orP; left.
Qed.
Lemma mem_bigcat_nat_exists :
forall (T: eqType) x m n (f: nat -> list T),
x \in \cat_(m <= i < n) (f i) ->
exists i, x \in (f i) /\
m <= i < n.
Proof.
intros T x m n f IN.
induction n; 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; des.
split; first by done.
by apply/andP; split; [by done | by apply ltnW].
}
{
exists n; split; first by done.
apply/andP; split; [by done | by apply ltnSn].
}
Qed.
Lemma mem_bigcat_ord:
forall (T: eqType) x n (j: 'I_n) (f: 'I_n -> list T),
j < n ->
x \in (f j) ->
x \in \cat_(i < n) (f i).
Proof.
intros T x n j f LE IN; rewrite (big_mkord_ord nil).
rewrite -(big_mkord (fun x => true)).
apply mem_bigcat_nat with (j := j);
[by apply/andP; split | by rewrite eq_fun_ord_to_nat].
Qed.
Lemma mem_bigcat_ord_exists :
forall (T: eqType) x n (f: 'I_n -> list T),
x \in \cat_(i < n) (f i) ->
exists i, x \in (f i).
Proof.
intros T x n f IN.
induction n; first by rewrite big_ord0 in_nil in IN.
{
rewrite big_ord_recr /= mem_cat in IN.
move: IN => /orP [HEAD | TAIL].
{
apply IHn in HEAD; destruct HEAD as [x0 IN].
by eexists (widen_ord _ x0); apply IN.
}
{
by exists ord_max; desf.
}
}
Qed.
Lemma bigcat_ord_uniq :
forall (T: eqType) n (f: 'I_n -> list T),
(forall i, uniq (f i)) ->
(forall x i1 i2,
x \in (f i1) -> x \in (f i2) -> i1 = i2) ->
uniq (\cat_(i < n) (f i)).
Proof.
intros T n f SINGLE UNIQ.
induction n; first by rewrite big_ord0.
{
rewrite big_ord_recr cat_uniq; apply/andP; split.
{
apply IHn; first by done.
intros x i1 i2 IN1 IN2.
exploit (UNIQ x);
[by apply IN1 | by apply IN2 | intro EQ; inversion EQ].
by apply ord_inj.
}
apply /andP; split; last by apply SINGLE.
{
rewrite -all_predC; apply/allP; intros x INx.
simpl; apply/negP; unfold not; intro BUG.
rewrite -big_ord_narrow in BUG.
rewrite big_mkcond /= in BUG.
have EX := mem_bigcat_ord_exists T x n.+1 _.
apply EX in BUG; clear EX; desf.
apply UNIQ with (i1 := ord_max) in BUG; last by done.
by desf; unfold ord_max in *; rewrite /= ltnn in Heq.
}
}
Qed.
Lemma map_bigcat_ord {T} {T'} n (f: 'I_n -> seq T) (g: T -> T') :
map g (\cat_(i < n) (f i)) = \cat_(i < n) (map g (f i)).
Proof.
destruct n; first by rewrite 2!big_ord0.
induction n; first by rewrite 2!big_ord_recr 2!big_ord0.
rewrite big_ord_recr [\cat_(cpu < n.+2)_]big_ord_recr /=.
by rewrite map_cat; f_equal; apply IHn.