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

  predicate iq3_4_loc (oak : seq_voeu) (m : EnumMap.t) (i : int) =
    get_type_candidat oak[i] = NON_BOURSIER_HORS_SECTEUR ->
     (voeu_lt_than_queue oak[i] oak[i+1..] &&
      forall t. voeu_lt_than_queue oak[i] (EnumMap.get_queue m t))

  predicate iq3_4 (oak : seq_voeu) (m : EnumMap.t) =
    forall i. 0 <= i < length oak -> iq3_4_loc oak m i
end

module IQ3_4_Snoc
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.eligibles.ValidEligibles
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  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.enum_map.EnumMap

  use export IQ3_4

  let lemma iq3_4_snoc (cB cR : bool) (eligibles : PQueue.t) (oak : seq_voeu)	(om m : EnumMap.t) (x : voeu)
    requires {[@expl:pre iq3_4] iq3_4 oak om }
    requires {[@expl:alld m] enummap_all_distincts om }
    requires {[@expl:x selected] enummap_pop_v om m x }
    requires {[@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    ensures { iq3_4 (snoc oak x) m }
  =
    let s = snoc oak x in
    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> iq3_4_loc s m i }

      if k = length s - 1 then
      begin
        if not PQueue.is_empty eligibles then
	      begin
          meilleur_eligible_imp_pre_iq3 cB cR om eligibles x;
          assert {[@expl:iq3_4/meilleur nbhs < all] est_non_boursier_hors_secteur x
	                -> forall t. t <> NON_BOURSIER_HORS_SECTEUR -> voeu_lt_than_queue x (EnumMap.get_queue m t) };
          assert {[@expl:iq3_4/meilleur nbhs < all] get_type_candidat x = NON_BOURSIER_HORS_SECTEUR
	                -> voeu_lt_than_queue x (EnumMap.get_queue m NON_BOURSIER_HORS_SECTEUR) };
          assert {[@expl:iq3_4/meilleur nbhs < all] est_non_boursier_hors_secteur x
	                -> forall t. voeu_lt_than_queue x (EnumMap.get_queue m t) };
          assert {[@expl:iq3_4 k] iq3_4_loc s m k };
	      end;
      end else begin
        assert { forall i. 0 <= i <= k -> s[i..] == snoc oak[i..] x };
        assert { forall i. 0 <= i <= k -> s[i+1..] == snoc oak[i+1..] x };
        assert { forall i. 0 <= i <= k -> s[i] = oak[i] };

	      if est_non_boursier_hors_secteur s[k] then
	      begin
          assert {[@expl:iq3_4/suffix] iq3_4_loc oak om k };
	        assert {[@expl:iq3_4/suffix] voeu_lt s[k] x };
	        assert {[@expl:iq3_4/suffix] voeu_lt_than_queue s[k] (EnumMap.get_queue m BOURSIER_DU_SECTEUR) };
	        assert {[@expl:iq3_4/suffix] voeu_lt_than_queue s[k] (EnumMap.get_queue m BOURSIER_HORS_SECTEUR) };
	        assert {[@expl:iq3_4/suffix] voeu_lt_than_queue s[k] (EnumMap.get_queue m NON_BOURSIER_DU_SECTEUR) };
	        assert {[@expl:iq3_4/suffix] voeu_lt_than_queue s[k] (EnumMap.get_queue m NON_BOURSIER_HORS_SECTEUR) };
	        assert {[@expl:iq3_4/suffix] forall t. voeu_lt_than_queue s[k] (EnumMap.get_queue m t) };
	        assert {[@expl:iq3_4/suffix] voeu_lt_than_queue s[k] (snoc oak[k+1..] x) };
          assert {[@expl:iq3_4 k] iq3_4_loc s m k };
	      end;
      end;
    done
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)