module IQ3_1
  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_1_loc (oak : seq_voeu) (m : EnumMap.t) (i : int) =
    voeu_lt_than_queue oak[i] (EnumMap.get_queue m BOURSIER_DU_SECTEUR) &&
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] BOURSIER_DU_SECTEUR

  predicate iq3_1 (oak : seq_voeu) (m : EnumMap.t) =
    forall i. 0 <= i < length oak -> iq3_1_loc oak m i

end

module IQ3_1_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_1

  let lemma iq3_1_snoc (cB cR : bool) (eligibles : PQueue.t) (oak : seq_voeu)	(om m : EnumMap.t) (x : voeu)
    requires {[@expl:pre iq3_1] iq3_1 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_1 (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_1_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_1/meilleur < bds] voeu_lt_than_queue x m.bds };
          assert {[@expl:iq3_1 k] iq3_1_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] };

        assert {[@expl:iq3_1/suffix] iq3_1_loc oak om k };
	      assert {[@expl:iq3_1/suffix] (get_type_candidat x) = BOURSIER_DU_SECTEUR -> voeu_lt oak[k] x };
	      assert {[@expl:iq3_1/suffix] voeu_lt_than_typed_in_queue s[k] oak[k+1..] BOURSIER_DU_SECTEUR };
	      assert {[@expl:iq3_1/suffix] (get_type_candidat x) = BOURSIER_DU_SECTEUR
	              -> voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) BOURSIER_DU_SECTEUR };
	      assert {[@expl:iq3_1/suffix] voeu_lt_than_typed_in_queue s[k] (snoc oak[k+1..] x) BOURSIER_DU_SECTEUR };
        assert {[@expl:iq3_1 k] iq3_1_loc s m k };
      end;
    done
end

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