Formalization of [ABF20]

[ABF20] Michael Albert, Mathilde Bouvel, and Valentin Féray. Two first-order logics of permutations. Journal of Combinatorial Theory, Series A, 171:105158, April 2020. [https://arxiv.org/abs/1808.05459v2](https://arxiv.org/abs/1808.05459v2).

[Gio20] A. Giorgetti. Formalisation et vérification de théories de permutations. Research report RR-1715 (in French), UBFC (Université de Bourgogne Franche-Comté) and FEMTO-ST, 17 pages, December 2020. [https://hal.archives-ouvertes.fr/hal-03033416](https://hal.archives-ouvertes.fr/hal-03033416).

[Gio21] A. Giorgetti. Théories de permutations avec Why3. In JFLA 2021, 8 pages, April 2021. [http://jfla.inria.fr/jfla2021.html](http://jfla.inria.fr/jfla2021.html).

1. Proposal of extension of relations.mlw in stdlib, for TOOB

module Relation
  type t
  type u
  predicate rel t u
end

module Determinism (* or PartialFunction *)
  clone export Relation
  axiom Deter : forall x:t. forall y z:u. rel x y -> rel x z -> y = z
end

module Functionality
  clone export Determinism with axiom Deter
  axiom Total : forall x:t. exists y:u. rel x y
end

module Injectivity
  clone export Relation
  axiom Injec : forall x y:t. forall a:u. rel x a -> rel y a -> x = y
end

module Surjectivity
  clone export Relation
  axiom Surjec : forall y:u. exists x:t. rel x y
end

module Bijectivity
  clone export Functionality with axiom Deter, axiom Total
  clone export Injectivity with type t = t, type u = u, predicate rel = rel, axiom Injec
  clone export Surjectivity with type t = t, type u = u, predicate rel = rel, axiom Surjec
end

module MapRelation
  use map.Map

  type t
  type u

  predicate map_rel (m: map t u) (x:t) (y:u) = (m[x] = y)

  constant m: map t u

  predicate m_graph (x:t) (y:u) = map_rel m x y

  clone export Functionality with type t = t, type u = u, predicate rel = m_graph

end

2. Proposal of extension of map.mlw in stdlib, for ModelTOOB and other modules

(* Injectivity, surjectivity and bijectivity for any maps, more general than
   module `MapInjection` in map.mlw in stdlib. *)
module MapInjSurjBij

  use map.Map

  predicate injective (m: map 'a 'b) = forall i j: 'a. m[i] = m[j] -> i = j

  predicate surjective (m: map 'a 'b) = forall j: 'b. exists i: 'a. m[i] = j

  predicate bijective (m: map 'a 'b) = injective m /\ surjective m

  (* TODO: add more, by analogy with `MapInjection`. *)

end

3. Proposal of extension of int.mlw in stdlib

module NumOfExt

  use int.Int
  use int.NumOf

  lemma Numof_no_add:
    forall p : int -> bool, a b c: int.
    a <= b < c -> not p b -> numof p a c = numof p a b + numof p (b+1) c

end

4. Type for {low,...,up}, proposed for a new file interval.mlw in stdlib

module Interval

  use int.Int

  val constant low : int (* lower interval endpoint *)
  val constant  up : int (* upper interval endpoint *)
  axiom Nonempty : low <= up

  type bint = {
    to_int: int
  } invariant { low <= to_int <= up }
    by { to_int = low }

  let constant low_bint : bint = { to_int = low }

  meta coercion function to_int

  axiom Extensionality : forall i j:bint. to_int i = to_int j -> i = j

  let (=) (i j: bint) : bool = to_int i = to_int j

  let predicate lt_bint (i j: bint) = to_int i < to_int j

  clone relations.TotalStrictOrder with
  type t = bint, predicate rel = lt_bint

  let function of_int (i:int) : bint
    requires { low <= i <= up }
    ensures  { result.to_int = i }
  =
    { to_int = i }

  lemma of_int_quasi_inj :
    forall i j: int. low <= i <= up -> low <= j <= up -> of_int i = of_int j -> i = j

  lemma of_intK: forall i:bint. of_int (to_int i) = i

  use int.NumOf

  let function numof_bint (p: bint -> bool) (a b: bint) : int
  =
    numof (fun (i:int) -> low <= i <= up && p (of_int i)) a.to_int b.to_int

end

5. Theory Of One Bijection

module TOOB

  type t
  predicate rel t t

  clone export Bijectivity with type t = t, type u = t, predicate rel = rel, axiom .

end

6. Models for TOOB

Hereafter we only consider models where permutations are endomaps on the type bint satisfying the predicate MapInjSurjBij.bijective.

module ModelTOOB

  use map.Map
  use Interval
  use MapInjSurjBij

  val constant sigma : map bint bint
  axiom sigma_bij : bijective sigma

  clone MapRelation with type t = bint, type u = bint, constant m = sigma, axiom Deter, axiom Total

  predicate rel_sigma (i j: bint) = map_rel sigma i j

  clone TOOB with type t = bint, predicate rel = rel_sigma

end

module Proposition2

  use map.Map
  use Interval
  use MapInjSurjBij

  type a
  predicate rel a a
  clone TOOB with type t = a, predicate rel = rel, axiom .

  function a2bint a : bint
  function bint2a bint : a
  clone functions.Bijective with type t = a, type u = bint,
    function t2u = a2bint, function u2t = bint2a, axiom Cancel, axiom Right.Cancel

  predicate map_rel (m: map 'a 'b) (x: 'a) (y: 'b) = (m[x] = y)

  predicate isomorphic (sigma : map bint bint) =
    exists f: map a bint. bijective f /\ forall x y:a. rel x y <-> map_rel sigma (f x) (f y)

  lemma ex_rel_permut : exists rel_permut : map bint bint.
    forall i j:bint. rel_permut[i] = j <-> rel (bint2a i) (bint2a j)

  lemma Proposition2 : exists sigma: map bint bint. bijective sigma /\ isomorphic sigma

end

7. Theory Of Two Orders

module TOTO

  type t            (* type of positions and values    *)
  predicate ltP t t (* strict total order on positions *)
  predicate ltV t t (* strict total order on values    *)

  clone export relations.TotalStrictOrder with type t = t, predicate rel = ltP, axiom .
  clone relations.TotalStrictOrder as V with type t = t, predicate rel = ltV, axiom .

end

8. Type for the arcs of the graph of a map

module MapGraph

  use int.Int
  use map.Map
  use Interval

  constant m : map bint bint
  type arrow = {
    source : bint;
    target : bint
  } invariant { target = m[source] }
    by { source = low_bint; target = m[low_bint] }

  axiom Extensionality: forall a b:arrow. a.source = b.source /\ a.target = b.target -> a = b

  let (=) (a b: arrow) : bool = a.source = b.source && a.target = b.target

  let predicate lt_source (a b: arrow) = lt_bint a.source b.source

  clone export relations.TotalStrictOrder with type t = arrow, predicate rel = lt_source

  lemma Source_inj: forall a b:arrow. a.source = b.source -> a = b

end

9. Models for TOTO

module ModelTOTO

  use int.Int
  use map.Map
  use Interval
  use MapInjSurjBij

  constant sigma : map bint bint
  axiom sigma_bij : bijective sigma

  clone MapGraph with constant m = sigma, axiom Extensionality (* provides type arrow, etc *)

  let predicate ltP_sigma (a b: arrow) = lt_bint a.source b.source
  let predicate ltV_sigma (a b: arrow) = lt_bint a.target b.target

  clone TOTO with type t = arrow, predicate ltP = ltP_sigma, predicate ltV = ltV_sigma

end

Restriction to integer intervals for simpler constructions and proofs

Hereafter we abandon the objectives of fidelity to [ABF20] and universality of logic with any support set, and we focus on types int and bint. Thus we get shorter definitions and computable predicates and functions.

1. Strict Total Order on one integer Interval

module STOI

  type t

  val predicate lt t t
  clone export relations.TotalStrictOrder with type t = t, predicate rel = lt, axiom .

  clone export relations.Irreflexive with type t = t, predicate rel = lt

end

2. Permutation model for STOI

2.1. From a permutation over [1..size]

module Gio20proposition5 (* [Gio20, Proposition 5] *)

  use int.Int
  use map.Map
  use MapInjSurjBij

  val constant size : int

  clone export Interval with val low = one, val up = size, axiom .

  val constant sigma : map bint bint
  axiom sigma_bij : bijective sigma

  let predicate lt_sigma (i j: bint) = lt_bint (sigma i) (sigma j)

  clone export STOI with type t = bint, val lt = lt_sigma

end

2.2. From a permutation over any interval [low..up]

module ModelSTOI (* [Gio21, Section 4, Paragraph 2] *)

  use map.Map
  use MapInjSurjBij

  clone export Interval with axiom .

  val constant sigma : map bint bint
  axiom sigma_bij : bijective sigma

  let predicate lt_map (m: map bint bint) (i j: bint) = lt_bint m[i] m[j]
  let predicate lt_sigma (i j: bint) = lt_map sigma i j

  clone export relations.TotalStrictOrder with type t = bint, predicate rel = lt_sigma

end

3. Two mutually inverse permutations associated to a strict total order

[ABF20] defines a rank function to associate a permutation to any model of TOTO, composed of two strict total orders. Here we associate a rank function to any strict total order on bint. Its type requires a proof that its range is bint. Then we prove (with Coq) that rank lt is injective for any strict total order lt. Surjectivity is more difficult to prove. We implement a candidate for an inverse function (not in [ABF20]). This implementation goes through a constructive definition of the minimum and maximum of a strict total order on bint, and of a function succ.

module Rank

  use ref.Ref
  use int.Int
  use int.NumOf
  use map.Map
  use NumOfExt
  use MapInjSurjBij

  clone export Interval with axiom .

  predicate trans (rel : 'a -> 'a -> bool) = forall x y z:'a. rel x y -> rel y z -> rel x z
  predicate asymm (rel : 'a -> 'a -> bool) = forall x y:'a. rel x y -> not rel y x
  predicate partialStrictOrder (rel : 'a -> 'a -> bool) = trans rel /\ asymm rel
  predicate trichotomy (rel : 'a -> 'a -> bool) = forall x y:'a. rel x y \/ rel y x \/ x = y
  predicate totalStrictOrder (rel : 'a -> 'a -> bool) = partialStrictOrder rel /\ trichotomy rel

  lemma irrefl :
    forall lt : 'a -> 'a -> bool. asymm lt -> forall a:'a. lt a a = false

  let predicate lt_int (lt : bint -> bint -> bool) (a:bint) (j:int) = low <= j <= up && lt (of_int j) a

  lemma numof_max : forall lt : bint -> bint -> bool. asymm lt ->
    forall a:bint. numof (lt_int lt a) low (up+1) <= up - low

  let predicate lt_map (m: map bint bint) (i j:bint) = lt_bint m[i] m[j]

  lemma lt_map_bij_sto: forall sigma : map bint bint. bijective sigma ->
    totalStrictOrder (fun i -> fun j -> lt_map sigma i j)

  let function rank (lt : bint -> bint -> bool) (a:bint) : bint
    requires { totalStrictOrder lt }
  =
    of_int ((numof (lt_int lt a) low (up+1)) + low)

  lemma rank_lt_inj: forall lt : bint -> bint -> bool. totalStrictOrder lt -> injective (rank lt)

  predicate is_max_left (lt : bint -> bint -> bool) (m:bint) (i:int) =
    forall j. low <= j <= i -> lt (of_int j) m \/ of_int j = m

  predicate is_max (lt : bint -> bint -> bool) (m:bint) = is_max_left lt m up

  let function max (lt : bint -> bint -> bool) : bint
    requires { totalStrictOrder lt }
    ensures  { is_max lt result }
  =
    let ref m = of_int low in
    for i = low+1 to up do
      invariant { low+1 <= i <= up+1 }
      invariant { is_max_left lt m (i-1) }
      let j = of_int i in
      if lt m j then m := j
    done;
    m

  lemma max_is_max : forall lt : bint -> bint -> bool. totalStrictOrder lt ->
    forall a. a = max lt <-> is_max lt a

  predicate is_succ_left (lt : bint -> bint -> bool) (a b:bint) (i:int) = lt a b /\
    forall j. low <= j <= i -> let c = of_int j in not (lt a c && lt c b)

  predicate is_succ (lt : bint -> bint -> bool) (a b:bint) = is_succ_left lt a b up

  let succ (lt : bint -> bint -> bool) (a:bint) : bint
    requires { totalStrictOrder lt }
    requires { a <> max lt }
    ensures  { is_succ lt a result }
  =
    let ref i = low in
    while i <= up && not (lt a (of_int i)) do  (* the first loop searches some (of_int i) greater than a *)
      invariant { low <= i <= up+1 }
      invariant { forall j. low <= j < i -> not (lt a (of_int j)) }
      variant { up - i }
      i := i+1
    done;
    let ref b = of_int i in (* candidate for (succ a) *)
    i := i+1;
    while i <= up do (* the second loop improves this (of_int i) greater than a *)
      invariant { low <= i <= up+1 }
      invariant { is_succ_left lt a b (i-1) }
      variant { up - i }
      let k = of_int i in
      if lt a k && lt k b then b := k;
      i := i+1
    done;
    b

  predicate is_min_left (lt : bint -> bint -> bool) (m:bint) (i:int) =
    forall j. low <= j <= i -> lt m (of_int j) \/ m = of_int j

  predicate is_min (lt : bint -> bint -> bool) (m:bint) = is_min_left lt m up

  let function min (lt : bint -> bint -> bool) : bint
    requires { totalStrictOrder lt }
    ensures  { is_min lt result }
  =
    let ref m = of_int low in
    for i = low+1 to up do
      invariant { low+1 <= i <= up+1 }
      invariant { is_min_left lt m (i-1) }
      let j = of_int i in
      if lt j m then m := j
    done;
    m

  let function unrank (lt : bint -> bint -> bool) (i:bint) : bint
    requires { totalStrictOrder lt }
  =
    let ref k = i.to_int in
    let ref j = min lt in
    while not (j = max lt) && k > low do
      variant { k+1-low }
      j := succ lt j;
      k := k-1
    done;
    j

  lemma rank_ltK: forall lt. totalStrictOrder lt -> forall i. rank lt (unrank lt i) = i

  lemma unrank_ltK: forall lt. totalStrictOrder lt -> forall i. unrank lt (rank lt i) = i

  lemma lt_mapK: forall lt. totalStrictOrder lt -> lt_map (rank lt) = lt

  lemma Proposition1: forall lt. totalStrictOrder lt ->
    exists sigma. bijective sigma /\ lt_map sigma = lt

end

4. Enumerative tests

module Tests

  use int.Int
  use array.Array
  (* Enumerative testing tool *)
  use Enum.Permutation
  use SCheck.Test
  use SCheck.SCheck
  use SCheck.SCheck_runner

  let constant size : int = 6
  clone export Rank with val low = one, val up = size, axiom .

  let function array_sto (a:{array int}) : bint -> bint -> bool
    requires { a.length = size /\ is_permut a }
    ensures  { totalStrictOrder result }
  =
    fun x -> fun y -> a[x.to_int-one] < a[y.to_int-one]
  (* `-one` because `a` is on [0..n-1] whereas `bint` is [`one`..`size`] *)

  let function rank_cancel lt : bool
    requires { totalStrictOrder lt }
  =
    for i = one to size do
      let j = of_int i in
      if not (rank lt (unrank lt j) = j) then return false
    done;
    true

  let rank_cancel_array (a:array int) : bool
    requires { a.length = size /\ is_permut a }
  =
    rank_cancel (array_sto a)

  let function rank_cancel_test
  =
    SCheck_runner.run_tests (Test.make SCheck.(permut_of_size size) rank_cancel_array)

end