Commit 97dc173f authored by Felipe Cerqueira's avatar Felipe Cerqueira

Finish main proof

parent 9a8b3009
This diff is collapsed.
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile apa.v divround.v eqtask_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v test.v Vbase.v WorkloadDefs.v
# coq_makefile apa.v BertognaResponseTimeDefs.v BertognaResponseTimeFP.v divround.v eqtask_dec.v extralib.v ExtraRelations.v helper.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v seq_nat_notation.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefs.v
#
.DEFAULT_GOAL := all
......@@ -81,7 +81,10 @@ endif
######################
VFILES:=apa.v\
BertognaResponseTimeDefs.v\
BertognaResponseTimeFP.v\
divround.v\
eqtask_dec.v\
extralib.v\
ExtraRelations.v\
helper.v\
......@@ -89,9 +92,9 @@ VFILES:=apa.v\
PlatformDefs.v\
PriorityDefs.v\
ResponseTimeDefs.v\
BertognaResponseTimeDefs.v\
SchedulabilityDefs.v\
ScheduleDefs.v\
ssromega.v\
TaskArrivalDefs.v\
TaskDefs.v\
Vbase.v\
......
......@@ -556,6 +556,32 @@ Proof.
Qed.
Lemma sorted_rcons_prefix :
forall {T: eqType} (leT: rel T) s x
(SORT: sorted leT (rcons s x)),
sorted leT s.
Proof.
ins; destruct s; simpl; first by ins.
rewrite rcons_cons /= rcons_path in SORT.
by move: SORT => /andP [PATH _].
Qed.
Lemma order_sorted_rcons :
forall {T: eqType} (leT: rel T) (s: seq T) (x last: T)
(TRANS: transitive leT) (SORT: sorted leT (rcons s last))
(IN: x \in s),
leT x last.
Proof.
ins; induction s; first by rewrite in_nil in IN.
simpl in SORT; move: IN; rewrite in_cons; move => /orP IN.
destruct IN as [HEAD | TAIL];
last by apply IHs; [by apply path_sorted in SORT| by ins].
move: HEAD => /eqP HEAD; subst a.
apply order_path_min in SORT; last by ins.
move: SORT => /allP SORT.
by apply SORT; rewrite mem_rcons in_cons; apply/orP; left.
Qed.
(*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
(x : nat) : T :=
match (x < n) with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment