1. 17 Apr, 2022 1 commit
  2. 23 Feb, 2022 2 commits
  3. 22 Feb, 2022 2 commits
  4. 21 Feb, 2022 1 commit
  5. 18 Feb, 2022 3 commits
  6. 09 Feb, 2022 1 commit
  7. 08 Feb, 2022 1 commit
  8. 25 Jan, 2022 1 commit
  9. 21 Dec, 2021 1 commit
  10. 20 Dec, 2021 2 commits
  11. 13 Dec, 2021 2 commits
    • Pierre Roux's avatar
      Change the definition of flow_cc · 75d2a798
      Pierre Roux authored
      The two definitions are proved equivalent, the older one was more
      "computational" but this one is closer from the mathematical
      definition.
      75d2a798
    • Pierre Roux's avatar
      Change the definition of Fup · 2e7d7244
      Pierre Roux authored
      The two definitions are proved equivalent, the older one was more
      "computational" but this one is closer from the mathematical
      definition.
      2e7d7244
  12. 10 Dec, 2021 3 commits
  13. 06 Dec, 2021 1 commit
  14. 22 Nov, 2021 1 commit
  15. 04 Nov, 2021 1 commit
  16. 22 Oct, 2021 1 commit
  17. 11 Oct, 2021 1 commit
  18. 03 Oct, 2021 1 commit
  19. 27 Sep, 2021 1 commit
    • Lucien RAKOTOMALALA's avatar
      Fix incompleteness bug of sequpp_leb · 0e1ed3d0
      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
      0e1ed3d0
  20. 24 Sep, 2021 3 commits
  21. 23 Sep, 2021 1 commit
  22. 21 Sep, 2021 1 commit
  23. 13 Sep, 2021 1 commit
  24. 23 Aug, 2021 2 commits
  25. 09 Aug, 2021 1 commit
  26. 01 Aug, 2021 2 commits
  27. 31 Jul, 2021 1 commit
    • Pierre Roux's avatar
      Make Qed fast · 64079d3b
      Pierre Roux authored
      Use abstract + vm_cast_no_check to avoid redoing the full check a
      second time during Qed.
      64079d3b
  28. 30 Jul, 2021 1 commit
    • Pierre Roux's avatar
      Improve UPP_PA_JS_upto for affine functions · 95a7ba97
      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.
      95a7ba97