Library prosa.implementation.refinements.refinements

Require Export prosa.implementation.definitions.task.
Require Export prosa.implementation.facts.extrapolated_arrival_curve.
Require Export NArith.
From CoqEAL Require Export hrel param refinements binnat.
Export Refinements.Op.

Refinements Library

This file contains a variety of support definitions and proofs for refinements. Refinements allow to convert unary-number definitions into binary-number ones. This is used for the sole purpose of performing computations involving large numbers, and can safely be ignored if this is of no interest to the reader. See Maida et al. (ECRTS 2022) for the motivation and further details, available at https://drops.dagstuhl.de/opus/volltexte/2022/16336/.

Brief Introduction

Consider the refinement refines (Rnat ==> Rnat ==> Rnat)%rel maxn maxn_T. This statements uses the relation Rnat, which relates each unary number with its binary counterpart.

Proving this statement shows that the maxn function is isomorphic to maxn_T, i.e., given two unary numbers (a,b) and two binary numbers (a', b'), Rnat a b → Rnat a' b' → Rnat (maxn a b) (maxn_T a' b'). In other words, if a is related to a' and b to b', then maxn a b is related to maxn_T a' b'). This statement is encoded in a succinct way via the ==> notation.

For more information, refer to https://hal.inria.fr/hal-01113453/document.

Auxiliary Definitions

First, we define a convenience function that translates a list of unary natural numbers to binary numbers...

Definition m_b2n b := map nat_of_bin b.
Definition m_n2b n := map bin_of_nat n.

... and an analogous version that works on pairs.

Definition tmap {X Y : Type} (f : X → Y) (t : X × X) := (f (fst t), f (snd t)).
Definition tb2tn t := tmap nat_of_bin t.
Definition tn2tb t := tmap bin_of_nat t.
Definition m_tb2tn xs := map tb2tn xs.
Definition m_tn2tb xs := map tn2tb xs.

Basic Arithmetic

In the following, we encode refinements for a variety of basic arithmetic functions.

Definitions

We begin by defining a generic version of the functions we seek to refine.

Section Definitions.

Consider a generic type T supporting basic arithmetic operations, neutral elements, and comparisons.

  Context {T : Type}.
  Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
      !div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.

We redefine the predecessor function. Note that, although this definition uses common notation, the %C indicates that we refer to the generic type T defined above.

Definition predn_T (n : T) := (n - 1)%C.

Further, we redefine the maximum and minimum functions...

Definition maxn_T (m n : T) := (if m < n then n else m)%C.
Definition minn_T (m n : T) := (if m < n then m else n)%C.

... the "divides" function...

Definition dvdn_T (d : T) (m : T) := (m %% d == 0)%C.

... and the division with ceiling function.

Definition div_ceil_T (a : T) (b : T) :=
if dvdn_T b a then (a %/ b)%C else (1 + a %/ b)%C.

End Definitions.

Refinements

We now establish the desired refinements.

First, we prove a refinement for the b2n function.

Global Instance refine_b2n :
refines (unify (A:=N) ==> Rnat)%rel nat_of_bin id.

Second, we prove a refinement for the predecessor function.

Global Instance Rnat_pred :
refines (Rnat ==> Rnat)%rel predn predn_T.

Next, we prove a refinement for the "divides" function.

Global Instance refine_dvdn :
refines (Rnat ==> Rnat ==> bool_R)%rel dvdn dvdn_T.

Next, we prove a refinement for the division with ceiling.

Global Instance refine_div_ceil :
refines (Rnat ==> Rnat ==> Rnat)%rel div_ceil div_ceil_T.

Next, we prove a refinement for the minimum function.

Global Instance refine_minn :
refines (Rnat ==> Rnat ==> Rnat)%rel minn minn_T.

Finally, we prove a refinement for the maximum function.

Global Instance refine_maxn :
refines (Rnat ==> Rnat ==> Rnat)%rel maxn maxn_T.

Supporting Lemmas

As the next step, we prove some helper lemmas used in refinements. We differentiate class instances from lemmas, as lemmas are applied manually, and not via the typeclass engine.

First, we prove that negating a positive, binary number results in 0.

Lemma posBinNatNotZero:
∀ p, ¬ (nat_of_bin (N.pos p)) = O.

Next, we prove that, if the successor of a unary number b corresponds to a positive binary number p, then b corresponds to the predecessor of p.

Lemma eq_SnPos_to_nPred:
∀ b p, Rnat b .+1 (N.pos p) → Rnat b (Pos.pred_N p).

Finally, we prove that if two unary numbers a and b have the same numeral as, respectively, two binary numbers a' and b', then a<b is rewritable into a'<b'.

Lemma refine_ltn :
  ∀ a a' b b',
    Rnat a a' →
    Rnat b b' →
    bool_R (a < b) (a' < b')%C.

Functions on Lists

In the following, we encode refinements for a variety of functions related to lists.

Definitions

We begin by defining a generic version of the functions we want to refine.

Section Definitions.

Consider a generic type T supporting basic arithmetic operations and comparisons

  Context {T : Type}.
  Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
      !div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.

We redefine the iota function, ...

  Fixpoint iota_T (a : T) (b : nat): seq T :=
    match b with
    | 0 ⇒ [::]
    | S b' ⇒ a :: iota_T (a + 1)%C b'
    end.

