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


module Q5
  use seq.Seq
  use int.Int
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  predicate q5a_loc (oa: seq_voeu) (k : int) =
    est_non_boursier_hors_secteur oa[k] ->
    forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] ->
      est_boursier oa[i] \/ est_du_secteur oa[i]

Q5 * * a) Un candidat non-boursier non-resident boursier qui a le rang r dans * le classement pedagogique ne double jamais personne

  predicate q5a (oa: seq_voeu) =
    forall k. 0 <= k < length oa -> q5a_loc oa k

  predicate q5a_aux_loc (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (k : int) =
    est_non_boursier_hors_secteur oa[k] ->
    forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> (in_Zb nb_b tx_b oa i \/ in_Zr nb_r tx_r oa i)

  predicate q5a_aux (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q5a_aux_loc nb_b nb_r tx_b tx_r oa k

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

  predicate q5b_loc (taux_b taux_ds : Taux.t) (oa : seq_voeu) (k : int) =
    taux_b + taux_ds < 100 -> est_non_boursier_hors_secteur oa[k] ->
       0 <= (100 - (taux_b + taux_ds)) * k <= 100 * (get_rang oa[k]) + 100

  predicate q5b (tx_b tx_r : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q5b_loc tx_b tx_r oa k

  predicate q5b_aux_loc (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (k : int) =
    est_non_boursier_hors_secteur oa[k] ->
    let nbCb = nb_contraintes_taux_b nb_b tx_b oa[..k] in
    let nbCds = nb_contraintes_taux_ds nb_r tx_r oa[..k] in
      k <= (get_rang oa[k]) - 1 + nbCb + nbCds

  predicate q5b_aux (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k < length oa -> q5b_aux_loc nb_b nb_r tx_b tx_r oa k

  predicate q5 (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) =
      q5a_aux nb_b nb_r tx_b tx_r oa && q5a oa &&
      q5b_aux nb_b nb_r tx_b tx_r oa && q5b tx_b tx_r oa

  let lemma q5a_aux_imp_q5a (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu)
    requires { q5a_aux nb_b nb_r tx_b tx_r oa }
    ensures { q5a oa }
  =
    assert { forall k. 0 <= k < length oa -> q5a_aux_loc nb_b nb_r tx_b tx_r oa k -> q5a_loc oa k }
end

module Q5_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 proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3

  use export Q5

  let lemma q5_up_to_rang_appel_oa (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa1 oa2 : seq_voeu)
    requires { q5 nb_b nb_ds tx_b tx_ds oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q5 nb_b nb_ds tx_b tx_ds oa2 }
  =
    for i = 0 to length oa2 - 1  do
      invariant { [@expl:q5a_aux_loc] forall k. 0 <= k < i -> q5a_aux_loc nb_b nb_ds tx_b tx_ds oa2 k }
      invariant { [@expl:q5a_loc] forall k. 0 <= k < i -> q5a_loc oa2 k }
      invariant { [@expl:q5b_aux_loc] forall k. 0 <= k < i -> q5b_aux_loc nb_b nb_ds tx_b tx_ds oa2 k }
      invariant { [@expl:q5b_loc]  forall k. 0 <= k < i -> q5b_loc tx_b tx_ds oa2 k }
      if not est_non_boursier_hors_secteur oa2[i] then
        continue;
      assert { est_non_boursier_hors_secteur oa1[i] };
      assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa1 i };
      assert { q5a_loc oa1 i };
      assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds oa1 i };
      assert { q5b_loc tx_b tx_ds 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 -> in_Zb nb_b tx_b oa1 k = in_Zb nb_b tx_b oa2 k };
      assert { forall k. 0 <= k < i -> voeu_lt oa2[i] oa2[k] -> (in_Zb nb_b tx_b oa2 k \/ in_Zr nb_ds tx_ds oa2 k)  };

      assert { nb_contraintes_taux_ds nb_b tx_b oa1[..i] = nb_contraintes_taux_ds nb_b tx_b oa2[..i] };
      assert { nb_contraintes_taux_ds nb_ds tx_ds oa1[..i] = nb_contraintes_taux_ds nb_ds tx_ds oa2[..i] }
    done
end

module Q5a_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 proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use Q5

  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 q5a_snoc1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (x : voeu)
    requires { q5a_aux nb_b nb_ds tx_b tx_ds oa }
    requires { est_non_boursier_hors_secteur x -> forall i. 0 <= i < length oa -> voeu_lt x oa[i] -> in_some_Z nb_b nb_ds tx_b tx_ds oa i }
    ensures { q5a_aux nb_b nb_ds tx_b 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 -> q5a_aux_loc nb_b nb_ds tx_b tx_ds s i }
      if k < length s - 1 then
      begin
        assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa k };
	      assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k }
      end else begin
        if est_non_boursier_hors_secteur x then
	      begin
	        assert { forall i. 0 <= i < length s -> voeu_lt x s[i] -> in_some_Z nb_b nb_ds tx_b tx_ds s i };
     	    assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k }
	      end
      end
    done

  let lemma q5a_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
     requires { iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m }
     requires { q5a_aux nb_b nb_ds tx_b tx_ds oa }
     ensures { q5a_aux nb_b nb_ds tx_b 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 -> q5a_aux_loc nb_b nb_ds tx_b tx_ds s i }
      if k < length s - 1 then
      begin
        assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa k };
        assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k }
      end
      else if est_non_boursier_hors_secteur x then
      begin
        assert { forall i. 0 <= i < k -> s[i+1..] == snoc oa[i+1..] x };
        assert { est_non_boursier_hors_secteur s[k] };
        assert { iq4_3b_loc nb_b nb_ds tx_b tx_ds s m k };
        assert { forall i. 0 <= i <= k ->
	         not in_some_Z nb_b nb_ds tx_b tx_ds s i ->
	         seq_contains s[k] s[i+1..] ->
	         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_some_Z nb_b nb_ds tx_b tx_ds oa i -> s[k] <> s[i] -> voeu_lt s[i] s[k]  };
        assert { forall i. 0 <= i < k -> voeu_lt s[k] s[i] -> in_some_Z nb_b nb_ds tx_b tx_ds oa i };
        assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k }
      end
    done
