module IQ4_xa
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use int.Int
  use int.NumOf

  function est_x (v: voeu) : bool

  function nb_x (s : seq_voeu) : int =
    seq_numof est_x s

  function in_Z (s : seq_voeu) (taux_x : taux) (total_x i : int) : bool =
     est_x s[i] && taux_x_contraignant taux_x s[..i] nb_x total_x

  function nb_contraintes_taux_x (s : seq_voeu) (taux_x : taux) (total_x : int) : int =
    numof (in_Z s taux_x total_x) 0 (length s)

  predicate iq4_xa_loc (s : seq_voeu) (taux_x : taux) (total_x k : int) =
    forall i. 0 <= i <= k ->
      let nbCb = nb_contraintes_taux_x s[..i] taux_x total_x in
          100 * nbCb <= taux_x * i + 100

  predicate iq4_xa (oak : seq_voeu) (taux_x : taux) (total_x : int) =
    forall k. 0 <= k <= length oak -> iq4_xa_loc oak taux_x total_x k

  let lemma in_Z_cons (s : seq_voeu) (x : voeu) (taux_x : taux) (total_x : int)
    ensures { forall i. 0 <= i < length s ->
    	        in_Z s taux_x total_x i  = in_Z (snoc s x) taux_x total_x i }
  = ()

  let lemma numof_in_Z_snoc (s : seq_voeu) (x : voeu) (taux_x : taux) (total_x : int)
    ensures { numof (in_Z s taux_x total_x) 0 (length s) = numof (in_Z (snoc s x) taux_x total_x) 0 (length s) }
  = ()

  let lemma nb_contraintes_taux_x_snoc (s : seq_voeu) (x : voeu) (taux_x : taux) (total_x : int)
    ensures { est_x x && taux_x_contraignant taux_x s nb_x total_x ->
    	      nb_contraintes_taux_x (snoc s x) taux_x total_x =
    	      nb_contraintes_taux_x s taux_x total_x + 1}
    ensures { not (est_x x && taux_x_contraignant taux_x s nb_x total_x)
    	        -> nb_contraintes_taux_x (snoc s x) taux_x total_x = nb_contraintes_taux_x s taux_x total_x }
  = ()

  let rec lemma nb_contraintes_taux_x_lt_b_all (s: seq_voeu) (taux_x : taux) (total_x : int)
    ensures { nb_contraintes_taux_x s taux_x total_x <= nb_x s }
    variant { length s }
  = if length s > 0 then
      nb_contraintes_taux_x_lt_b_all s[..length s-1] taux_x total_x

  let lemma iq4_xa_snoc (oak : seq_voeu) (taux_x : taux) (total_x : int) (x : voeu)
    requires { iq4_xa oak taux_x total_x }
    ensures { (est_x x && taux_x_contraignant taux_x oak nb_x total_x)
	      -> nb_contraintes_taux_x (snoc oak x) taux_x total_x =
	      	 nb_contraintes_taux_x oak taux_x total_x +1 }
    ensures { not (est_x x && taux_x_contraignant taux_x oak nb_x total_x)
	      -> nb_contraintes_taux_x (snoc oak x) taux_x total_x =
	      	 nb_contraintes_taux_x oak taux_x total_x }
    ensures { iq4_xa (snoc oak x) taux_x total_x }
  =
    let s' = snoc oak x in
     assert { nb_contraintes_taux_x oak taux_x total_x <=
     	      nb_contraintes_taux_x (snoc oak x) taux_x total_x };
     assert { forall i. 0 <= i <= length oak = length s'-1
     	      -> s'[..i] == oak[..i] };
     assert { forall k. 0 <= k < length s' ->
              (iq4_xa_loc oak taux_x total_x k &&
               iq4_xa_loc s' taux_x total_x k) };

     assert { iq4_xa_loc oak taux_x total_x (length oak) };
     assert { forall i. 0 <= i <= length oak ->
     	      let nbCb = nb_contraintes_taux_x oak[..i] taux_x total_x in
              	  100 * nbCb <= taux_x * i + 100 };

     assert { forall i. 0 <= i < length s' ->
      let nbCb = nb_contraintes_taux_x s'[..i] taux_x total_x in
          100 * nbCb <= taux_x * i + 100 };

     let nbCb = nb_contraintes_taux_x oak taux_x total_x in
     let nbCbx = nb_contraintes_taux_x (snoc oak x) taux_x total_x in
       assert { 100 * nbCb <= taux_x * (length oak) + 100 };
       if est_x x && taux_x_contraignant taux_x oak nb_x total_x then
       begin
         let nb_b = nb_x oak in
	 assert { nbCb <= nb_b };
         assert { nb_b < total_x && 100 * nb_b < taux_x * (length oak +1) };
	 assert { 100 * nbCb < taux_x * (length oak +1) };
         assert { nbCbx = nbCb + 1 };

       end else begin
         assert { nbCbx = nbCb };
         assert { 100 * nbCb <= taux_x * (length oak) + 100 ->
	          100 * nbCb <= taux_x * (length oak) + 100 + taux_x };
         assert { 100 * nbCb <= taux_x * (length oak + 1) + 100 };
       end;
       assert { 100 * nbCbx <= taux_x * (length oak + 1) + 100 };

     assert { forall i. i = length s' ->
         let nbCb = nb_contraintes_taux_x s'[..i] taux_x total_x in
           100 * nbCb <= taux_x * i + 100 };
     assert { iq4_xa_loc s' taux_x total_x (length s') }

  let lemma nb_contraintes_taux_x_prefix_1 (s : seq_voeu) (taux_x : taux)
					  (total_x : int) (l k : int)
    requires { 0 <= l < k <= length s }
    ensures { nb_contraintes_taux_x s[..l] taux_x total_x = nb_contraintes_taux_x s[..k][..l] taux_x total_x }
  = ()

  let lemma nb_contraintes_taux_x_prefix (s : seq_voeu) (taux_x : taux)
					 (total_x : int) (l k : int)
    requires { 0 <= l < k <= length s }
    ensures { nb_contraintes_taux_x s[..l] taux_x total_x <= nb_contraintes_taux_x s[..k] taux_x total_x }
  = assert { forall i. 0 <= i <= l -> s[..l][..i] == s[..k][..i] };
    assert { forall i. 0 <= i < l -> s[..l][i] = s[..k][i] };
    assert { forall i. 0 <= i < l -> (in_Z s[..l] taux_x total_x i = in_Z s[..k] taux_x total_x i) };
    assert { numof (in_Z s[..k] taux_x total_x) 0 k =
    	     numof (in_Z s[..k] taux_x total_x) 0 l +
      	     numof (in_Z s[..k] taux_x total_x) l k };
    assert { numof (in_Z s[..k] taux_x total_x) 0 k =
    	     numof (in_Z s[..l] taux_x total_x) 0 l +
      	     numof (in_Z s[..k] taux_x total_x) l k }

  let lemma taux_nul_pas_de_contrainte (s : seq_voeu) (t : taux) (total_x i : int)
     requires { 0 <= i < length s }
     requires { t = 0 }
     ensures { not in_Z s t total_x i }
  =
    assert { not taux_x_contraignant t s[..i] nb_x total_x };
    ()

  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel

  let lemma in_Z_eq_up_to_rang_appel (s1 s2 : seq_voeu) (taux_x : taux) (total_x i : int)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { 0 <= i < length s1 }
    requires { forall i. 0 <= i < length s1 -> est_x s1[i] = est_x s2[i] }
    ensures { in_Z s1 taux_x total_x i = in_Z s2 taux_x total_x i }
  =
    seq_numof_eq_prefix s1[..i] s2[..i] est_x;
    assert { nb_x s1[..i] = nb_x s2[..i] }

  let lemma nb_contraintes_taux_x_up_to_rang_appel (s1 s2 : seq_voeu) (taux_x : taux) (total_x i : int)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { 0 <= i <= length s1 }
    requires { forall i. 0 <= i < length s1 -> est_x s1[i] = est_x s2[i] }
    ensures { nb_contraintes_taux_x s1[..i] taux_x total_x = nb_contraintes_taux_x s2[..i] taux_x total_x }
  =
    ghost begin
    let f1 = pure { in_Z s1[..i] taux_x total_x } in
    let f2 = pure { in_Z s2[..i] taux_x total_x } in
    assert { forall k. 0 <= k < i -> in_Z s1[..i] taux_x total_x k = in_Z s2[..i] taux_x total_x k };
    assert { forall k. 0 <= k < i -> f1 k = f2 k };
    assert { numof f1 0 (length s1[..i]) = numof f2 0 (length s2[..i]) }
  end
end

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