module IQ3_3
  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_3_loc (oak : seq_voeu) (m : EnumMap.t) (i : int) =
    not est_du_secteur oak[i] ->
    voeu_lt_than_queue oak[i] (EnumMap.get_queue m BOURSIER_HORS_SECTEUR) &&
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] BOURSIER_HORS_SECTEUR

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

module IQ3_3_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_3

  let lemma iq3_3_snoc (cB cR : bool) (eligibles : PQueue.t) (oak : seq_voeu)	(om m : EnumMap.t) (x : voeu)
    requires {[@expl:pre iq3_3] iq3_3 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_3 (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_3_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_3/meilleur hs < bhs] not est_du_secteur x -> voeu_lt_than_queue x m.bhs };
          assert {[@expl:iq3_3 k] iq3_3_loc s m k };
	      end else begin
	        if not est_du_secteur s[k] then begin
     	      assert {[@expl:s(k) boursier] est_boursier_hors_secteur s[k] };
	          assert {[@expl:s(k) is head] enummap_v_is_head om s[k] };
	          assert { voeu_lt_than_queue s[k] om.bhs[1..] };
   	        assert { voeu_lt_than_queue s[k] m.bhs };
	          assert {[@expl:iq3_3 k] iq3_3_loc s m k };
	        end;
	      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_du_secteur s[k] then
	      begin
          assert {[@expl:iq3_3/suffix] iq3_3_loc oak om k };
	        assert {[@expl:iq3_3/suffix] get_type_candidat x = BOURSIER_HORS_SECTEUR -> voeu_lt oak[k] x };
          assert {[@expl:iq3_3/suffix] voeu_lt_than_typed_in_queue s[k] oak[k+1..] BOURSIER_HORS_SECTEUR };
  	      assert {[@expl:iq3_3/suffix] get_type_candidat x = BOURSIER_HORS_SECTEUR
  	              -> voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) BOURSIER_HORS_SECTEUR };
	        assert {[@expl:iq3_3/suffix] voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) BOURSIER_HORS_SECTEUR };
          assert {[@expl:iq3_3 k] iq3_3_loc s m k };
        end;
        assert {[@expl:iq3_3 k] iq3_3_loc s m k };
      end;
    done
end

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