module IQX
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts

  (*
   * Invariant qui lie la taille du groupe de classement, de l'ordre d'appel
   * courant et des files de voeux
   *)
  predicate iqx_0 (nb_v nb_b nb_ds : int) (oa : seq_voeu) (m : EnumMap.t) =
    nb_v = Seq.length oa + EnumMap.get_nb_voeux_classes m &&
    nb_b = SeqVoeux.nb_boursiers oa + EnumMap.get_nb_boursiers m &&
    nb_ds = SeqVoeux.nb_du_secteur oa + EnumMap.get_nb_du_secteur m

  predicate iqx_2_loc (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (i : int) =
    taux_b_contraignant tx_b oa[..i] nb_b -> est_boursier oa[i]

  predicate iqx_2 (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) =
    forall i. 0 <= i < length oa ->
      taux_b_contraignant tx_b oa[..i] nb_b -> est_boursier oa[i]

  let lemma iqx_2_equiv (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu)
    ensures { iqx_2 nb_b tx_b oa <-> forall i. 0 <= i < length oa -> iqx_2_loc nb_b tx_b oa i }
  =
    for i = 0 to length oa-1 do
      invariant { forall j. 0 <= j < i -> (taux_b_contraignant tx_b oa[..j] nb_b  -> est_boursier oa[j])
		              <-> iqx_2_loc nb_b tx_b oa j }
    done

  predicate iqx_3ds_loc (nb_ds : int) (oa : seq_voeu) (k : int) =
    not remains_du_secteur oa[..k] nb_ds -> hors_secteur_seulement oa[k..]

  predicate iqx_3ds (nb_ds : int) (oa : seq_voeu) =
    forall k. 0 <= k <= length oa -> iqx_3ds_loc nb_ds oa k

  predicate iqx_3b_loc (nb_b : int) (oa : seq_voeu) (k : int) =
    not remains_boursiers oa[..k] nb_b -> non_boursiers_seulement oa[k..]

  predicate iqx_3b (nb_b : int) (oa : seq_voeu) =
    forall k. 0 <= k <= length oa -> iqx_3b_loc nb_b oa k

  predicate iqx_3 (nb_b nb_ds : int) (oa : seq_voeu) =
    iqx_3b nb_b oa && iqx_3ds nb_ds oa

  predicate iqx_4 (oa : seq_voeu) (m : EnumMap.t) =
    enummap_seq_all_distincts oa m

  predicate iqx_5 (oa : seq_voeu) (m : EnumMap.t) =
    (forall i. 0 <= i < Seq.length oa -> get_rang oa[i] >= 1) &&
    (forall v. enummap_contains m v -> get_rang v >= 1)

end

module IQX_Snoc
  use int.Int
  use set.Fset
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.eligibles.Eligibles
  use proofs.ordre_appel.eligibles.ValidEligibles
  use proofs.ordre_appel.invariants.iq0.IQ0
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts
  use export IQX

  let lemma om_m_move (oa : seq_voeu) (om m : EnumMap.t) (x : voeu) (nbb nbr : int)
    requires { nbb = SeqVoeux.nb_boursiers oa + EnumMap.get_nb_boursiers om }
    requires { nbr = SeqVoeux.nb_du_secteur oa + EnumMap.get_nb_du_secteur om }
    requires { [@expl:alld m] enummap_all_distincts om }
    requires { [@expl:x selected] enummap_pop_v om m x }
    ensures { nbb = SeqVoeux.nb_boursiers (snoc oa x) + EnumMap.get_nb_boursiers m }
    ensures { nbr = SeqVoeux.nb_du_secteur (snoc oa x) + EnumMap.get_nb_du_secteur m }
  =
    if est_boursier x then begin
      assert { SeqVoeux.nb_boursiers (snoc oa x) + EnumMap.get_nb_boursiers m =
               (SeqVoeux.nb_boursiers oa + 1) + (EnumMap.get_nb_boursiers om) - 1 = nbb };
    end;
    if est_du_secteur x then begin
      assert { SeqVoeux.nb_du_secteur (snoc oa x) + EnumMap.get_nb_du_secteur m =
               (SeqVoeux.nb_du_secteur oa + 1) + (EnumMap.get_nb_du_secteur om) - 1 = nbr };
    end

  let lemma iqx_0_snoc (nb_v nb_b nb_ds : int) (oa : seq_voeu) (om m : EnumMap.t) (x : voeu)
    requires { [@expl:iqx0 oa] iqx_0 nb_v nb_b nb_ds oa om }
    requires { [@expl:alld m] enummap_all_distincts om }
    requires { [@expl:x selected] enummap_pop_v om m x }

    ensures { iqx_0 nb_v nb_b nb_ds (snoc oa x) m }
    ensures { est_boursier x -> nb_b > 0 }
    ensures { est_du_secteur x -> nb_ds > 0 }
    ensures { est_boursier x -> remains_boursiers oa nb_b }
    ensures { est_du_secteur x -> remains_du_secteur oa nb_ds }
  =
    om_m_move oa om m x nb_b nb_ds

  let lemma iqx_0_empty (op oak : seq_voeu) (m : EnumMap.t )
    requires { iq0 op oak m }
    requires { length op = get_nb_voeux_classes m}
    requires { nb_boursiers op = EnumMap.get_nb_boursiers m}
    requires { nb_du_secteur op = EnumMap.get_nb_du_secteur m}
    requires { oak = Seq.empty }
    ensures { iqx_0 (length op) (nb_boursiers op) (nb_du_secteur op) oak m }
  =
    ()

  (* IQ1/L3 *)
  let lemma iqx_2_snoc (cB cR : bool) (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (om : EnumMap.t)
                       (eligibles: PQueue.t) (x : voeu)
    requires { [@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    requires { [@expl:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oa nb_b }
    requires { [@expl:iqx_2(oa)] iqx_2 nb_b tx_b oa }
    ensures { iqx_2 nb_b tx_b (snoc oa x) }
  =
    let s' = snoc oa x in
    for i = 0 to length s'-1 do
      invariant { forall j. 0 <= j < i -> iqx_2_loc nb_b tx_b s' j }
      if i < length s'-1 then
        assert { iqx_2_loc nb_b tx_b oa i }
      else if taux_b_contraignant tx_b s'[..i] nb_b then
      begin
        assert { cB && s'[i] = x };
	      assert { not Fset.is_empty eligibles -> est_eligible_p cB cR x };
	      assert { Fset.is_empty eligibles -> est_boursier_hors_secteur s'[i] };
      end else
        assert { iqx_2_loc nb_b tx_b s' i }
    done

  let lemma iqx_2_prefix (nb_b : int) (tx_b : Taux.t) (s : seq_voeu)
    requires { iqx_2 nb_b tx_b s }
    ensures { forall i. 0 <= i < length s -> iqx_2 nb_b tx_b s[..i] }
  = ()

  let lemma iqx_3ds_snoc (nb_v nb_b nb_ds : int) (oa : seq_voeu) (om m : EnumMap.t) (x : voeu)
    requires { iqx_0 nb_v nb_b nb_ds oa om }
    requires { [@expl:x selected] enummap_pop_v om m x }
    requires { [@expl:iqx_3ds(oa)] iqx_3ds nb_ds oa }
    ensures { iqx_3ds nb_ds (snoc oa x) }
  =
    assert { [@expl:x ds -> remains ds] est_du_secteur x -> remains_du_secteur oa nb_ds };
    let s = snoc oa x in
    if est_du_secteur x then
    begin
      assert { forall k. 0 <= k < length s -> s[..k] == oa[..k] };
      assert { iqx_3ds_loc nb_ds s (length s) };
      assert { forall k. 0 <= k <= length s -> iqx_3ds_loc nb_ds s k };
      return;
    end;
    for k = 0 to length s do
      invariant { forall i. 0 <= i < k -> iqx_3ds_loc nb_ds s i }
      assert { est_hors_secteur x };
      if k < length s then
      begin
        if not remains_du_secteur oa[..k] nb_ds then begin
          assert { hors_secteur_seulement (snoc oa[k..] x) };
          hors_secteur_seulement_snoc oa[k..] x;
          assert { s[k..] == snoc oa[k..] x };
          assert { hors_secteur_seulement s[k..] };
	      end;
      end else
        assert { iqx_3ds_loc nb_ds s k };
    done

  let lemma iqx_3b_snoc (nb_v nb_b nb_ds : int) (oa : seq_voeu) (om m : EnumMap.t) (x : voeu)
    requires { iqx_0 nb_v nb_b nb_ds oa om }
    requires { [@expl:x selected] enummap_pop_v om m x }
    requires { [@expl:iqx_3b(oa)] iqx_3b nb_b oa }
    ensures { iqx_3b nb_b (snoc oa x) }
  =
    assert { [@expl:x b -> remains b] est_boursier x -> remains_boursiers oa nb_b };
    let s = snoc oa x in
    for k = 0 to length s do
      invariant { forall i. 0 <= i < k -> iqx_3b_loc nb_b s i }
      if k <= length s - 1 then begin
         if est_boursier x then begin
           assert { remains_boursiers oa[..k] nb_b };
           assert { remains_boursiers s[..k] nb_b };
           assert { iqx_3b_loc nb_b s k };
         end else if not remains_boursiers oa[..k] nb_b then begin
	         assert { non_boursiers_seulement (snoc oa[k..] x) };
           non_boursiers_seulement_snoc oa[k..] x;
	         assert { s[k..] == snoc oa[k..] x };
           assert { non_boursiers_seulement s[k..] };
           assert { iqx_3b_loc nb_b oa k };
           assert { iqx_3b_loc nb_b s k };
	       end;
      end else begin
        assert { iqx_3b_loc nb_b s k };
      end
    done

  let lemma iqx_3_snoc (nb_v nb_b nb_ds : int) (oa : seq_voeu) (om m : EnumMap.t) (x : voeu)
    requires { iqx_0 nb_v nb_b nb_ds oa om }
    requires { [@expl:x selected] enummap_pop_v om m x }
    requires { [@expl:iqx_3(oa)] iqx_3 nb_b nb_ds oa }
    ensures { iqx_3 nb_b nb_ds (snoc oa x)  }
  =
    iqx_3b_snoc nb_v nb_b nb_ds oa om m x;
    iqx_3ds_snoc nb_v nb_b nb_ds oa om m x

  let lemma iqx_3_empty (op oak : seq_voeu) (m : EnumMap.t)
    requires { iq0 op oak m }
    requires { oak = Seq.empty }
    ensures { iqx_3 (nb_boursiers op) (nb_du_secteur op) oak }
  =
    ()

  let lemma iqx_4_snoc (s : seq_voeu) (om m : EnumMap.t) (x : voeu)
    requires {[@expl:alld(om)] enummap_all_distincts om }
    requires {[@expl:alld(s)] all_distincts s }
    requires {[@expl:alld(om + s)] enummap_seq_distincts om s }
    requires {[@expl:x = om-m] enummap_contains om x && not enummap_contains m x }
    requires {[@expl:m included in om] forall v. enummap_contains m v -> enummap_contains om v }
    ensures { enummap_seq_distincts m (snoc s x) }
    ensures { enummap_all_distincts m }
    ensures { all_distincts (snoc s x) }
  = let s' = snoc s x in
    assert { forall i. 0 <= i < length s'-1 -> voeu_distinct s'[i] x };
    alld_snoc x s

  let lemma iqx_4_empty (op oak : seq_voeu) (m : EnumMap.t)
    requires { seq_groupe_ok op }
    requires { seq_rangs_sorted op }
    requires { iq0 op oak m }
    requires { oak = Seq.empty }
    ensures { iqx_4 oak m }
  =
    assert { enummap_all_distincts m }

  let lemma iqx_5_snoc (oa : seq_voeu) (om m : EnumMap.t) (x : voeu)
    (* requires {[@expl:alld(om)] enummap_all_distincts om }
    requires {[@expl:alld(s)] all_distincts s }
    requires {[@expl:alld(om + s)] enummap_seq_distincts om s }
    requires { [@expl:x = om-m] enummap_contains om x && not enummap_contains m x }
    requires { [@expl:m included in om] forall v. enummap_contains m v -> enummap_contains om v } *)
    requires { [@expl:pre iqx_5 / pop v] enummap_pop_v om m x }
    requires { [@expl:pre iqx_5 / iqx_5] iqx_5 oa om }
    ensures { iqx_5 (snoc oa x) m }
  = let s = snoc oa x in
    assert { s[length s - 1] = x };
    assert { enummap_contains om x };
    assert { get_rang x >= 1 };
    assert { forall i. 0 <= i < length s -> 1<= get_rang s[i] }

  let lemma iqx_5_empty (op s : seq_voeu) (m : EnumMap.t )
    requires { seq_groupe_ok op }
    requires { seq_rangs_sorted op }
    requires { iq0 op s m }
    requires { s = Seq.empty }
    ensures { iqx_5 s m }
  =
    assert { seq_rangs_ge_1 op };
    assert { forall v. enummap_contains m v -> seq_contains v op };
    assert { forall v. seq_contains v op -> get_rang v >= 1 };
    ()

end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)