... the size function, ...

  Fixpoint size_T {X : Type} (s : seq X): T :=
    match s with
    | [::] ⇒ 0%C
    | _ :: s' ⇒ (1 + size_T s')%C
    end.

... the forward-shift function, ...

Definition shift_points_pos_T (xs : seq T) (s : T) : seq T :=
map (fun x ⇒ s + x)%C xs.

... and the backwards-shift function.

  Definition shift_points_neg_T (xs : seq T) (s : T) : seq T :=
    let nonsmall := filter (fun x ⇒ s ≤ x)%C xs in
    map (fun x ⇒ x - s)%C nonsmall.

End Definitions.

Refinements

In the following, we establish the required refinements.

First, we prove a refinement for the map function.

Global Instance refine_map :
  ∀ {A A' B B': Type}
    (F : A → B) (F' : A' → B')
    (rA : A → A' → Type) (rB : B → B' → Type) xs xs',
    refines (list_R rA) xs xs' →
    refines (rA ==> rB)%rel F F' →
    refines (list_R rB)%rel (map F xs) (map F' xs').

Second, we prove a refinement for the zip function.

Global Instance refine_zip :
refines (list_R Rnat ==> list_R Rnat ==> list_R (prod_R Rnat Rnat))%rel zip zip.

Next, we prove a refinement for the all function.

Global Instance refine_all :
∀ {A A' : Type} (rA : A → A' → Type),
refines ((rA ==> bool_R) ==> list_R rA ==> bool_R)%rel all all.

Next, we prove a refinement for the flatten function.

Global Instance refine_flatten :
∀ {A A': Type} (rA : A → A' → Type),
refines (list_R (list_R rA) ==> list_R rA)%rel flatten flatten.

Next, we prove a refinement for the cons function.

Global Instance refine_cons A C (rAC : A → C → Type) :
refines (rAC ==> list_R rAC ==> list_R rAC)%rel cons cons.

Next, we prove a refinement for the nil function.

Global Instance refine_nil A C (rAC : A → C → Type) :
refines (list_R rAC) nil nil.

Next, we prove a refinement for the last function.

Global Instance refine_last :
∀ {A B : Type} (rA : A → B → Type),
refines (rA ==> list_R rA ==> rA)%rel last last.

Next, we prove a refinement for the size function.

Global Instance refine_size A C (rAC : A → C → Type) :
refines (list_R rAC ==> Rnat)%rel size size_T.

Next, we prove a refinement for the iota function when applied to the successor of a number.

Lemma iotaTsuccN :
∀ (a : N) p,
iota_T a (N.succ (Pos.pred_N p)) = a :: iota_T (succN a) (Pos.pred_N p).

Next, we prove a refinement for the iota function.

Global Instance refine_iota :
refines (Rnat ==> Rnat ==> list_R Rnat)%rel iota iota_T.

Next, we prove a refinement for the shift_points_pos function.

Global Instance refine_shift_points_pos:
refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel shift_points_pos shift_points_pos_T.

Next, we prove a refinement for the shift_points_neg function.

Global Instance refine_shift_points_neg:
refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel shift_points_neg shift_points_neg_T.

Finally, we prove that the if the nat_of_bin function is applied to a list, the result is the original list translated to binary.

Global Instance refine_abstract :
∀ xs,
refines (list_R Rnat)%rel (map nat_of_bin xs) xs | 0.

Supporting Lemmas

As the last step, we prove some helper lemmas used in refinements. Again, we differentiate class instances from lemmas, as lemmas are applied manually, not via the typeclass engine.

First, we prove a refinement for the foldr function.

Lemma refine_foldr_lemma :
refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> list_R Rnat ==> Rnat)%rel foldr foldr.
Section GenericLists.

Now, consider two types T1 and T2, and two lists of the respective type.

Context {T1 T2 : Type}.
Variable (xs : seq T1) (xs' : seq T2).

We prove a refinement for the foldr function when applied to a map and filter operation.

  Lemma refine_foldr:
    ∀ (R : T1 → bool) (R' : T2 → bool) (F : T1 → nat) (F' : T2 → N),
    ∀ (rT : T1 → T2 → Type),
      refines ( list_R rT )%rel xs xs' →
      refines ( rT ==> Rnat )%rel F F' →
      refines ( rT ==> bool_R )%rel R R' →
      refines Rnat (\sum_(x <- xs | R x ) F x) (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x']).

Next, we prove a refinement for the foldr function when applied to a map operation.

  Lemma refine_uncond_foldr :
    ∀ (F : T1 → nat) (F' : T2 → N),
    ∀ (rT : T1 → T2 → Type),
      refines ( list_R rT )%rel xs xs' →
      refines ( rT ==> Rnat )%rel F F' →
      refines Rnat (\sum_(x <- xs ) F x) (foldr +%C 0%C [seq F' x' | x' <- xs']).

Next, we prove a refinement for the foldr function when applied to a max operation over a list. In terms, the list is the result of a map and filter operation.

  Lemma refine_foldr_max :
    ∀ (R : T1 → bool) (R' : T2 → bool)
      (F : T1 → nat) (F' : T2 → N),
    ∀ (rT : T1 → T2 → Type),
      refines ( list_R rT )%rel xs xs' →
      refines ( rT ==> Rnat )%rel F F' →
      refines ( rT ==> bool_R )%rel R R' →
      refines Rnat (\max_(x <- xs | R x ) F x) (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x']).

End GenericLists.