module Q3
  use int.Int
  use seq.Seq

  use proofs.ordre_appel.seq_voeux.SeqVoeux
  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

Q3 * * Un candidat resident boursier qui a le rang r dans le classement * pedagogique n'est jamais doublé par personne et a un rang inferieur ou * egal a r dans l'ordre d'appel.

  predicate q3a_loc (s: seq_voeu) (i : int) =
    est_boursier_du_secteur s[i] -> forall j. 0 <= j < i -> voeu_lt s[j] s[i]

  predicate q3a (s: seq_voeu) =
    forall i. 0 <= i < Seq.length s -> q3a_loc s i

  predicate q3b_loc_x (s : seq_voeu) (i : int) =
    est_boursier_du_secteur s[i] -> (1 <= (i+1) <= get_rang s[i])

  predicate q3b_loc (seq_voeu) (int)

  axiom q3b_loc_def:
    forall s: seq_voeu, i : int.
      q3b_loc s i <-> (est_boursier_du_secteur s[i] -> 1 <= (i+1) <= get_rang s[i])

  let lemma q3b_loc_equiv (s : seq_voeu) (i : int)
    ensures { q3b_loc_x s i <-> q3b_loc s i }
  = ()

  predicate q3b (s: seq_voeu) =
    forall i. 0 <= i < Seq.length s -> q3b_loc s i

  predicate q3 (oa : seq_voeu) =
      q3a oa /\ q3b oa

end

module Q3_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use export Q3

  let lemma q3_up_to_rang_appel_oa (oa1 oa2 : seq_voeu)
    requires { q3 oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q3 oa2 }
  =
    for i = 0 to length oa2 - 1 do
      invariant { forall k. 0 <= k < i -> q3b_loc oa2 k }
      invariant { forall k. 0 <= k < i -> q3a_loc oa2 k }
      assert { q3b_loc oa1 i };
      assert { q3a_loc oa1 i }
    done

end

module Q3_Lemmas
  use int.Int
  use mach.java.lang.Integer
  use seq.Seq
  use seq.FreeMonoid
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use Q3

  let lemma q3a_snoc (s: seq_voeu) (x : voeu)
     requires {[@expl:q3a s] q3a s }
     requires {[@expl:q3a x] est_boursier_du_secteur x -> forall j. 0 <= j < length s -> voeu_lt s[j] x }
     ensures { q3a (snoc s x) }
  =
    let sp = snoc s x in
    for i = 0 to length sp - 1 do
      invariant { forall j. 0 <= j < i -> q3a_loc sp j }
      assert { i < length sp - 1 -> q3a_loc s i }
    done

  use pigeon.Pigeonhole

  function pigeon_map (s : seq_voeu) (i : int) : int =
    ((get_rang s[i]) - (1:integer))

  let lemma q3b_snoc (s: seq_voeu) (x : voeu)
    requires { [@expl:rangs >= 1] get_rang x >= 1 /\ forall i. 0 <= i < length s -> get_rang s[i] >= 1 }
    requires { [@expl:q3b s] q3b s }
    requires { [@expl:alld (s x)] all_distincts (snoc s x) }
    requires { [@expl:q3a (s x)] q3a (snoc s x) }
    ensures { q3b (snoc s x) }
  = let sp = snoc s x in

    for k = 0 to length sp-1 do
      invariant { forall i. 0 <= i < k -> q3b_loc sp i }

      if not est_boursier_du_secteur x then
        continue;

      if k < length sp-1 then
      begin
        assert { sp[..k] == s[..k] };
      end else begin
        let rang_oa = k + 1 in
        let rang_pedago = Integer.to_int (get_rang sp[k]) in

        if rang_oa > rang_pedago then
        begin
          assert { q3a_loc sp k };
          pigeonhole rang_oa rang_pedago (pigeon_map sp);
	        absurd;
        end;
        assert { 1 <= rang_oa <= rang_pedago };
        assert { q3b_loc sp k };
      end
    done
end

module Q3_Snoc
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.invariants.iq3_1.IQ3_1

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use Q3_Lemmas
  use export Q3

  let lemma q3_snoc (oak : seq_voeu) (m : EnumMap.t) (x : voeu)
    requires { [@expl:pre Q3 / rangs >= 1] get_rang x >= 1 /\ forall i. 0 <= i < length oak -> get_rang oak[i] >= 1 }
    requires { [@expl:pre Q3 / Q3(oak)] q3 oak }
    requires { [@expl:pre Q3 / iq3_1(oak.x)] iq3_1 (snoc oak x) m }
    requires { [@expl:pre Q3 / alld(oak.x)] all_distincts (snoc oak x) }
    ensures { est_boursier_du_secteur x -> q3a (snoc oak x) }
    ensures { q3b (snoc oak x) }
    ensures { q3 (snoc oak x) }
  =
    let s = snoc oak x in
    let k = length s - 1 in

    assert { forall j. 0 <= j < k  -> iq3_1_loc s m j ->
             voeu_lt_than_typed_in_queue s[j] s[j+1..] BOURSIER_DU_SECTEUR };
    voeu_lt_than_last_typed_in_queue s BOURSIER_DU_SECTEUR

  let lemma q3_empty (oak : seq_voeu)
    requires { oak = Seq.empty }
    ensures { q3 oak }
  = ()

end

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