Parcoursup / Calcul de l'ordre d'appel des candidats index


module Q4_2
  use int.Int
  use seq.Seq

  use proofs.ordre_appel.invariants.iq4_1.IQ4_1

  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

Q4.2 * * a) Un candidat non-resident boursier qui a le rang r dans le classement * pedagogique ne peut être double que par des residents, boursiers ou non,

  predicate q4_2a_loc (oa: seq_voeu) (k : int) =
    est_boursier_hors_secteur oa[k] ->
    forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> est_du_secteur oa[i]

  predicate q4_2a (oa: seq_voeu) =
    forall k. 0 <= k < length oa -> q4_2a_loc oa k

  predicate q4_2a_aux_loc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (k : int) =
    est_boursier_hors_secteur oa[k] ->
    forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] ->
      (est_du_secteur oa[i] && in_Zr nb_ds tx_ds oa i)

  predicate q4_2a_aux (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q4_2a_aux_loc nb_ds tx_ds oa k

  predicate q4_2b_loc (tx_ds : Taux.t) (oa : seq_voeu) (k : int) =
    est_boursier_hors_secteur oa[k] ->
       0 <= (100 - tx_ds) * k <= 100 * (get_rang oa[k])

* b) et a un rang dans l'ordre d'appel k inférieur ou egal à * 1 + floor((1 + tx_ds/(1-tx_ds))*r)

  predicate q4_2b (tx_ds : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q4_2b_loc tx_ds oa k

  predicate q4_2b_aux_loc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (k : int) =
    est_boursier_hors_secteur oa[k] ->
    let nbCb = nb_contraintes_taux_ds nb_ds tx_ds oa[..k] in
      k <= (get_rang oa[k]) - 1 + nbCb

  predicate q4_2b_aux (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q4_2b_aux_loc nb_ds tx_ds oa k

  predicate q4_2 (nb_ds : int)  (tx_ds : Taux.t) (oa : seq_voeu) =
      q4_2a_aux nb_ds tx_ds oa && q4_2a oa &&
      q4_2b_aux nb_ds tx_ds oa && q4_2b tx_ds oa

  let lemma q4_2a_aux_imp_q4_2a (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu)
    requires { q4_2a_aux nb_ds tx_ds oa }
    ensures { q4_2a oa }
  = assert { forall k. 0 <= k < length oa -> q4_2a_aux_loc nb_ds tx_ds oa k -> q4_2a_loc oa k }
end

module Q4_2_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1

  use export Q4_2

  let lemma q4_2_up_to_rang_appel_oa (nb_ds : int) (tx_ds : Taux.t) (oa1 oa2 : seq_voeu)
    requires { q4_2 nb_ds tx_ds oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q4_2 nb_ds tx_ds oa2 }
  =
    for i = 0 to length oa2 - 1  do
      invariant { [@expl:q4_2a_aux_loc] forall k. 0 <= k < i -> q4_2a_aux_loc nb_ds tx_ds oa2 k }
      invariant { [@expl:q4_2a_loc] forall k. 0 <= k < i -> q4_2a_loc oa2 k }
      invariant { [@expl:q4_2b_aux_loc] forall k. 0 <= k < i -> q4_2b_aux_loc nb_ds tx_ds oa2 k }
      invariant { [@expl:q4_2b_loc]  forall k. 0 <= k < i -> q4_2b_loc tx_ds oa2 k }

      if not est_boursier_hors_secteur oa2[i] then
        continue;

      assert { q4_2a_aux_loc nb_ds tx_ds oa1 i };
      assert { q4_2a_loc oa1 i };
      assert { q4_2b_aux_loc nb_ds tx_ds oa1 i };
      assert { q4_2b_loc tx_ds oa1 i };
      assert { est_boursier_hors_secteur oa1[i] };
      assert { forall k. 0 <= k < i -> in_Zr nb_ds tx_ds oa1 k = in_Zr nb_ds tx_ds oa2 k };
      assert { forall k. 0 <= k < i -> voeu_lt oa2[i] oa2[k] -> in_Zr nb_ds tx_ds oa2 k  };
      assert { nb_contraintes_taux_ds nb_ds tx_ds oa1[..i] = nb_contraintes_taux_ds nb_ds tx_ds oa2[..i] }
    done
end

module Q4_2a_Lemmas
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use Q4_2

  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  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

  let lemma q4_2a_snoc1 (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (x : voeu)
    requires { q4_2a_aux nb_ds tx_ds oa }
    requires { est_boursier_hors_secteur x -> (forall i. 0 <= i < length oa -> voeu_lt x oa[i] -> in_Zr nb_ds tx_ds oa i) }
    ensures { q4_2a_aux nb_ds tx_ds (snoc oa x) }
  = let s = snoc oa x in
    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> q4_2a_aux_loc nb_ds tx_ds s i }
      if k < length s - 1 then
      begin
        assert { q4_2a_aux_loc nb_ds tx_ds oa k };
	      assert { q4_2a_aux_loc nb_ds tx_ds s k }
      end
    done

  let lemma q4_2a_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
     requires { iq4_1 nb_ds tx_ds (snoc oa x) m }
     requires { q4_2a_aux nb_ds tx_ds oa }
     ensures { q4_2a_aux nb_ds tx_ds (snoc oa x) }
  =
    let s = snoc oa x in
    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> q4_2a_aux_loc nb_ds tx_ds s i }
      if k < length s - 1 then
      begin
        assert { q4_2a_aux_loc nb_ds tx_ds oa k };
        assert { forall i. 0 <= i < k -> s[i] = oa[i] };
        assert { s[..k] = oa[..k] };
        assert { q4_2a_aux_loc nb_ds tx_ds s k }
      end
      else if est_boursier_hors_secteur x then
      begin
        assert { forall i. 0 <= i < k -> s[i+1..] == snoc oa[i+1..] x };
	      assert { est_boursier_hors_secteur s[k] };
	      assert { iq4_1b_loc nb_ds tx_ds s m k };
        assert { forall i. 0 <= i < k -> not in_Zr nb_ds tx_ds s i ->
	         seq_contains s[k] s[i+1..] -> est_boursier s[k] ->
	         s[k] <> s[i] -> voeu_lt s[i] s[k] };
        seq_contains_suffix_snoc s[k] oa s;
        assert { forall i. 0 <= i < k -> not in_Zr nb_ds tx_ds s i -> s[i] <> s[k] -> voeu_lt s[i] s[k]  };
        assert { forall i. 0 <= i < k -> voeu_lt s[k] s[i] -> in_Zr nb_ds tx_ds s i };
        assert { q4_2a_aux_loc nb_ds tx_ds s k }
      end
    done
end

module Q4_2b_Lemmas
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use Q4_2

  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  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 ref.Ref
  use pigeon.Pigeonhole

  function pigeon_map (s : seq_voeu) (x : voeu) (i : int) : int =
     x.rang -1 - s[i].rang

  let lemma q4_2b_aux_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
    requires { 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang  }
    requires { all_distincts (snoc oa x) }
    requires { iq4_1 nb_ds tx_ds (snoc oa x) m }
    requires { q4_2a_aux nb_ds tx_ds (snoc oa x) }
    requires { q4_2b_aux nb_ds tx_ds oa }
    ensures { q4_2b_aux nb_ds tx_ds (snoc oa x) }
  =
    let s = snoc oa x in

    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> q4_2b_aux_loc nb_ds tx_ds s i }

      if not est_boursier_hors_secteur s[k] then
        continue;

      let nbCr_k = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in
      if k < length s -1 then
      begin
   	    assert { q4_2b_aux_loc nb_ds tx_ds oa k };
  	    assert { q4_2b_aux_loc nb_ds tx_ds s k };
      end else begin
        let lt = ref Seq.empty in
	      let gt = ref Seq.empty in
  	    assert { q4_2a_aux_loc nb_ds tx_ds s (k-1) };

        for i = 0 to k - 1 do
          invariant { forall j. 0 <= j < length !lt ->  1 <= !lt[j].rang }
          invariant { forall j. 0 <= j < length !lt -> voeu_lt !lt[j] s[k] }
          invariant { length !lt <= s[k].rang - 1 }
          invariant { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i..] }
          invariant { forall j. 0 <= j < length !lt -> seq_contains !lt[j] s }
          invariant { all_distincts !lt }
          invariant { length !gt <= nb_contraintes_taux_ds nb_ds tx_ds s[..i] <= nbCr_k }
          invariant { length !lt + length !gt = i }

          if voeu_lt s[i] s[k] then
          begin
            seq_suffix_cons s i;
            assert { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i+1..] };
            assert { forall j. 0 <= j < length !lt -> voeu_distinct !lt[j] s[i] };
            lt := snoc !lt s[i];
            assert { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i+1..] };
            assert { forall i j. 0 <= i < j < length !lt -> voeu_distinct !lt[i] !lt[j] };
            assert { seq_forall_two voeu_distinct !lt };
            assert { all_distincts !lt };

            if length !lt > Integer.to_int (s[k].rang - 1) then
            begin
              let n = length !lt in
              let m = Integer.to_int (s[k].rang - 1) in
              assert { forall j. 0 <= j < length !lt -> 1 <= !lt[j].rang < s[k].rang };
              assert { [@expl:pc pigeon hole] forall i. 0 <= i < n -> 0 <= s[k].rang -1 - !lt[i].rang < m };
              pigeonhole n m (pigeon_map !lt s[k]);
              assert { exists i1, i2. 0 <= i1 < i2 < n &&
                       pigeon_map !lt s[k] i1 = pigeon_map !lt s[k] i2
                       so !lt[i1].rang = !lt[i2].rang
                 so not voeu_distinct !lt[i1]!lt[i2] };
              absurd;
            end;
          end else begin
            assert { q4_2a_aux_loc nb_ds tx_ds s k };
            assert { in_Zr nb_ds tx_ds s i };
            seq_prefix_snoc s i;

            gt := snoc !gt s[i];
          end;

        done;
        assert { k = length !lt + length !gt <=  s[k].rang - 1 + nbCr_k };
      end;
    done

  let lemma q4_2b_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
    requires { 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang  }
    requires { all_distincts (snoc oa x) }
    requires { iq4_1 nb_ds tx_ds (snoc oa x) m }
    requires { q4_2a_aux nb_ds tx_ds (snoc oa x) }
    requires { q4_2b_aux nb_ds tx_ds oa }
    ensures { q4_2b tx_ds (snoc oa x) }
  =
    let s = snoc oa x in
    let taux_r = tx_ds in
    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> q4_2b_loc taux_r s i }

      assert { iq4_1a_loc nb_ds tx_ds s k };

      if est_boursier_hors_secteur s[k] then
      begin
        let nbCb = nb_contraintes_taux_ds nb_ds taux_r s[..k] in
        q4_2b_aux_snoc nb_ds tx_ds oa m x ;
        assert { 100 * nbCb <= taux_r * k + 100 };
	      assert { q4_2b_aux_loc nb_ds tx_ds s  k };
        assert { k <= s[k].rang - 1 + nbCb };
        assert { 100*(k + 1 - nbCb) <= 100 * s[k].rang };
        assert { 0 <= (100 - taux_r) * k <= 100 * s[k].rang };
      end
    done
end

module Q4_2_Snoc
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap

  use Q4_2a_Lemmas
  use Q4_2b_Lemmas
  use export Q4_2

  let lemma q4_2_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
    requires { [@expl:pre q4_2 / rangs >= 1] 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang  }
    requires { [@expl:pre q4_2 / alld(oa.x)] all_distincts (snoc oa x) }
    requires { [@expl:pre q4_2 / iq4_2 (oa.x)] iq4_1 nb_ds tx_ds (snoc oa x) m }
    requires { [@expl:pre q4_2 / q4_1 oa] q4_2 nb_ds tx_ds oa }
    ensures { q4_2 nb_ds tx_ds (snoc oa x) }
  = q4_2a_snoc nb_ds tx_ds oa m x;
    q4_2b_snoc nb_ds tx_ds oa m x

  let lemma q4_2_empty (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu)
    requires { oa = Seq.empty }
    ensures { q4_2 nb_ds tx_ds oa }
  =
    ()

end

(* generated on Thu Jan 30 02:06:23 UTC 2025 from rev:  *)

Generated by why3doc 1.7.2+git