module IQ3_2
  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_2_loc (oak : seq_voeu) (m : EnumMap.t) (i : int) =
    not est_boursier oak[i] ->
    (voeu_lt_than_queue oak[i] (EnumMap.get_queue m NON_BOURSIER_DU_SECTEUR) &&
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] NON_BOURSIER_DU_SECTEUR)

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

module IQ3_2_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 proofs.ordre_appel.invariants.iqx.IQX
  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_2

  let lemma iq3_2_snoc (cB cR : bool) (eligibles : PQueue.t) (oak : seq_voeu)	(om m : EnumMap.t) (x : voeu)
    requires {[@expl:pre iq3_2] iq3_2 oak om }
    requires {[@expl:pre iqx_4] iqx_4 oak om }
    requires {[@expl:x selected] enummap_pop_v om m x }
    requires {[@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    ensures { iq3_2 (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_2_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_2/meilleur nb < nbds] est_non_boursier_du_secteur x -> voeu_lt_than_queue x m.nbds };
          assert {[@expl:iq3_2/meilleur nb < nbds] not est_boursier x -> voeu_lt_than_queue x m.nbds };
          assert {[@expl:iq3_2 k] iq3_2_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 not est_boursier s[k] then
	      begin
          assert {[@expl:iq3_2/suffix] iq3_2_loc oak om k };
	        assert {[@expl:iq3_2/suffix] get_type_candidat x = NON_BOURSIER_DU_SECTEUR -> voeu_lt oak[k] x };
          assert {[@expl:iq3_2/suffix] voeu_lt_than_typed_in_queue s[k] oak[k+1..] NON_BOURSIER_DU_SECTEUR };
  	      assert {[@expl:iq3_2/suffix] get_type_candidat x = NON_BOURSIER_DU_SECTEUR
  	              -> voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) NON_BOURSIER_DU_SECTEUR };
	        assert {[@expl:iq3_2/suffix] voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) NON_BOURSIER_DU_SECTEUR };
          assert {[@expl:iq3_2 k] iq3_2_loc s m k };
        end;
      end;
    done

  let lemma iq3_2_empty (oak : seq_voeu) (m : EnumMap.t)
    requires { oak = Seq.empty }
    ensures { iq3_2 oak m }
  =
    ()

end

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