Parcoursup / Calcul de l'ordre d'appel des candidats index


module Pair
  use int.Int

  type pair = {
    i: int;
    j : int;
  }

  let function mkp (i j : int) : pair = { i=i; j=j }

  predicate in_quadrant (p : pair) =
    0 <= p.i < p.j

  predicate in_quadrant_n (p : pair) (n : int) =
    0<= p.i < p.j < n

  predicate in_rect (p : pair) (ni nj : int) =
    0<= p.i < ni && 0<= p.j < nj

  let function pair_lt (p q : pair) : bool
  =
    p.i < q.i || (p.i = q.i && p.j < q.j)

  let function pair_neq (p q : pair) : bool
  =
    p.i <> q.i || p.j <> q.j

  let function pair_eq (p q : pair) : bool
  =
    p.i = q.i && p.j = q.j

  let lemma mkp_carac (i j :int)
    ensures { (mkp i j).i = i && (mkp i j).j = j }
  =
    ()

  let lemma lt_gt_eq (p q : pair)
    requires { not pair_lt p q }
    requires { not pair_lt q p }
    ensures { pair_eq p q }
  =
    ()

  let lemma exists_in_quadrant_n (n : int) : (p : pair)
    requires { 2 <= n }
    ensures { in_quadrant_n p n }
  =
    assert { exists i j. 0 <= i < j < n };
    let i, j = any (i:int, j:int) ensures { 0 <= i < j < n } in
    mkp i j
end

(* generated on Thu Jan 30 02:06:23 UTC 2025 from rev:  *)

Generated by why3doc 1.7.2+git