- 17 Apr, 2022 1 commit
-
-
Pierre Roux authored
-
- 23 Feb, 2022 2 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
-
- 22 Feb, 2022 2 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
-
- 21 Feb, 2022 1 commit
-
-
Pierre Roux authored
-
- 18 Feb, 2022 3 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
- 09 Feb, 2022 1 commit
-
-
Pierre Roux authored
The new definition uses a left-closed interval, as in the book. The (wrong) theorem in the book is fixed by assuming the service curve beta is left continuous.
-
- 08 Feb, 2022 1 commit
-
-
Pierre Roux authored
-
- 25 Jan, 2022 1 commit
-
-
Pierre Roux authored
-
- 21 Dec, 2021 1 commit
-
-
Pierre Roux authored
The definition was specialized to non empty intervals open on the left and closed on the right (l, r].
-
- 20 Dec, 2021 2 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
* Compile with MathCOmp 1.13 * NC-Coq doesn't need CoqEAL since Minerve is now separated
-
- 13 Dec, 2021 2 commits
-
-
Pierre Roux authored
The two definitions are proved equivalent, the older one was more "computational" but this one is closer from the mathematical definition.
-
Pierre Roux authored
The two definitions are proved equivalent, the older one was more "computational" but this one is closer from the mathematical definition.
-
- 10 Dec, 2021 3 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
- 06 Dec, 2021 1 commit
-
-
Pierre Roux authored
-
- 22 Nov, 2021 1 commit
-
-
Pierre Roux authored
Now including dual extended real addition.
-
- 04 Nov, 2021 1 commit
-
-
Pierre Roux authored
It requires minerve to compile (which itself requires NCCoq, creating some kind of deadlock).
-
- 22 Oct, 2021 1 commit
-
-
Lucien RAKOTOMALALA authored
-
- 11 Oct, 2021 1 commit
-
-
Lucien RAKOTOMALALA authored
Update name in nc file and update old comment about previous S6 (now S5_2).
-
- 03 Oct, 2021 1 commit
-
-
Lucien RAKOTOMALALA authored
Replace UIB_departure with maximal_departure
-
- 27 Sep, 2021 1 commit
-
-
Lucien RAKOTOMALALA authored
It was using sequpp_min instead of sequpp_min' and was failing for instance on : sequpp_min {| sequpp_T := (12987 # 3125); sequpp_d := 1; sequpp_c := 20000; sequpp_js := [:: (0, (0%:E, (0, 0%:E))); ((3612 # 3125), (0%:E, (20000, 8000%:E)))] |}%bigQ {| sequpp_T := 2; sequpp_d := 1; sequpp_c := 0; sequpp_js := [:: (0, (0%:E, (0, 0%:E))); ((3612 / 3125), (0%:E, (0, +oo)))] |}%bigQ
-
- 24 Sep, 2021 3 commits
-
-
Lucien RAKOTOMALALA authored
Variables match with thesis. Min with delta 0 added to match with minerve.
-
Lucien RAKOTOMALALA authored
-
Lucien RAKOTOMALALA authored
To avoid having usual_functions depend on deviations.
-
- 23 Sep, 2021 1 commit
-
-
Pierre Roux authored
-
- 21 Sep, 2021 1 commit
-
-
- 13 Sep, 2021 1 commit
-
-
Pierre Roux authored
-
- 23 Aug, 2021 2 commits
-
-
Pierre Roux authored
Avoids having to local open scope after importing NCCoq.computation.tactic.
-
Pierre Roux authored
-
- 09 Aug, 2021 1 commit
-
-
Pierre Roux authored
CoqEAL 1.0.6 has a bug making typeclass search expensive.
-
- 01 Aug, 2021 2 commits
-
-
Pierre Roux authored
-
Pierre Roux authored
-
- 31 Jul, 2021 1 commit
-
-
Pierre Roux authored
Use abstract + vm_cast_no_check to avoid redoing the full check a second time during Qed.
-
- 30 Jul, 2021 1 commit
-
-
Pierre Roux authored
For instance, on the example below, f was extended to period 40000 by duplicating its period 40000 times, now it is done by just keeping its jump sequence unchanged since the function is affine after its initial segment. Require Import mathcomp.ssreflect.ssrbool mathcomp.ssreflect.order. Require Import NCCoq.computation.tactic. Local Open Scope ereal_scope. Local Open Scope order_scope. Local Open Scope F_scope. Let f := F_of_sequpp {| (* Conversion of upp([(0,0)0(1,0)[, period([(1,0)0(2,0)[), 0, 1) *) sequpp_T := 1; sequpp_d := 1; sequpp_c := 0; sequpp_js := [:: (0, ( (0)%:E, (0, (0)%:E))); (1, ( (0)%:E, (0, (0)%:E)))] |}%bigQ. Let g := F_of_sequpp {| (* Conversion of upp([(0,0)0(0,0)], period(](0,2560)0(40000,2560)]), 2560, 40000) *) sequpp_T := 20000; sequpp_d := 40000; sequpp_c := 2560; sequpp_js := [:: (0, ( (0)%:E, (0, (2560)%:E))); (20000, ( (2560)%:E, (0, (2560)%:E))); (40000, ( (2560)%:E, (0, (5120)%:E)))] |}%bigQ. Let h := F_of_sequpp {| (* Conversion of upp([(0,0)0(0,0)], period(](0,2560)0(40000,2560)]), 2560, 40000) *) sequpp_T := 20000; sequpp_d := 40000; sequpp_c := 2560; sequpp_js := [:: (0, ( (0)%:E, (0, (2560)%:E))); (20000, ( (2560)%:E, (0, (2560)%:E))); (40000, ( (2560)%:E, (0, (5120)%:E)))] |}%bigQ. Goal h = f + g. Proof. nccoq. Qed.
-