Parcoursup / Calcul de l'ordre d'appel des candidats index
module P4 use int.Int use seq.Seq use proofs.lib.seq.Seq use proofs.lib.permutation.Permutation use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxInversions use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use proofs.ordre_appel.properties.q1.Q1 predicate p4 (tx_b tx_r : Taux.t) (s : seq_voeu) = tx_r = 0 -> forall p : permutation. length s = p.n -> let sp = permut s p in q1 tx_b sp -> nb_inversions s <= nb_inversions sp end
module P4_UpToRangAppel use int.Int use seq.Seq use proofs.lib.pair.Pair use proofs.lib.permutation.Permutation use proofs.lib.sum2d.Sum2d use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxInversions 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.properties.q1.Q1 use proofs.ordre_appel.properties.q1.Q1_UpToRangAppel use proofs.ordre_appel.properties.p5.P5_UpToRangAppel use export P4 let rec lemma nb_inversions_up_to_rang_appel (s1 s2 : seq_voeu) requires { seq_voeu_eq_up_to_rang_appel s1 s2 } ensures { nb_inversions s1 = nb_inversions s2 } variant { length s1 } = let n = length s1 in if n <= 1 then return; assert { forall p. inversions_count s1 p = inversions_count s2 p }; assert { sum2d (inversions_count s1) n n = sum2d (inversions_count s2) n n } let lemma p4_up_to_rang_appel_oa (tx_b tx_r : Taux.t) (oa1 oa2 : seq_voeu) requires { p4 tx_b tx_r oa1 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { p4 tx_b tx_r oa2 } = if Taux.to_int tx_r > 0 then return; let lemma aux (p : permutation) (oa2p : seq_voeu) requires { p.n = length oa2 } requires { oa2p = permut oa2 p } requires { q1 tx_b oa2p } ensures { nb_inversions oa2 <= nb_inversions oa2p } = let oa1p = permut oa1 p in assert { seq_voeu_eq_up_to_rang_appel oa1p oa2p }; q1_up_to_rang_appel_oa tx_b oa2p oa1p; assert { q1 tx_b oa1p }; () in () end module P4_Lemmas use int.Int use seq.Seq use proofs.lib.seq.Seq use proofs.lib.permutation.Permutation use proofs.lib.permutation.Swap use proofs.lib.sum2d.SumBasics use proofs.lib.pair.Pair use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts use proofs.ordre_appel.seq_voeux.SeqVoeuxInversions use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use proofs.ordre_appel.seq_voeux.NbBoursiers use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.properties.q1.Q1 use proofs.ordre_appel.properties.p5.P5_Lemmas use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props use P4
(* * Le nombre d'inversion est positif. *) let lemma nb_inv_pos (d : seq_voeu) ensures { nb_inversions d >= 0 } = () (* * Pas d'inversion pour un sequence vide ou un singleton. *) let lemma nb_inv_small (d : seq_voeu) requires { length d <= 1 } ensures { nb_inversions d = 0 } = () (* * Le swap d'une inversion diminue le nombre total d'inversions. * Prouvé dans le module Inversions. * Egalement prouvé en Coq. *) let lemma p4_dec_inv (s : seq_voeu) (i j : int) requires { 0 <= i < j < length s } requires { voeu_lt s[j] s[i] } ensures { nb_inversions (swap s (mkp i j)) < nb_inversions s } = inversions_dec s (mkp i j) (* * Effet de 'swap' sur le nombre de boursiers dans un préfixe de longueur 'k'. *) let lemma swap_nb_boursiers (d : seq_voeu) (i j k : int) requires { 0 <= i < j < length d } requires { 0 <= k <= length d } ensures { let d' = (swap d (mkp i j)) in if i < k <= j then let x = (if est_boursier d[i] then 1 else 0) in let y = (if est_boursier d[j] then 1 else 0) in nb_boursiers d[..k] = nb_boursiers d'[..k] + x - y else nb_boursiers d[..k] = nb_boursiers d'[..k] } = let d' = (swap d (mkp i j)) in let x = (nb_boursiers d[i..i+1]) in let y = (nb_boursiers d[j..j+1]) in for l = 0 to k-1 do invariant { forall k'. 0 <= k' <= l -> if i < k' <= j then nb_boursiers d[..k'] = nb_boursiers d'[..k'] + x - y else nb_boursiers d[..k'] = nb_boursiers d'[..k'] } begin let dk = nb_boursiers d[..l] - nb_boursiers d'[..l] in let dk1 = nb_boursiers d[..l+1] - nb_boursiers d'[..l+1] in let xk = nb_boursiers d[l..l+1] in let yk = nb_boursiers d'[l..l+1] in assert { dk1 = dk + xk - yk }; assert { l <> i /\ l <> j -> xk = yk }; assert { l <> i /\ l <> j -> dk1 = dk }; assert { l = i -> (dk = 0) /\ dk1 = x - y}; assert { l = j -> (dk = (x - y)) /\ dk1 = (x - y) + (y - x) = 0 }; end done let lemma nbs_helper (s : seq_voeu) (k :int) requires { 0 <= k < length s } requires { non_boursiers_seulement s[k..] } ensures { est_non_boursier s[k] } ensures { non_boursiers_seulement s[k+1..] } =( assert { s[k] = s[k..][0] } ) let lemma nbs_helper2 (s : seq_voeu) (k :int) requires { 0 <= k < length s } requires { est_non_boursier s[k] } requires { non_boursiers_seulement s[k+1..] } ensures { non_boursiers_seulement s[k..] } =( ) (* * 'swap' préserve le nombre de non-boursiers sur un suffixe ne contenant * que des non boursiers. *) let rec lemma swap_preserve_non_boursiers (s : seq_voeu) (i j k : int) requires { 0 <= i < j < length s } requires { est_boursier s[i] -> est_boursier s[j] } requires { 0 <= k < length s } requires { non_boursiers_seulement s[k..] } ensures { non_boursiers_seulement (swap s (mkp i j))[k..] } variant { length s - k } = let sp = (swap s (mkp i j)) in if k < length s - 1 then swap_preserve_non_boursiers s i j (k+1); (* induction hypothesis *) assert { non_boursiers_seulement sp[k+1..] }; nbs_helper s k; assert { non_boursiers_seulement s[k+1..] }; (* induction step *) if k <> i && k <> j then begin assert { sp[k] = s[k] }; nbs_helper s k; assert { est_non_boursier s[k] }; end else if k = i then begin assert { sp[k] = s[k..][j-k] }; assert { est_non_boursier s[k..][j-k] }; end else (* k = j *) begin assert { sp[k] = s[i] }; assert { est_non_boursier sp[k] }; end; assert { est_non_boursier sp[k] }; nbs_helper2 sp k (* * 'swap' préserve Q1 *) let function taux_ok (taux_p: int) (nb_p: int) (nb_total: int) = 100 * nb_p >= taux_p * nb_total let lemma swap_preserve_q1 (tx_b: Taux.t) (s : seq_voeu) (i j k: int) requires { 0 <= i < j < length s } requires { 0 <= k < length s } requires { q1_loc tx_b s k } requires { est_boursier s[i] -> est_boursier s[j]} ensures { q1_loc tx_b (swap s (mkp i j)) k } = let sp = (swap s (mkp i j)) in if non_boursiers_seulement s[k..] then begin swap_preserve_non_boursiers s i j k; assert { non_boursiers_seulement sp[k..] }; end else swap_nb_boursiers s i j k (* * Si les types de voeux correspondent deux à deux dans d et d' * alors 'non_boursiers_seulement' a la même valeur pour les deux séquences. *) let rec lemma meme_non_boursiers_seulement (d d' : seq_voeu) (l : int) requires { 0 <= l <= length d = length d'} requires { forall k. l <= k < length d -> est_boursier d[k] <-> est_boursier d'[k] } ensures { non_boursiers_seulement d[l..] = non_boursiers_seulement d'[l..] } variant { length d - l } = if l < length d then begin meme_non_boursiers_seulement d d' (l+1); assert { est_non_boursier d[l] <-> est_non_boursier d'[l] } end (* * Si deux séquences sont égales elles respectent toutes les deux Q1. *) let lemma meme_q1 (tx_b : Taux.t) (d d' : seq_voeu) requires { length d = length d'} requires { forall k. 0 <= k < length d -> d[k] = d'[k] } ensures { q1 tx_b d = q1 tx_b d'} = assert { d == d' } (* * Si deux séquences sont égales elles ont le même nombre d'inversions. *) let lemma meme_nb_inversions (d d' : seq_voeu) requires { length d = length d'} requires { d == d' } ensures { nb_inversions d = nb_inversions d' } = () (* * 'swap' et 'transposition' ont le même effet. *) let lemma swap_carac (s : seq_voeu) (i j : int) requires { 0 <= i < j < length s } ensures { let n = length s in let t = transposition n i j in let d' = permut s t in let dij = (swap s (mkp i j)) in d' == dij } = ( let n = length s in let t = transposition n i j in let d' = permut s t in let dij = (swap s (mkp i j)) in for k = 0 to n-1 do invariant { forall k'. 0<= k' < k -> d'[k'] = dij[k'] } () done ) let lemma swap_carac2 (s : seq_voeu) (p : permutation) (i j : int) requires { 0 <= i < j < p.n } requires { p.n = length s } ensures { let p' = compose (transposition p.n i j) p in let d' = permut s p' in let dij = (swap (permut s p) (mkp i j)) in d' == dij } = (swap_carac (permut s p) i j) (* * Si on application 'p' à l'ordre d'appel alors Q1 est maintenue. *) predicate satisfait_q1 (tx_b : Taux.t) (ordre_appel: seq_voeu) (p : permutation) = let d = (permut ordre_appel p) in p.n = length ordre_appel /\ q1 tx_b d (* * La séquence 'd' est équitable pour les voeux 'i' et 'j' *) predicate is_fair_loc_seq (d: seq_voeu) (i j: int) = (i < j && voeu_lt d[j] d[i]) -> (est_boursier d[i] && est_non_boursier d[j]) (* * La permutation 'p' de l'ordre d'appel 'oa' est équitable pour 'i' et 'j' *) predicate is_fair_loc (d: seq_voeu) (p: permutation) (i j: int) = let d' = (permut d p) in is_fair_loc_seq d' i j predicate is_fair (d : seq_voeu) = forall i j. 0 <= i < j < length d -> is_fair_loc_seq d i j predicate satq1_and_is_fair (tx_b : Taux.t) (d : seq_voeu) (p: permutation) = satisfait_q1 tx_b d p /\ let d' = (permut d p) in is_fair d' (* * Si 'p' est une permutation de l'ordre d'appel qui satisfait Q1 mais qui * n'est pas équitable pour les candidats 'i' et 'j' alors * il existe une autre permutation de l'ordre d'appel qui satisfait Q1 * mais qui contient moins d'inversions que 'p'. Il suffit de composer 'p' * la permutation qui échange 'i' et 'j'. *) let lemma loc_improve (tx_b : Taux.t) (ordre_appel : seq_voeu) (p : permutation) (i j : int) : permutation requires { 0 <= i < j < p.n } requires { p.n = length ordre_appel } requires { satisfait_q1 tx_b ordre_appel p } requires { not is_fair_loc ordre_appel p i j } ensures { satisfait_q1 tx_b ordre_appel result } ensures { nb_inversions (permut ordre_appel result) < nb_inversions (permut ordre_appel p)} = let ooa = ordre_appel in let d = (permut ooa p) in let dij = (swap d (mkp i j)) in let result = compose (transposition p.n i j) p in (* preuve de satisfait_q1 oa result *) for k = 0 to length d - 1 do invariant { forall k'. 0<= k' <= k -> q1_loc tx_b dij k' } swap_preserve_q1 tx_b d i j k done; assert { q1 tx_b dij }; swap_carac2 ooa p i j; let d' = permut ooa result in assert { dij == d'}; assert { satisfait_q1 tx_b ooa result }; (* le nombre d'inversion diminue *) assert { voeu_lt d[j] d[i] }; p4_dec_inv d i j; swap_carac2 ooa p i j; assert { nb_inversions (permut ooa result) = nb_inversions dij < nb_inversions d = nb_inversions d }; result let rec lemma q1_ordering_rec (tx_b : Taux.t) (oa: seq_voeu) (p : permutation) (i j : int) : permutation requires { satisfait_q1 tx_b oa p } requires { 0 <= i < j < p.n } requires { forall i' j'. 0 <= i' < j' < p.n -> ((i' < i) \/ (i' = i /\ j' < j)) -> is_fair_loc oa p i' j' } ensures { satq1_and_is_fair tx_b oa result } ensures { nb_inversions (permut oa result) <= nb_inversions (permut oa p) } variant { nb_inversions (permut oa p), p.n - i, p.n - j } = if not is_fair_loc oa p i j then let p' = loc_improve tx_b oa p i j in q1_ordering_rec tx_b oa p' 0 1 else if j < (p.n - 1) then q1_ordering_rec tx_b oa p i (j + 1) else if i < (p.n - 2) then q1_ordering_rec tx_b oa p (i + 1) (i + 2) else p (* * Etant donnée une permutation 'p' de l'ordre d'appel qui satisfait Q1 * il existe une permutation satisfaisant Q1, avec moins d'inversions et * qui satisfait la condition d'équité boursier/non-boursier. *) predicate q1_ordering_p (tx_b : Taux.t) (oa: seq_voeu) (p pr: permutation) = satq1_and_is_fair tx_b oa pr && nb_inversions (permut oa pr) <= nb_inversions (permut oa p) let lemma q1_ordering (tx_b : Taux.t) (oa: seq_voeu) (p : permutation) : permutation requires { satisfait_q1 tx_b oa p } requires { p.n > 1 } ensures { satq1_and_is_fair tx_b oa result } ensures { nb_inversions (permut oa result) <= nb_inversions (permut oa p) } ensures { q1_ordering_p tx_b oa p result } = q1_ordering_rec tx_b oa p 0 1 let lemma meme_nombre_boursier_avant_id (d : seq_voeu) (p : permutation) (k : int) requires { 0 <= k < length d} requires { p.n = length d } requires { k = first_not_id p } ensures { let d' = permut d p in nb_boursiers d[..k] = nb_boursiers d'[..k] } = let d' = permut d p in for l = 0 to k -1 do invariant { nb_boursiers d[..l] = nb_boursiers d'[..l] } assert { d[l] = d[p l] = d'[l] }; assert { est_boursier d[l] <-> est_boursier d'[l] }; assert { nb_boursiers d[l..l+1] = (if est_boursier d[l] then 1 else 0) = (if est_boursier d'[l] then 1 else 0) = nb_boursiers d'[l..l+1] }; nb_boursiers_eq_snoc d d' (l+1); assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1] } done; assert { nb_boursiers d[..k] = nb_boursiers d'[..k] } let lemma perm_preserves_all_distincts (d : seq_voeu) (p: permutation) requires { all_distincts d } requires { length d = p.n } ensures { let d'= permut d p in all_distincts d' } =( let n = length d in let d'= permut d p in assert { forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> ((p i) <> (p j) && (voeu_distinct d[p i] d[p j]) && (voeu_distinct d'[i] d'[j ]))} ) let lemma inZb_implies_tension (nb_b : int) (tx_b : Taux.t) (d : seq_voeu) (k : int) requires { 0 <= k < length d } requires { IQ4_2.in_Zb nb_b tx_b d k } ensures { tension_taux_boursier tx_b d k } = () let lemma q1_loc_permut (d : seq_voeu) (tx_b : taux) (p: permutation) requires { length d = p.n } requires { q1_loc tx_b d p.n } ensures { q1_loc tx_b (permut d p) p.n} =() let lemma equiv_seq (d : seq_voeu) ensures { d == d[..length d] } = () (* * Preuve de minimalité de l'ordre d'appel par rapport aux permutations * satisfaisant Q1 *) let lemma p4_rec_case_0 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu) (p0: permutation) requires { tx_ds = 0 } requires { all_distincts oa } requires { non_boursiers_ordonnes oa } requires { q1 tx_b oa } requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds oa } requires { is_fair oa } requires { satisfait_q1 tx_b oa p0 } requires { length oa <= 1 } ensures { nb_inversions oa <= nb_inversions (permut oa p0) } = nb_inv_small oa; nb_inv_pos (permut oa p0) let lemma p4_rec_case_1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (d d': seq_voeu) (p0 p: permutation) requires { tx_ds = 0 } requires { all_distincts d } requires { non_boursiers_ordonnes d } requires { q1 tx_b d } requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds d } requires { is_fair d } requires { satisfait_q1 tx_b d p0 } requires { length d > 1 } requires { q1_ordering_p tx_b d p0 p } requires { d' = permut d p } requires { length d = first_not_id p } ensures { nb_inversions d <= nb_inversions (permut d p0) } = meme_nb_inversions d d' let lemma p4_rec_case_2_1_n_2_2 (nb_b nb_ds nb k : int) (tx_b tx_ds : Taux.t) (d d': seq_voeu) (p0 p: permutation) requires { tx_ds = 0 } requires { all_distincts d } requires { non_boursiers_ordonnes d } requires { q1 tx_b d } requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds d } requires { is_fair d } requires { satisfait_q1 tx_b d p0 } requires { nb = length d > 1 } requires { q1_ordering_p tx_b d p0 p } requires { d' = permut d p } requires { k = first_not_id p } requires { k <> nb } ensures { not same_type d[k] d'[k] } ensures { not est_boursier d[k] } = let c = d[k] in let c' = d'[k] in let k0' = (p.inv k) in let k0 = (p.map k) in assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) }; assert { is_fair_loc_seq d' k k0' }; assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) }; assert { is_fair_loc_seq d k k0 }; if same_type c c' then begin (* puisque d et d' sont équitables *) assert { voeu_lt c c' /\ voeu_lt c' c }; absurd end; (* Cas 2.2: si c est boursier, il y a contradiction de Q1 par d' *) if est_boursier c then begin (* la condition d'équité sur d' implique (car c' non boursier) *) assert { rang c' < rang c }; (* le boursier c est plus loin que c' dans d' *) assert { est_boursier d'[k+1..][k0' - (k + 1)] }; assert { not non_boursiers_seulement d'[k+1..] }; (* d'après Q1 sur d' le taux est ok *) assert { [@expl:accel] satisfait_q1 tx_b d p }; assert { q1_loc tx_b d' (k+1) }; assert { nb_boursiers d'[..k+1] = nb_boursiers d'[..k] }; assert { taux_ok tx_b (nb_boursiers d'[..k]) (k+1) }; (* c a doublé c' donc d'après prop 1 sur d tension sur le taux *) assert { iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds d k }; assert { c' = d[k0] = d[k+1..][k0 - k - 1] }; assert { Seq.seq_contains c' d[k+1..] }; assert { voeu_lt c' d[k] }; assert { IQ4_3.in_some_Z nb_b nb_ds tx_b tx_ds d k }; all_resident_implies_Zr_empty nb_ds tx_ds d; assert { not IQ4_1.in_Zr nb_ds tx_ds d k }; assert { IQ4_2.in_Zb nb_b tx_b d k }; inZb_implies_tension nb_b tx_b d k; assert { tension_taux_boursier tx_b d k }; assert { not taux_ok tx_b (nb_boursiers d[..k]) (k+1) }; assert { nb_boursiers d[..k] = nb_boursiers d'[..k] }; assert { not taux_ok tx_b (nb_boursiers d'[..k]) (k+1) }; absurd end let lemma p4_rec_case_2_3_a (nb_b nb_ds nb k k0 k0' : int) (tx_b tx_ds : Taux.t) (d d' d'': seq_voeu) (p0 p: permutation) requires { tx_ds = 0 } requires { all_distincts d } requires { non_boursiers_ordonnes d } requires { q1 tx_b d } requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds d } requires { is_fair d } requires { satisfait_q1 tx_b d p0 } requires { nb = length d > 1 } requires { q1_ordering_p tx_b d p0 p } requires { d' = permut d p } requires { k = first_not_id p } requires { k <> nb } requires { not same_type d[k] d'[k] } requires { not est_boursier d[k] } requires { d'' = (swap d' (mkp k k0')) } requires { k0' = (p.inv k) } requires { k0 = (p.map k) } ensures { nb_boursiers d[..k] = nb_boursiers d''[..k] = nb_boursiers d'[..k] } ensures {forall l. 0 <= l < k -> q1_loc tx_b d'' l } = let c = d[k] in let c' = d'[k] in assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) }; assert { is_fair_loc_seq d' k k0' }; assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) }; assert { is_fair_loc_seq d k k0 }; for l = 0 to k-1 do invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' } invariant { nb_boursiers d[..l] = nb_boursiers d''[..l] = nb_boursiers d'[..l] } assert { est_boursier d'[l..][k-l] }; assert { c' = d'[l..][k - l] }; assert { not est_non_boursier d'[l..][k - l] }; assert { not non_boursiers_seulement d'[l..] };
Q1 pour d' **
assert { satisfait_q1 tx_b d p }; assert { q1_loc tx_b d' l }; assert { taux_ok tx_b (nb_boursiers d'[..l]) l }; assert { taux_ok tx_b (nb_boursiers d''[..l]) l }; assert { q1_loc tx_b d'' l }; assert { d[l] = d[p l] = d'[l] = (swap d' (mkp k k0'))[l] = d''[l] }; assert { same_type d'[l] d''[l] }; nb_boursiers_eq_snoc d' d'' (l+1); nb_boursiers_eq_snoc d d' (l+1); assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1] = nb_boursiers d''[..l+1] }; done let rec lemma p4_rec (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu) (p0: permutation) requires { tx_ds = 0 } requires { all_distincts oa } requires { non_boursiers_ordonnes oa } requires { q1 tx_b oa } requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds oa } requires { is_fair oa } requires { satisfait_q1 tx_b oa p0 } ensures { nb_inversions oa <= nb_inversions (permut oa p0) } variant { nb_inversions (permut oa p0) } = let tx_b = tx_b in let nb = length oa in let d = oa in (* Cas 0: pas de voeux ou 1 seul *) if nb <= 1 then return; let p = q1_ordering tx_b oa p0 in let d'= permut d p in let k = first_not_id p in (* Cas 1: p est la permutation identité *) if k = nb then return; (* Cas 2: p n'est pas l'identité k est l'indice du premier swap dans p. On compare les candidats/voeux, c et c', en k dans d et d'. Trois cas à étudier: 1) si les candidats sont de même type, il y a contradiction de la condition d'équité 2) si c est boursier (et c' non boursier) alors il y a contradiction de Q1 dans d' 3) c est non boursier (et c' boursier) alors on pourrait faire un swap *) let c = d[k] in let c' = d'[k] in let k0' = (p.inv k) in let k0 = (p.map k) in assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) }; assert { is_fair_loc_seq d' k k0' }; assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) }; assert { is_fair_loc_seq d k k0 }; (* Cas 2.1: les deux voeux sont de même type. *) (* Cas 2.2: si c est boursier, il y a contradiction de Q1 par d' *) if same_type c c' || est_boursier c then absurd; (* Cas 2.3: d' a réduit son nombre d'inversions en faisant remonter prématurément un boursier. mais alors on pourrait échanger c et c' dans d' et faire moins d'inversions en contredisant la minimalité de d' tout en conservant la propriete 1 au niveau du nombre de boursiers. sur 0..k d'' a comme d en k+1..k0' d'' au taquet en k0'+1..n d'' a comme d' *) assert {[@expl:comment] est_non_boursier c /\ est_boursier c' };
todo assert {[@expl:oav inv] non_boursier_mieux_classe_que_suivants d k k0 };**
assert { rang c < rang c' }; let d'' = (swap d' (mkp k k0')) in (* d'' satisfait Q1 sur [0,k[ *) for l = 0 to k-1 do invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' } invariant { nb_boursiers d[..l] = nb_boursiers d''[..l] = nb_boursiers d'[..l] } assert { est_boursier d'[l..][k-l] }; assert { c' = d'[l..][k - l] }; assert { not est_non_boursier d'[l..][k - l] }; assert { not non_boursiers_seulement d'[l..] };
Q1 pour d' **
assert { satisfait_q1 tx_b oa p }; assert { q1_loc tx_b d' l }; assert { taux_ok tx_b (nb_boursiers d'[..l]) l }; assert { taux_ok tx_b (nb_boursiers d''[..l]) l }; assert { q1_loc tx_b d'' l }; assert { d[l] = d[p l] = d'[l] = (swap d' (mkp k k0'))[l] = d''[l] }; assert { same_type d'[l] d''[l] }; nb_boursiers_eq_snoc d' d'' (l+1); nb_boursiers_eq_snoc d d' (l+1); assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1] = nb_boursiers d''[..l+1] }; done; (* fin preuve d'' satisfies Q1 on [0, k[ *) assert { nb_boursiers d[..k] = nb_boursiers d''[..k] = nb_boursiers d'[..k] }; assert { forall l. 0 <= l < k -> q1_loc tx_b d'' l }; (* d'' satisfies Q1 on [k, k0'[ *) assert { nb_boursiers d''[..k+1] = nb_boursiers d[..k+1] }; assert { q1_loc tx_b d (k+1) }; assert { est_boursier d[k0] }; assert { d[k0] = d[k+1..][k0 - (k+1)] }; assert { not est_non_boursier d[k+1..][k0 - (k+1)] }; assert { not non_boursiers_seulement d[k+1..] }; assert { seq_respecte_taux_b tx_b d[..k+1] }; assert { taux_ok tx_b (nb_boursiers d[..k+1]) (k+1) }; assert { taux_ok tx_b (nb_boursiers d''[..k+1]) (k+1) }; assert { seq_respecte_taux_b tx_b d''[..k] }; assert { q1_loc tx_b d'' k }; for l = k + 1 to k0' -1 do invariant { nb_boursiers d''[..l] = nb_boursiers d[..k] + (l - k - 1) } invariant { forall l'. k+1 <= l' < l -> taux_ok tx_b (nb_boursiers d''[..l']) l' } invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' } if est_non_boursier d'[l] then begin assert {[@expl: post_cond_of_q1_ordering] let oa' = (permut oa p) in is_fair oa' }; assert { is_fair_loc oa p l k0' }; assert { is_fair_loc_seq d' l k0' }; assert { not voeu_lt d'[k0'] d'[l] }; perm_preserves_all_distincts d p; assert { voeu_lt d'[l] d'[k0'] }; assert { d'[l] = d[p l] by d'= permut d p }; assert { d'[k0'] = d[k] }; assert { voeu_lt d[p l] d[k] };
Q1 pour d **
assert { forall i. 0 <= i < k -> p i = i }; let l' = (p.map l) in assert { 0 <= l < p.n }; assert { in_range p.n p.map }; assert { l' < p.n }; assert { est_non_boursier d[k]}; assert { d[l'] = d[p l] = d'[l] }; assert { est_non_boursier d[l'] }; assert { k < l' }; assert { non_boursiers_ordonnes d }; assert { p.n = length d }; assert { 0 <= k < l' < p.n = length d }; assert {voeu_lt d[k] d[l'] }; absurd; end; assert { est_boursier d'[l] }; assert { est_boursier d''[l] }; assert { nb_boursiers d''[..l+1] = nb_boursiers d''[..l] + nb_boursiers d''[l..l+1] = nb_boursiers d''[..l] + 1 }; assert { 100 * (nb_boursiers d''[..l+1]) = 100 * nb_boursiers d''[..l] + 100 >= tx_b + tx_b * l = tx_b * (l+1) }; assert { seq_respecte_taux_b tx_b d''[..l]}; assert { q1_loc tx_b d'' l }; done; (* fin preuve d'' satisfies Q1 on [k, k0'[ *) (* d'' satisfait Q1 sur [k0',length d[ *) assert { [@expl: init inv1] forall l'. 0 <= l' < k0' -> q1_loc tx_b d'' l' }; assert { [@expl: init inv1] seq_respecte_taux_b tx_b d''[..k0'] }; assert { [@expl: init inv1] q1_loc tx_b d'' k0' }; for l = k0' + 1 to nb - 1 do invariant { [@expl: inv1 q1 sur [k0',l[] forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' } invariant { nb_boursiers d'[..l] = nb_boursiers d''[..l] } assert { l<>k && l <> k0' }; assert { d''[l] = (swap d' (mkp k k0'))[l] = d'[l] }; assert { d'[l] = d''[l] }; if non_boursiers_seulement d'[l..] then begin assert { [@precond2 meme_non_boursiers_seulement] forall l'. l <= l' < length d -> (l'<>k && l' <> k0') && (d'[l'] = d''[l'])}; meme_non_boursiers_seulement d' d'' l; assert { non_boursiers_seulement d''[l..] }; assert { q1_loc tx_b d'' l }; end else begin assert { q1 tx_b d'}; assert { q1_loc tx_b d' l }; assert { seq_respecte_taux_b tx_b d'[..l] }; assert { taux_ok tx_b (nb_boursiers d'[..l]) l }; swap_nb_boursiers d' k k0' l; assert { nb_boursiers d'[l..l+1] = nb_boursiers d''[l..l+1]}; assert { nb_boursiers d'[..l+1] = nb_boursiers d'[..l] + nb_boursiers d'[l..l+1] = nb_boursiers d''[..l] + nb_boursiers d''[l..l+1] = nb_boursiers d''[..l+1] }; assert { taux_ok tx_b (nb_boursiers d''[..l]) l }; assert { q1_loc tx_b d'' l }; end; assert { q1_loc tx_b d'' l }; done; (* fin preuve d'' satisfait Q1 dur [k0',length d[ *) assert { forall l. 0 <= l < length d'' -> q1_loc tx_b d'' l }; assert { length d = length d' = length d'' = nb }; assert { q1_loc tx_b d nb }; q1_loc_permut d tx_b p; assert { q1_loc tx_b d' nb }; let t = (transposition nb k k0' ) in let d''' = permut d' t in swap_carac d' k k0'; assert { d'' == d'''}; q1_loc_permut d' tx_b t ; assert { q1 tx_b d''' }; assert { q1 tx_b d'' }; (*equiv_seq d'; equiv_seq d''; *) assert { nb_boursiers d'[..nb] = nb_boursiers d' = nb_boursiers d'' = nb_boursiers d''[..nb] }; (*assert { seq_respecte_taux_b tx_b d''[..nb] };*) assert { q1_loc tx_b d'' nb }; assert { q1 tx_b d'' }; assert { nb_inversions d'' < nb_inversions d' } ; let p'' = (compose (transposition nb k k0') p) in swap_carac2 oa p k k0'; assert { nb_inversions (permut oa p'') = nb_inversions d'' }; meme_q1 tx_b d'' (permut d p''); assert { satisfait_q1 tx_b oa p''}; p4_rec nb_b nb_ds tx_b tx_ds oa p'' let lemma iq4_1b_implies_fair (nb_ds : int) (tx_ds : Taux.t) (d: seq_voeu) requires { tx_ds = 0 } requires { non_boursiers_ordonnes d } requires { iq4_1b_nomap nb_ds tx_ds d } ensures { is_fair d } = ( P5_Lemmas.all_resident_implies_Zr_empty nb_ds tx_ds d; let n = length d in for i = 0 to n-1 do invariant { forall i' j. 0 <= i' < i -> i' < j < n -> is_fair_loc_seq d i' j } for j = i+1 to n-1 do invariant { forall j'. i < j' < j -> is_fair_loc_seq d i j' } begin if est_boursier d[j] then begin assert { d[j] = d[i+1..][j-i-1] }; assert { Seq.seq_contains d[j] d[i+1..] }; assert { iq4_1b_loc_nomap nb_ds tx_ds d i }; assert { not (IQ4_1.in_Zr nb_ds tx_ds d i) }; assert { voeu_lt d[i] d[j] } end else if est_non_boursier d[i] then assert { voeu_lt d[i] d[j] } end done done ) (* * Un ordre d'appel valide satisfait P4 *) let lemma oa_sat_p4 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu) requires { tx_ds = 0 } requires { all_distincts oa } requires { non_boursiers_ordonnes oa } requires { q1 tx_b oa } requires { iq4_1b_nomap nb_ds tx_ds oa} requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds oa } ensures { forall p : permutation. satisfait_q1 tx_b oa p -> nb_inversions oa <= nb_inversions (permut oa p) } = iq4_1b_implies_fair nb_ds tx_ds oa; let p = any permutation in if satisfait_q1 tx_b oa p then p4_rec nb_b nb_ds tx_b tx_ds oa p end module P4_Snoc use int.Int use seq.Seq use mach.java.lang.Integer use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts use proofs.ordre_appel.invariants.iq3_0.IQ3_0 use proofs.ordre_appel.invariants.iq3_2.IQ3_2 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.properties.q1.Q1 use proofs.ordre_appel.properties.p5.P5_Lemmas 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 P4_Lemmas use export P4 let lemma p4_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oak s : seq_voeu) (m :EnumMap.t) (v : voeu) requires {[@expl:pre p4 / s = oak.v] s == snoc oak v } requires {[@expl:pre p4 / all_distincts s] all_distincts s } requires {[@expl:pre p4 / q1] q1 tx_b s } requires {[@expl:pre p4 / iq3_0] iq3_0 s m } requires {[@expl:pre p4 / iq3_2] iq3_2 s m } requires {[@expl:pre p4 / iq4_1b] iq4_1b nb_ds tx_ds s m } requires {[@expl:pre p4 / iq4_3b] iq4_3b nb_b nb_ds tx_b tx_ds s m } requires {[@expl:pre p4 / p4] p4 tx_b tx_ds oak } ensures { p4 tx_b tx_ds s } = iq_nomap_transfers nb_b nb_ds tx_b tx_ds s m; if tx_ds.tx = (0:integer) then begin iq41b_implies_boursiers_ordonnes nb_ds tx_ds s; assert { boursiers_ordonnes s }; iq3_implies_non_boursiers_ordonnes nb_b nb_ds tx_b tx_ds s; assert { non_boursiers_ordonnes s }; oa_sat_p4 nb_b nb_ds tx_b tx_ds s end let lemma p4_empty (tx_b tx_ds : Taux.t) (oak : seq_voeu) requires { oak = empty } ensures { p4 tx_b tx_ds oak } = () end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git