Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Module AbstractRTAReduction.

  Import UniprocessorSchedule.

  Section SearchSpace.

    Context {Task: eqType}.

    Section EquivalentFunctions.

      Context {T: eqType}.

      Variables f1 f2: nat → T.

      Variable B: nat.

      Definition are_equivalent_at_values_less_than :=
        ∀ x, x < B → f1 x = f2 x.

      Definition are_not_equivalent_at_values_less_than :=
        ∃ x, x < B ∧ f1 x ≠ f2 x.

    End EquivalentFunctions.

    Variable tsk: Task.

    Variable B: time.

    Variable interference_bound_function: Task → time → time → time.

    Definition is_in_search_space A :=
      A = 0 ∨
      0 < A < B ∧ are_not_equivalent_at_values_less_than
                     (interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.

    Section ExistenceOfRepresentative.

      Variable A: time.
      Hypothesis H_A_less_than_B: A < B.

      Lemma representative_exists:
        ∃ A_sp,
          A_sp ≤ A ∧
          are_equivalent_at_values_less_than (interference_bound_function tsk A)
                                             (interference_bound_function tsk A_sp) B ∧
          is_in_search_space A_sp.
      Proof.
        induction A as [|n].
        - ∃ 0; repeat split.
            by rewrite /is_in_search_space; left.
        - have ALT:
            all (fun t ⇒ interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
            ∨ has (fun t ⇒ interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
          { apply/orP.
            rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
            apply/negP; intros CONTR.
            move: CONTR ⇒ /andP [NALL /negP NHAS]; apply: NHAS.
              by rewrite -has_predC /predC in NALL.
          }
          feed IHn; first by apply ltn_trans with n.+1.
          move: IHn ⇒ [ASP [NEQ [EQ SP]]].
          move: ALT ⇒ [/allP ALT| /hasP ALT].
          { ∃ ASP; repeat split; try done.
            { by apply leq_trans with n. }
            { intros x LT.
              move: (ALT x) ⇒ T. feed T; first by rewrite mem_iota; apply/andP; split.
              move: T ⇒ /eqP T.
                by rewrite -T EQ.
            }
          }
          { ∃ n.+1; repeat split; try done.
            rewrite /is_in_search_space; right.
            split; first by apply/andP; split.
            move: ALT ⇒ [y IN N].
            ∃ y.
            move: IN; rewrite mem_iota add0n. move ⇒ /andP [_ LT].
            split; first by done.
            rewrite subn1 -pred_Sn.
            intros CONTR; move: N ⇒ /negP N; apply: N.
              by rewrite CONTR.
          }
      Qed.

    End ExistenceOfRepresentative.

    Section FixpointSolutionForAnotherA.

      Variables A_sp F_sp: time.
      Hypothesis H_less_than: A_sp + F_sp < B.
      Hypothesis H_fixpoint: A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).

      Variable A: time.
      Hypothesis H_bounds_for_A: A_sp ≤ A ≤ A_sp + F_sp.
      Hypothesis H_equivalent:
        are_equivalent_at_values_less_than
          (interference_bound_function tsk A)
          (interference_bound_function tsk A_sp) B.

      Lemma solution_for_A_exists:
        ∃ F,
          A_sp + F_sp = A + F ∧
          F ≤ F_sp ∧
          A + F = interference_bound_function tsk A (A + F).
      Proof.
        move: H_bounds_for_A ⇒ /andP [NEQ1 NEQ2].
        set (X := A_sp + F_sp) in ×.
        ∃ (X - A); split; last split.
        - by rewrite subnKC.
        - by rewrite leq_subLR /X leq_add2r.
        - by rewrite subnKC // H_equivalent.
      Qed.

    End FixpointSolutionForAnotherA.

  End SearchSpace.

End AbstractRTAReduction.