Propriété Q6: si les deux taux sont nuls alors l'ordre d'appel est le classement pédagogique

module Q6
  use int.Int
  use seq.Seq

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

  predicate q6_loc (op oa : seq_voeu) (k : int) =
    0 <= k <= length oa <= length op &&
    forall j. 0 <= j < k -> get_rang op[j] = get_rang oa[j]

  predicate q6 (tx_b tx_r : Taux.t) (op oa : seq_voeu)   =
      tx_b = 0 -> tx_r = 0 -> q6_loc op oa (length oa)
end

module Q6_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 export Q6

  let lemma q6_up_to_rang_appel_oa (tx_b tx_r : Taux.t) (op oa1 oa2 : seq_voeu)
    requires { q6 tx_b tx_r op oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q6 tx_b tx_r op oa2 }
  =
   ()

  let lemma q6_up_to_rang_appel_op (tx_b tx_r : Taux.t) (op1 op2 oa : seq_voeu)
    requires { q6 tx_b tx_r op1 oa }
    requires { seq_voeu_eq_up_to_rang_appel op1 op2 }
    ensures { q6 tx_b tx_r op2 oa }
  =
    ()
end

module Q6_Snoc
  use seq.Seq
  use int.Int
  use seq.FreeMonoid
  use mach.java.lang.Integer
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SortedSeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.invariants.iq0.IQ0
  use proofs.ordre_appel.invariants.iqx.IQX
  use proofs.ordre_appel.invariants.iq6.IQ6
  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 export Q6

  let lemma q6_snoc (nb_b nb_ds : int) (tx_b tx_r : Taux.t) (op oak : seq_voeu) (m : EnumMap.t) (x : voeu)
    requires { [@expl:pre q6 / g sorted] seq_rangs_sorted op }
    requires { [@expl:pre q6 / iq6] iq6 tx_b tx_r (snoc oak x) m }
    requires { [@expl:pre q6 / iq0] iq0 op (snoc oak x) m }
    requires { [@expl:pre q6 / iq0] iqx_0 (length op) nb_b nb_ds (snoc oak x) m }
    requires { [@expl:pre q6 / q6] q6 tx_b tx_r op oak }

    ensures  { [@expl:q6(oak.x)] q6 tx_b tx_r op (snoc oak x) }
  =
    if not (tx_b.tx = (0:integer) && tx_r.tx = (0:integer)) then
      return;

    let s = snoc oak x in
    assert { forall i. 0 <= i < length oak -> seq_contains x s[i+1..] };
    assert { iq6 tx_b tx_r (snoc oak x) m };
    assert { forall i. 0 <= i < length oak -> voeu_lt s[i] x };
    assert { forall i. 0 <= i < length oak -> s[i] = oak[i] };
    assert { forall i. 0 <= i < length oak -> voeu_lt oak[i] x };
    assert {[@expl:|s|<=|g] length s <= length op };

    for k = 0 to length s - 1 do
      invariant { q6_loc op s k }

      if k < length s - 1 then
      begin
        assert { q6_loc op oak k };
        assert { q6_loc op s k };
        continue;
      end;

      let v = op[k] in

      assert { iq0 op s m };
      assert { seq_contains v s \/ enummap_contains m v };

      let y = s[k] in
      assert { [@expl:s(k) in op] seq_contains y op };

      let j = any (j : int) ensures { 0 <= j < length op /\ op[j] = y } in
      assert { [@expl:op(j) = s(k)] op[j] = s[k] };

      if j < k then begin
        assert { [@expl:q6 j] q6_loc op oak j };
        assert { [@expl:s(j) = s(k)] s[j] = s[k] };
        assert { voeu_lt s[j] s[k] };
        absurd;
      end else if k < j then begin
        assert { [@expl:v < y] voeu_lt v s[k] };

        assert { seq_contains v s -> seq_contains v s[..k] };
        assert { enummap_contains m v -> voeu_lt s[k] v };
        assert { not enummap_contains m v };

        assert { not seq_contains v s[k+1..] };
        assert { [@expl:v in s(..k)] seq_contains v s[..k] };

        let i = any int ensures { 0 <= result < k && s[result] = v } in
        assert { voeu_lt op[i] op[k] };
        assert { [@expl:q6 i] q6_loc op s i };
        assert { [@expl:g(i) = g(k)] v = s[i] = op[i] };
        assert { [@expl:g(i) = g(k)] i < k /\ op[i] = op[k] };
        absurd;
      end;
    done

end

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