end

module Q5b_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 proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use Q5

  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 q5b_aux_snoc (nb_b nb_ds : int) (tx_b 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_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m }
    requires { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) }
    requires { q5b_aux nb_b nb_ds tx_b tx_ds oa }
    ensures { q5b_aux nb_b nb_ds tx_b
                          tx_ds oa }
    ensures { q5b_aux nb_b nb_ds tx_b 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 -> q5b_aux_loc nb_b nb_ds tx_b tx_ds s i }

      if not est_non_boursier_hors_secteur s[k] then
        continue;

      let nbCb_k = nb_contraintes_taux_b nb_b tx_b s[..k] in
      let nbCds_k = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in
      if k < length s -1 then
      begin
        assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds oa k };
        assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s k };
      end else begin
        let lt = ref Seq.empty in
        let gtb = ref Seq.empty in
        let gtds = ref Seq.empty in

  	    assert { q5a_aux_loc nb_b nb_ds tx_b 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 !gtb <= nb_contraintes_taux_b nb_b tx_b s[..i] <= nbCb_k }
          invariant { length !gtds <= nb_contraintes_taux_ds nb_ds tx_ds s[..i] <= nbCds_k }
          invariant { length !lt + length !gtb + length !gtds = 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 -> seq_forall (voeu_distinct !lt[j]) s[i..] };
            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 { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k };
            assert { in_Zb nb_b tx_b s i \/ in_Zr nb_ds tx_ds s i };
            seq_prefix_snoc s i;
            if in_Zb nb_b tx_b s i then
              gtb := snoc !gtb s[i]
            else
              gtds := snoc !gtds s[i]
            end;
        done;
	      assert { k = length !lt + length !gtb + length !gtds <= s[k].rang - 1 + nbCb_k + nbCds_k };
      end;
    done

  let lemma q5b_snoc (nb_b nb_ds : int) (tx_b 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 { tx_b+tx_ds < 100 }
    requires { all_distincts (snoc oa x) }
    requires { iq4_1 nb_ds tx_ds (snoc oa x) m }
    requires { iq4_2 nb_b tx_b (snoc oa x) m }
    requires { iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m }
    requires { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) }
    requires { q5b_aux nb_b nb_ds tx_b tx_ds oa }
    ensures { q5b tx_b 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 -> q5b_loc tx_b tx_ds s i }

      assert { iq4_1a_loc nb_ds tx_ds s k };
      assert { iq4_2a_loc nb_b tx_b s k };

      if est_non_boursier_hors_secteur s[k] then
      begin
        let nbCb = nb_contraintes_taux_b nb_b tx_b s[..k] in
        let nbCds = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in
        q5b_aux_snoc nb_b nb_ds tx_b tx_ds oa m x;
        assert { 100 * nbCb <= tx_b * k + 100 };
        assert { 100 * nbCds <= tx_ds * k + 100 };
        assert { 100 * (nbCb + nbCds) <= tx_b * k + tx_ds * k + 200 };
	      assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s k };

        assert {[@expl:to prove] k <= s[k].rang - 1 + nbCb + nbCds };
        assert { 100*(k + 1 - nbCb - nbCds) <= 100 * s[k].rang };
        assert { 0 <= (100 - (tx_b + tx_ds)) * k <= 100 * s[k].rang + 100};
      end;
    done
end

module Q5_Snoc
  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 proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3

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

  use Q5a_Lemmas
  use Q5b_Lemmas
  use export Q5

  let lemma q5_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu)
    requires { [@expl:pre q5 / rangs >= 1] 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang  }
    requires { [@expl:pre q5 / alld(oa.x)] all_distincts (snoc oa x) }
    requires { [@expl:pre q5 / iq4_1 (oa.x)] iq4_1 nb_ds tx_ds (snoc oa x) m }
    requires { [@expl:pre q5 / iq4_2 (oa.x)] iq4_2 nb_b tx_b (snoc oa x) m }
    requires { [@expl:pre q5 / iq4_3 (oa.x)] iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m }
    requires { [@expl:pre q5 / q5 oa] q5 nb_b nb_ds tx_b tx_ds oa }
    ensures { [@expl:q5(oa.x)] q5 nb_b nb_ds tx_b tx_ds (snoc oa x) }
  =
    q5a_snoc nb_b nb_ds tx_b tx_ds oa m x;
    if tx_b.tx + tx_ds.tx < 100 then
     q5b_snoc nb_b nb_ds tx_b tx_ds oa m x

  let lemma q5_empty (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu)
    requires { oa = Seq.empty }
    ensures { q5 nb_b nb_ds tx_b tx_ds oa  }
  =
    ()
end

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

Generated by why3doc 1.7.2+git