module IQ1
  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 iq1_loc (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (k : int) =
  forall i. 0 <= i <= k ->
    remains_boursiers oak[..i] nb_b ->
    seq_respecte_taux_b tx_b oak[..i+1]

  predicate iq1 (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) =
    forall k. 0 <= k < length oak -> iq1_loc nb_b tx_b  oak k
end

module IQ1_Lemmas
  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

  let lemma iq1_l1 (s : seq_voeu) (total_b : int) (i : int)
    requires {[@expl:i lt |s|] 0 < i <= length s }
    requires {[@expl:remains_boursiers up to i] remains_boursiers s[..i] total_b }
    ensures { remains_boursiers s[..i-1] total_b }
  = assert { snoc s[..i-1] s[i-1] == s[..i] }

  let lemma iq1_l2a (s : seq_voeu) (v : voeu) (tx : taux) (p : voeu -> bool) (count : seq_voeu -> int)
    requires { forall s v. count (snoc s v) = if p v then count s +1 else count s }
    requires { p v }
    requires { seq_respecte_taux tx s count }
    ensures {  seq_respecte_taux tx (snoc s v) count }
  = ()

  let lemma iq1_l2a_b (tx_b : Taux.t) (s : seq_voeu) (v : voeu)
    requires { seq_respecte_taux_b tx_b s }
    requires { est_boursier v }
    ensures {  seq_respecte_taux_b tx_b (snoc s v) }
  = ()

  let lemma iq1_l2a_ds (tx_ds : Taux.t)  (s : seq_voeu) (v : voeu)
    requires { seq_respecte_taux_ds tx_ds s }
    requires { est_du_secteur v }
    ensures { seq_respecte_taux_ds tx_ds (snoc s v) }
  = ()

  let lemma iq1_l2b (s : seq_voeu) (v : voeu) (tx : taux) (total : int) (p : voeu -> bool) (count : seq_voeu -> int)
    requires { forall s v. count (snoc s v) = if p v then count s +1 else count s }
    requires { not taux_x_contraignant tx s count total }
    ensures { seq_respecte_taux tx (snoc s v) count \/ ((count s = 0) \/ not (count s < total)) }
  = ()

  let lemma iq1_l2b_b (nb_b : int) (tx_b : Taux.t) (s : seq_voeu) (v : voeu)
    requires { not taux_b_contraignant tx_b s nb_b }
    ensures { seq_respecte_taux_b tx_b (snoc s v) \/ not remains_boursiers s nb_b }
  = ()

  let lemma iq1_l2b_ds (nb_ds : int) (tx_ds : Taux.t) (s : seq_voeu) (v : voeu)
    requires { not taux_ds_contraignant tx_ds s nb_ds}
    ensures { seq_respecte_taux_ds tx_ds (snoc s v) \/ not remains_du_secteur s nb_ds }
  = ()
end

module IQ1_Snoc
  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
  use IQ1_Lemmas
  use export IQ1

  let lemma iq1_snoc (nb_b : int) (tx_b : Taux.t)  (oak : seq_voeu) (v : VoeuClasse.t)
    requires { [@expl:pre/iq1(s)] iq1 nb_b tx_b oak }
    requires { [@expl:pre/v not boursier -> tx_b non_contraignant] not est_boursier v -> not taux_b_contraignant tx_b oak nb_b }
    ensures { iq1 nb_b tx_b (snoc oak v)  }
  =
    let s = snoc oak v in
    for k = 0 to length s - 1 do
      invariant { forall j. 0 <= j < k -> iq1_loc nb_b tx_b  s j }
      if k < length s - 1 then begin
	      assert { forall i. 0 <= i <= k -> s[..i+1] == oak[..i+1] };
        assert { iq1_loc nb_b tx_b  oak k };
	      assert {  forall i. 0 <= i <= k
	             	  -> remains_boursiers s[..i] nb_b
	                -> remains_boursiers oak[..i] nb_b
		              -> seq_respecte_taux_b tx_b oak[..i+1]
 		              -> seq_respecte_taux_b tx_b s[..i+1] };
	      assert {  forall i. 0 <= i <= k
	       	        -> remains_boursiers s[..i] nb_b
 		              -> seq_respecte_taux_b tx_b s[..i+1] };
        assert { iq1_loc nb_b tx_b  s k };
      end else begin
        assert { forall i. 0 <= i < k -> s[..i+1] == oak[..i+1] };
        assert { iq1_loc nb_b tx_b  s (k-1) };
	      assert { remains_boursiers s[..k] nb_b
	               -> remains_boursiers oak nb_b
	               -> seq_respecte_taux_b tx_b oak
	               -> seq_respecte_taux_b tx_b s };
        assert { iq1_loc nb_b tx_b  s k };
      end
    done
end

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