module IQ3_0
  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 voeu_lt_than_its_queue (v : VoeuClasse.t) (m : EnumMap.t) =
    voeu_lt_than_queue v (EnumMap.get_queue m (get_type_candidat v))

  predicate iq3_0_loc (oak : seq_voeu) (m : EnumMap.t) (i : int) =
    voeu_lt_than_its_queue oak[i] m &&
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] (get_type_candidat oak[i])

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

module IQ3_0_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_0

  let lemma iq3_0_snoc (cB cR : bool) (eligibles : PQueue.t) (oak : seq_voeu)	(om m : EnumMap.t) (x : VoeuClasse.t)
    requires {[@expl:pre iq3_0] iq3_0 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_0 (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_0_loc s m i }

      if k = length s - 1 then
      begin
        if not PQueue.is_empty eligibles then
        begin
          assert {[@expl:iq3_0/meilleur < its queue] voeu_lt_than_its_queue x m };
          assert {[@expl:iq3_0 k] iq3_0_loc s m k };
	      end else begin
	        assert { voeu_lt_than_queue s[k] (get_queue_of om s[k])[1..] };
          assert {[@expl:iq3_0 k] iq3_0_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 { forall i. 0 <= i <= k -> iq3_0_loc oak om i -> voeu_lt_than_its_queue oak[i] om };
        assert { forall i. 0 <= i <= k -> voeu_lt_than_its_queue oak[i] om };
        assert { voeu_lt_than_its_queue s[k] om };
        assert { voeu_lt_than_its_queue s[k] m };

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

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