Require Export prosa.implementation.definitions.task.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.facts.extrapolated_arrival_curve.
Require Export NArith.
From CoqEAL Require Export hrel param refinements binnat.
Serlib plugin: coq-paramcoq.plugin is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file paramcoq.cmxs (using legacy method) ... done]
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.
refines (unify (A:=N) ==> Rnat) nat_of_bin id
Proof.
refines (unify (A:=N) ==> Rnat) nat_of_bin id
  apply refines_abstr; move => n n' Rn.
n, n': N
Rn: refines (unify (A:=N)) n n'
refines Rnat n n'
  compute in Rn; destruct refines_key in Rn; subst.
n': N
refines Rnat n' n'
  by apply trivial_refines.
Qed.

(** Second, we prove a refinement for the predecessor function. *)
Global Instance Rnat_pred :
  refines (Rnat ==> Rnat)%rel predn predn_T.
refines (Rnat ==> Rnat) predn predn_T
Proof.
refines (Rnat ==> Rnat) predn predn_T
  rewrite !refinesE => a a' Ra.
a: nat
a': N
Ra: Rnat a a'
Rnat a.-1 (predn_T a')
  rewrite -subn1 /predn_T.
a: nat
a': N
Ra: Rnat a a'
Rnat (a - 1) (a' - 1)%C
  by apply: refinesP.
Qed.

(** Next, we prove a refinement for the "divides" function. *)
Global Instance refine_dvdn :
  refines (Rnat ==> Rnat ==> bool_R)%rel dvdn dvdn_T.
refines (Rnat ==> Rnat ==> bool_R) dvdn dvdn_T
Proof.
refines (Rnat ==> Rnat ==> bool_R) dvdn dvdn_T
  apply refines_abstr2; unfold "%|", dvdn_T; move=> x x' rx y y' ry.
x: nat
x': N
rx: refines Rnat x x'
y: nat
y': N
ry: refines Rnat y y'
refines bool_R (y %% x == 0) (y' %% x' == 0)%C
  by exact: refines_apply.
Qed.

(** 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.
refines (Rnat ==> Rnat ==> Rnat) div_ceil div_ceil_T
Proof.
refines (Rnat ==> Rnat ==> Rnat) div_ceil div_ceil_T
  apply refines_abstr2; unfold div_ceil, div_ceil_T.
forall (a : nat) (b : N),
refines Rnat a b ->
forall (a' : nat) (b' : N),
refines Rnat a' b' ->
refines Rnat
  (if a' %| a then a %/ a' else (a %/ a').+1)
  (if dvdn_T b' b
   then (b %/ b')%C
   else (1 + b %/ b')%C)
  move => x x' Rx y y' Ry.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
refines Rnat (if y %| x then x %/ y else (x %/ y).+1)
  (if dvdn_T y' x'
   then (x' %/ y')%C
   else (1 + x' %/ y')%C)
  have <-: y %| x = dvdn_T y' x'.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
(y %| x) = dvdn_T y' x'
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
refines Rnat (if y %| x then x %/ y else (x %/ y).+1)
  (if y %| x then (x' %/ y')%C else (1 + x' %/ y')%C)
  {
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
(y %| x) = dvdn_T y' x' eapply refines_eq.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
refines eq (y %| x) (dvdn_T y' x')
    apply refines_bool_eq; unfold "%|", dvdn_T.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
refines bool_R (x %% y == 0) (x' %% y' == 0)%C
    by refines_apply. }
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
refines Rnat (if y %| x then x %/ y else (x %/ y).+1)
  (if y %| x then (x' %/ y')%C else (1 + x' %/ y')%C)
  destruct (y %| x) eqn:B; first by eapply refines_apply;[refines_abstr| exact: Ry].
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines Rnat (x %/ y).+1 (1 + x' %/ y')%C
  {
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines Rnat (x %/ y).+1 (1 + x' %/ y')%C eapply refines_apply.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines (?R ==> Rnat) succn (+%C 1%C)
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines ?R (x %/ y) (x' %/ y')%C
    -
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines (?R ==> Rnat) succn (+%C 1%C) refines_abstr.
    -
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines Rnat (x %/ y) (x' %/ y')%C eapply refines_apply.
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines (?R ==> Rnat) (divn x) (div_op x')
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines ?R y y'
      +
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines (?R ==> Rnat) (divn x) (div_op x') by refines_abstr.
      +
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = false
refines Rnat y y' exact: Ry. }
Qed.

(** Next, we prove a refinement for the minimum function. *)
Global Instance refine_minn :
  refines (Rnat ==> Rnat ==> Rnat)%rel minn minn_T.
refines (Rnat ==> Rnat ==> Rnat) minn minn_T
Proof.
refines (Rnat ==> Rnat ==> Rnat) minn minn_T
  intros *; rewrite refinesE => a a' Ra b b' Rb; unfold minn, minn_T.
a: nat
a': N
Ra: Rnat a a'
b: nat
b': N
Rb: Rnat b b'
Rnat (if a < b then a else b)
  (if (a' < b')%C then a' else b')
  compute in Ra, Rb; subst.
a', b': N
Rnat (if a' < b' then a' else b')
  (if (a' < b')%C then a' else b')
  rename a' into a, b' into b.
a, b: N
Rnat (if a < b then a else b)
  (if (a < b)%C then a else b)
  have <- : (a < b) = (a < b)%C; last by destruct (a < b).
a, b: N
(a < b) = (a < b)%C
  unfold lt_op, lt_N.
a, b: N
(a < b) = (a <? b)%N
  destruct (a < b) eqn:EQ; symmetry; first by apply N.ltb_lt; apply /Rnat_ltP.
a, b: N
EQ: (a < b) = false
(a <? b)%N = false
  apply N.ltb_ge.
a, b: N
EQ: (a < b) = false
(b <= a)%N
  apply negbT in EQ; rewrite -leqNgt in EQ.
a, b: N
EQ: b <= a
(b <= a)%N
  apply /N.leb_spec0.
a, b: N
EQ: b <= a
(b <=? a)%N
  by move: Rnat_leE => LE; unfold leq_op, leq_N in LE; rewrite LE.
Qed.

(** Finally, we prove a refinement for the maximum function. *)
Global Instance refine_maxn :
  refines (Rnat ==> Rnat ==> Rnat)%rel maxn maxn_T.
refines (Rnat ==> Rnat ==> Rnat) maxn maxn_T
Proof.
refines (Rnat ==> Rnat ==> Rnat) maxn maxn_T
  intros *; rewrite refinesE => a a' Ra b b' Rb; unfold maxn, maxn_T.
a: nat
a': N
Ra: Rnat a a'
b: nat
b': N
Rb: Rnat b b'
Rnat (if a < b then b else a)
  (if (a' < b')%C then b' else a')
  compute in Ra, Rb; subst.
a', b': N
Rnat (if a' < b' then b' else a')
  (if (a' < b')%C then b' else a')
  rename a' into a, b' into b.
a, b: N
Rnat (if a < b then b else a)
  (if (a < b)%C then b else a)
  have <- : (a < b) = (a < b)%C; last by destruct (a < b).
a, b: N
(a < b) = (a < b)%C
  unfold lt_op, lt_N.
a, b: N
(a < b) = (a <? b)%N
  destruct (a < b) eqn:EQ; symmetry; first by apply N.ltb_lt; apply /Rnat_ltP.
a, b: N
EQ: (a < b) = false
(a <? b)%N = false
  apply N.ltb_ge.
a, b: N
EQ: (a < b) = false
(b <= a)%N
  apply negbT in EQ; rewrite -leqNgt in EQ.
a, b: N
EQ: b <= a
(b <= a)%N
  apply /N.leb_spec0.
a, b: N
EQ: b <= a
(b <=? a)%N
  by move: Rnat_leE => LE; unfold leq_op, leq_N in LE; rewrite LE.
Qed.

(** ** 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:
  forall p, ~ (nat_of_bin (N.pos p)) = O.
forall p : positive, N.pos p <> 0
Proof.
forall p : positive, N.pos p <> 0
  rewrite -[0]bin_of_natK.
forall p : positive, N.pos p <> bin_of_nat 0
  intros p EQ.
p: positive
EQ: N.pos p = bin_of_nat 0
False
  have BJ := @Bijective _ _ nat_of_bin bin_of_nat.
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel nat_of_bin bin_of_nat ->
cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
False
  feed_n 2 BJ.
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel nat_of_bin bin_of_nat ->
cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
cancel nat_of_bin bin_of_nat
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
cancel bin_of_nat nat_of_bin
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: bijective nat_of_bin
False
  {
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel nat_of_bin bin_of_nat ->
cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
cancel nat_of_bin bin_of_nat by intros ?; rewrite bin_of_natE; apply nat_of_binK. }
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
cancel bin_of_nat nat_of_bin
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: bijective nat_of_bin
False
  {
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: cancel bin_of_nat nat_of_bin ->
bijective nat_of_bin
cancel bin_of_nat nat_of_bin by apply bin_of_natK. }
p: positive
EQ: N.pos p = bin_of_nat 0
BJ: bijective nat_of_bin
False
  apply bij_inj in BJ; apply BJ in EQ; clear BJ.
p: positive
EQ: N.pos p = bin_of_nat 0
False
  by destruct p.
Qed.

(** 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:
  forall b p, Rnat b.+1 (N.pos p) -> Rnat b (Pos.pred_N p).
forall (b : nat) (p : positive),
Rnat b.+1 (N.pos p) -> Rnat b (Pos.pred_N p)
Proof.
forall (b : nat) (p : positive),
Rnat b.+1 (N.pos p) -> Rnat b (Pos.pred_N p)
  move => b p.
b: nat
p: positive
Rnat b.+1 (N.pos p) -> Rnat b (Pos.pred_N p)
  rewrite /Rnat /fun_hrel => EQ.
b: nat
p: positive
EQ: N.pos p = b.+1
Pos.pred_N p = b
  rewrite -addn1 in EQ.
b: nat
p: positive
EQ: N.pos p = b + 1
Pos.pred_N p = b
  apply /eqP; rewrite -(eqn_add2r 1) -EQ; apply /eqP.
b: nat
p: positive
EQ: N.pos p = b + 1
Pos.pred_N p + 1 = N.pos p
  move: (nat_of_add_bin (Pos.pred_N p) 1%N) => EQadd1.
b: nat
p: positive
EQ: N.pos p = b + 1
EQadd1: (Pos.pred_N p + 1)%N = Pos.pred_N p + 1%N
Pos.pred_N p + 1 = N.pos p
  by rewrite -EQadd1 N.add_1_r N.succ_pos_pred.
Qed.

(** 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 :
  forall a a' b b',
    Rnat a a' ->
    Rnat b b' ->
    bool_R (a < b) (a' < b')%C.
forall (a : nat) (a' : N) (b : nat) (b' : N),
Rnat a a' -> Rnat b b' -> bool_R (a < b) (a' < b')%C
Proof.
forall (a : nat) (a' : N) (b : nat) (b' : N),
Rnat a a' -> Rnat b b' -> bool_R (a < b) (a' < b')%C
  move=> a a' b b' Ra Rb.
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
bool_R (a < b) (a' < b')%C
  replace (@lt_op N lt_N a' b') with (@leq_op N leq_N (1 + a')%N b');
    first by apply refinesP; refines_apply.
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
((1 + a')%N <= b')%C = (a' < b')%C
  unfold leq_op, leq_N, lt_op, lt_N.
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
(1 + a' <=? b')%N = (a' <? b')%N
  apply /N.leb_spec0; case (a' <? b')%N eqn:LT.
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
LT: (a' <? b')%N = true
(1 + a' <= b')%N
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
LT: (a' <? b')%N = false
~ (1 + a' <= b')%N
  -
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
LT: (a' <? b')%N = true
(1 + a' <= b')%N by move: LT => /N.ltb_spec0 LT; rewrite N.add_1_l; apply N.le_succ_l.
  -
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
LT: (a' <? b')%N = false
~ (1 + a' <= b')%N rewrite N.add_1_l => CONTR; apply N.le_succ_l in CONTR.
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'
LT: (a' <? b')%N = false
CONTR: (a' < b')%N
False
    by move: LT => /negP LT; apply: LT; apply /N.ltb_spec0.
Qed.


(** * 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 :
  forall {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').
forall (A A' B B' : Type) (F : A -> B) (F' : A' -> B')
  (rA : A -> A' -> Type) (rB : B -> B' -> Type)
  (xs : seq A) (xs' : seq A'),
refines (list_R rA) xs xs' ->
refines (rA ==> rB) F F' ->
refines (list_R rB) [seq F i | i <- xs]
  [seq F' i | i <- xs']
Proof.
forall (A A' B B' : Type) (F : A -> B) (F' : A' -> B')
  (rA : A -> A' -> Type) (rB : B -> B' -> Type)
  (xs : seq A) (xs' : seq A'),
refines (list_R rA) xs xs' ->
refines (rA ==> rB) F F' ->
refines (list_R rB) [seq F i | i <- xs]
  [seq F' i | i <- xs']
  intros * Rxs RF; rewrite refinesE.
A, A', B, B': Type
F: A -> B
F': A' -> B'
rA: A -> A' -> Type
rB: B -> B' -> Type
xs: seq A
xs': seq A'
Rxs: refines (list_R rA) xs xs'
RF: refines (rA ==> rB) F F'
list_R rB [seq F i | i <- xs] [seq F' i | i <- xs']
  eapply map_R; last first.
A, A', B, B': Type
F: A -> B
F': A' -> B'
rA: A -> A' -> Type
rB: B -> B' -> Type
xs: seq A
xs': seq A'
Rxs: refines (list_R rA) xs xs'
RF: refines (rA ==> rB) F F'
list_R ?T1_R xs xs'
A, A', B, B': Type
F: A -> B
F': A' -> B'
rA: A -> A' -> Type
rB: B -> B' -> Type
xs: seq A
xs': seq A'
Rxs: refines (list_R rA) xs xs'
RF: refines (rA ==> rB) F F'
forall (t₁ : A) (t₂ : A'),
?T1_R t₁ t₂ -> rB (F t₁) (F' t₂)
  -
A, A', B, B': Type
F: A -> B
F': A' -> B'
rA: A -> A' -> Type
rB: B -> B' -> Type
xs: seq A
xs': seq A'
Rxs: refines (list_R rA) xs xs'
RF: refines (rA ==> rB) F F'
list_R ?T1_R xs xs' by rewrite refinesE in Rxs; apply Rxs.
  -
A, A', B, B': Type
F: A -> B
F': A' -> B'
rA: A -> A' -> Type
rB: B -> B' -> Type
xs: seq A
xs': seq A'
Rxs: refines (list_R rA) xs xs'
RF: refines (rA ==> rB) F F'
forall (t₁ : A) (t₂ : A'),
rA t₁ t₂ -> rB (F t₁) (F' t₂) by intros x x' Rx; rewrite refinesE in RF; apply RF.
Qed.

(** 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.
refines
  (list_R Rnat ==>
   list_R Rnat ==> list_R (prod_R Rnat Rnat)) zip zip
Proof.
refines
  (list_R Rnat ==>
   list_R Rnat ==> list_R (prod_R Rnat Rnat)) zip zip by rewrite refinesE => xs xs' Rxs ys ys' Rys; apply zip_R. Qed.

(** Next, we prove a refinement for the [all] function. *)
Global Instance refine_all :
  forall {A A' : Type} (rA : A -> A' -> Type),
    refines ((rA ==> bool_R) ==> list_R rA ==> bool_R)%rel all all.
forall (A A' : Type) (rA : A -> A' -> Type),
refines ((rA ==> bool_R) ==> list_R rA ==> bool_R) all
  all
Proof.
forall (A A' : Type) (rA : A -> A' -> Type),
refines ((rA ==> bool_R) ==> list_R rA ==> bool_R) all
  all
  intros.
A, A': Type
rA: A -> A' -> Type
refines ((rA ==> bool_R) ==> list_R rA ==> bool_R) all
  all
  rewrite refinesE => P P' RP xs xs' Rxs.
A, A': Type
rA: A -> A' -> Type
P: A -> bool
P': A' -> bool
RP: (rA ==> bool_R)%rel P P'
xs: seq A
xs': seq A'
Rxs: list_R rA xs xs'
bool_R (all P xs) (all P' xs')
  eapply all_R; last by apply Rxs.
A, A': Type
rA: A -> A' -> Type
P: A -> bool
P': A' -> bool
RP: (rA ==> bool_R)%rel P P'
xs: seq A
xs': seq A'
Rxs: list_R rA xs xs'
forall (t₁ : A) (t₂ : A'),
rA t₁ t₂ -> bool_R (P t₁) (P' t₂)
  by intros x x' Rx; apply RP.
Qed.

(** Next, we prove a refinement for the [flatten] function. *)
Global Instance refine_flatten :
  forall {A A': Type} (rA : A -> A' -> Type),
    refines (list_R (list_R rA) ==> list_R rA)%rel flatten flatten.
forall (A A' : Type) (rA : A -> A' -> Type),
refines (list_R (list_R rA) ==> list_R rA) flatten
  flatten
Proof.
forall (A A' : Type) (rA : A -> A' -> Type),
refines (list_R (list_R rA) ==> list_R rA) flatten
  flatten
  by intros; rewrite refinesE => xss xss' Rxss; eapply flatten_R.
Qed.

(** 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.
A, C: Type
rAC: A -> C -> Type
refines (rAC ==> list_R rAC ==> list_R rAC) cons cons
Proof.
A, C: Type
rAC: A -> C -> Type
refines (rAC ==> list_R rAC ==> list_R rAC) cons cons
  by rewrite refinesE => h h' rh t t' rt; apply list_R_cons_R.
Qed.

(** 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.
A, C: Type
rAC: A -> C -> Type
refines (list_R rAC) [::] [::]
Proof.
A, C: Type
rAC: A -> C -> Type
refines (list_R rAC) [::] [::]
  by rewrite refinesE; apply list_R_nil_R.
Qed.

(** Next, we prove a refinement for the [last] function. *)
Global Instance refine_last :
  forall {A B : Type} (rA : A -> B -> Type),
    refines (rA ==> list_R rA ==> rA)%rel last last.
forall (A B : Type) (rA : A -> B -> Type),
refines (rA ==> list_R rA ==> rA) last last
Proof.
forall (A B : Type) (rA : A -> B -> Type),
refines (rA ==> list_R rA ==> rA) last last
  move=> A B rA; rewrite refinesE => d d' Rd xs xs' Rxs.
A, B: Type
rA: A -> B -> Type
d: A
d': B
Rd: rA d d'
xs: seq A
xs': seq B
Rxs: list_R rA xs xs'
rA (last d xs) (last d' xs')
  elim: xs d d' Rd xs' Rxs => [|a xs IHxs] d d' Rd xs' Rxs.
A, B: Type
rA: A -> B -> Type
d: A
d': B
Rd: rA d d'
xs': seq B
Rxs: list_R rA [::] xs'
rA (last d [::]) (last d' xs')
A, B: Type
rA: A -> B -> Type
a: A
xs: seq A
IHxs: forall (d : A) (d' : B),
rA d d' ->
forall xs' : seq B,
list_R rA xs xs' ->
rA (last d xs) (last d' xs')
d: A
d': B
Rd: rA d d'
xs': seq B
Rxs: list_R rA (a :: xs) xs'
rA (last d (a :: xs)) (last d' xs')
  -
A, B: Type
rA: A -> B -> Type
d: A
d': B
Rd: rA d d'
xs': seq B
Rxs: list_R rA [::] xs'
rA (last d [::]) (last d' xs') by destruct xs'; last inversion Rxs.
  -
A, B: Type
rA: A -> B -> Type
a: A
xs: seq A
IHxs: forall (d : A) (d' : B),
rA d d' ->
forall xs' : seq B,
list_R rA xs xs' ->
rA (last d xs) (last d' xs')
d: A
d': B
Rd: rA d d'
xs': seq B
Rxs: list_R rA (a :: xs) xs'
rA (last d (a :: xs)) (last d' xs') case: xs' Rxs => [|b xs'] Rxs; first by inversion Rxs.
A, B: Type
rA: A -> B -> Type
a: A
xs: seq A
IHxs: forall (d : A) (d' : B),
rA d d' ->
forall xs' : seq B,
list_R rA xs xs' ->
rA (last d xs) (last d' xs')
d: A
d': B
Rd: rA d d'
b: B
xs': seq B
Rxs: list_R rA (a :: xs) (b :: xs')
rA (last d (a :: xs)) (last d' (b :: xs'))
    exact: last_R.
Qed.

(** 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.
A, C: Type
rAC: A -> C -> Type
refines (list_R rAC ==> Rnat) size size_T
Proof.
A, C: Type
rAC: A -> C -> Type
refines (list_R rAC ==> Rnat) size size_T
  apply: refines_abstr => s s'; rewrite !refinesE.
A, C: Type
rAC: A -> C -> Type
s: seq A
s': seq C
list_R rAC s s' -> Rnat (size s) (size_T s')
  by elim=> [//|a a' Ra {}s {}s' Rs IHs] /=; apply: refinesP.
Qed.

(** Next, we prove a refinement for the [iota] function when applied
        to the successor of a number. *)
Lemma iotaTsuccN :
  forall (a : N) p,
    iota_T a (N.succ (Pos.pred_N p)) = a :: iota_T (succN a) (Pos.pred_N p).
forall (a : N) (p : positive),
iota_T a (N.succ (Pos.pred_N p)) =
a :: iota_T (succN a) (Pos.pred_N p)
Proof.
forall (a : N) (p : positive),
iota_T a (N.succ (Pos.pred_N p)) =
a :: iota_T (succN a) (Pos.pred_N p)
  move=> a p.
a: N
p: positive
iota_T a (N.succ (Pos.pred_N p)) =
a :: iota_T (succN a) (Pos.pred_N p)
  destruct (N.succ (Pos.pred_N p)) as [|p0] eqn:EQ; first by move: (N.neq_succ_0 (Pos.pred_N p)).
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
iota_T a (N.pos p0) =
a :: iota_T (succN a) (Pos.pred_N p)
  move: (posBinNatNotZero p0) => /eqP EQn0.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
EQn0: N.pos p0 != 0
iota_T a (N.pos p0) =
a :: iota_T (succN a) (Pos.pred_N p)
  destruct (nat_of_bin (N.pos p0)) as [|n] eqn:EQn; first by done.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
n: nat
EQn: N.pos p0 = n.+1
EQn0: n.+1 != 0
iota_T a n.+1 = a :: iota_T (succN a) (Pos.pred_N p)
  have -> : n = Pos.pred_N p; last by rewrite //= /succN /add_N /add_op N.add_comm.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
n: nat
EQn: N.pos p0 = n.+1
EQn0: n.+1 != 0
n = Pos.pred_N p
  apply /eqP.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
n: nat
EQn: N.pos p0 = n.+1
EQn0: n.+1 != 0
n == Pos.pred_N p
  rewrite -eqSS -EQn -EQ -addn1.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
n: nat
EQn: N.pos p0 = n.+1
EQn0: n.+1 != 0
N.succ (Pos.pred_N p) == Pos.pred_N p + 1
  move: (nat_of_add_bin (Pos.pred_N p) 1%N) => EQadd1; rewrite -EQadd1.
a: N
p, p0: positive
EQ: N.succ (Pos.pred_N p) = N.pos p0
n: nat
EQn: N.pos p0 = n.+1
EQn0: n.+1 != 0
EQadd1: (Pos.pred_N p + 1)%N = Pos.pred_N p + 1%N
N.succ (Pos.pred_N p) == (Pos.pred_N p + 1)%N
  by rewrite N.add_1_r.
Qed.

(** Next, we prove a refinement for the [iota] function. *)
Global Instance refine_iota :
  refines (Rnat ==> Rnat ==> list_R Rnat)%rel iota iota_T.
refines (Rnat ==> Rnat ==> list_R Rnat) iota
  (fun a b : N => iota_T a b)
Proof.
refines (Rnat ==> Rnat ==> list_R Rnat) iota
  (fun a b : N => iota_T a b)
  rewrite refinesE => a a' Ra b; move: a a' Ra; elim: b => [|b IHb] a a' Ra b' Rb.
a: nat
a': N
Ra: Rnat a a'
b': N
Rb: Rnat 0 b'
list_R Rnat (iota a 0) (iota_T a' b')
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
b': N
Rb: Rnat b.+1 b'
list_R Rnat (iota a b.+1) (iota_T a' b')
  {
a: nat
a': N
Ra: Rnat a a'
b': N
Rb: Rnat 0 b'
list_R Rnat (iota a 0) (iota_T a' b') destruct b'; first  by rewrite //=; apply list_R_nil_R.
a: nat
a': N
Ra: Rnat a a'
p: positive
Rb: Rnat 0 (N.pos p)
list_R Rnat (iota a 0) (iota_T a' (N.pos p))
    by compute in Rb; apply posBinNatNotZero in Rb. }
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
b': N
Rb: Rnat b.+1 b'
list_R Rnat (iota a b.+1) (iota_T a' b')
  {
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
b': N
Rb: Rnat b.+1 b'
list_R Rnat (iota a b.+1) (iota_T a' b') destruct b'; first  by compute in Rb; destruct b.
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
list_R Rnat (iota a b.+1) (iota_T a' (N.pos p))
    have Rsa := Rnat_S.
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
Rsa: refines (Rnat ==> Rnat) succn succN
list_R Rnat (iota a b.+1) (iota_T a' (N.pos p))
    rewrite refinesE in Rsa; specialize (Rsa a a' Ra).
b: nat
IHb: forall (a : nat) (a' : N),
Rnat a a' -> forall y : N, Rnat b y -> list_R Rnat (iota a b) (iota_T a' y)
a: nat
a': N
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
Rsa: Rnat a.+1 (succN a')
list_R Rnat (iota a b.+1) (iota_T a' (N.pos p))
    specialize (IHb _ _ Rsa).
b, a: nat
a': N
IHb: forall y : N, Rnat b y -> list_R Rnat (iota a.+1 b) (iota_T (succN a') y)
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
Rsa: Rnat a.+1 (succN a')
list_R Rnat (iota a b.+1) (iota_T a' (N.pos p))
    rewrite //= -N.succ_pos_pred iotaTsuccN.
b, a: nat
a': N
IHb: forall y : N, Rnat b y -> list_R Rnat (iota a.+1 b) (iota_T (succN a') y)
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
Rsa: Rnat a.+1 (succN a')
list_R Rnat (a :: iota a.+1 b)
  (a' :: iota_T (succN a') (Pos.pred_N p))
    apply list_R_cons_R; first by done.
b, a: nat
a': N
IHb: forall y : N, Rnat b y -> list_R Rnat (iota a.+1 b) (iota_T (succN a') y)
Ra: Rnat a a'
p: positive
Rb: Rnat b.+1 (N.pos p)
Rsa: Rnat a.+1 (succN a')
list_R Rnat (iota a.+1 b)
  (iota_T (succN a') (Pos.pred_N p))
    apply IHb; clear Rsa Ra IHb.
b, a: nat
a': N
p: positive
Rb: Rnat b.+1 (N.pos p)
Rnat b (Pos.pred_N p)
    by apply eq_SnPos_to_nPred. }
Qed.

(** 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.
refines (list_R Rnat ==> Rnat ==> list_R Rnat)
  shift_points_pos shift_points_pos_T
Proof.
refines (list_R Rnat ==> Rnat ==> list_R Rnat)
  shift_points_pos shift_points_pos_T
  rewrite refinesE => xs xs' Rxs s s' Rs.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
list_R Rnat (shift_points_pos xs s)
  (shift_points_pos_T xs' s')
  unfold shift_points_pos, shift_points_pos_T.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
list_R Rnat [seq s + i | i <- xs]
  [seq (s' + x)%C | x <- xs']
  apply refinesP; eapply refine_map; first by rewrite refinesE; apply Rxs.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (Rnat ==> Rnat) (addn s) [eta +%C s']
  rewrite refinesE => ? ? ?.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
_x_: nat
_y_: N
_Hyp_: Rnat _x_ _y_
Rnat (s + _x_) (s' + _y_)%C
  by apply refinesP; tc.
Qed.

(** 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.
refines (list_R Rnat ==> Rnat ==> list_R Rnat)
  shift_points_neg shift_points_neg_T
Proof.
refines (list_R Rnat ==> Rnat ==> list_R Rnat)
  shift_points_neg shift_points_neg_T
  rewrite refinesE => xs xs' Rxs s s' Rs.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
list_R Rnat (shift_points_neg xs s)
  (shift_points_neg_T xs' s')
  unfold shift_points_neg, shift_points_neg_T.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
list_R Rnat [seq x - s | x <- xs & s <= x]
  [seq (x - s')%C | x <- xs' & (s' <= x)%C]
  apply refinesP; eapply refine_map.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (list_R ?rA) [seq x <- xs | s <= x]
  [seq x <- xs' | (s' <= x)%C]
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (?rA ==> Rnat) (subn^~ s) (sub_op^~ s')
  -
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (list_R ?rA) [seq x <- xs | s <= x]
  [seq x <- xs' | (s' <= x)%C] rewrite refinesE; eapply filter_R; last by eassumption.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
forall (t₁ : nat) (t₂ : N),
Rnat t₁ t₂ -> bool_R (s <= t₁) (s' <= t₂)%C
    by intros; apply refinesP; refines_apply.
  -
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (Rnat ==> Rnat) (subn^~ s) (sub_op^~ s') rewrite refinesE => x x' Rx.
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
x: nat
x': N
Rx: Rnat x x'
Rnat (x - s) (x' - s')%C
    by apply refinesP; refines_apply.
Qed.

(** 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 :
  forall xs,
    refines (list_R Rnat)%rel (map nat_of_bin xs) xs | 0.
forall xs : seq N,
refines (list_R Rnat) [seq i | i <- xs] xs
Proof.
forall xs : seq N,
refines (list_R Rnat) [seq i | i <- xs] xs
  elim=> [|a xs IHxs]; first by rewrite refinesE; simpl; apply list_R_nil_R.
a: N
xs: seq N
IHxs: refines (list_R Rnat) [seq i | i <- xs] xs
refines (list_R Rnat) [seq i | i <- a :: xs] (a :: xs)
  rewrite //= refinesE; rewrite refinesE in IHxs.
a: N
xs: seq N
IHxs: list_R Rnat [seq i | i <- xs] xs
list_R Rnat (a :: [seq i | i <- xs]) (a :: xs)
  by apply list_R_cons_R; last by done.
Qed.

(** ** 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.
refines
  ((Rnat ==> Rnat ==> Rnat) ==>
   Rnat ==> list_R Rnat ==> Rnat) foldr foldr
Proof.
refines
  ((Rnat ==> Rnat ==> Rnat) ==>
   Rnat ==> list_R Rnat ==> Rnat) foldr foldr
  rewrite refinesE => f f' Rf d d' Rd; elim=> [|x xs IHxs] xs' Rxs.
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
xs': seq N
Rxs: list_R Rnat [::] xs'
Rnat (foldr f d [::]) (foldr f' d' xs')
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
x: nat
xs: seq nat
IHxs: forall y : seq N,
list_R Rnat xs y ->
Rnat (foldr f d xs) (foldr f' d' y)
xs': seq N
Rxs: list_R Rnat (x :: xs) xs'
Rnat (foldr f d (x :: xs)) (foldr f' d' xs')
  {
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
xs': seq N
Rxs: list_R Rnat [::] xs'
Rnat (foldr f d [::]) (foldr f' d' xs') by destruct xs' as [ | x' xs']; [ done | inversion Rxs ]. }
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
x: nat
xs: seq nat
IHxs: forall y : seq N,
list_R Rnat xs y ->
Rnat (foldr f d xs) (foldr f' d' y)
xs': seq N
Rxs: list_R Rnat (x :: xs) xs'
Rnat (foldr f d (x :: xs)) (foldr f' d' xs')
  {
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
x: nat
xs: seq nat
IHxs: forall y : seq N,
list_R Rnat xs y ->
Rnat (foldr f d xs) (foldr f' d' y)
xs': seq N
Rxs: list_R Rnat (x :: xs) xs'
Rnat (foldr f d (x :: xs)) (foldr f' d' xs') destruct xs' as [ | x' xs']; first by inversion Rxs.
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
x: nat
xs: seq nat
IHxs: forall y : seq N,
list_R Rnat xs y ->
Rnat (foldr f d xs) (foldr f' d' y)
x': N
xs': seq N
Rxs: list_R Rnat (x :: xs) (x' :: xs')
Rnat (foldr f d (x :: xs)) (foldr f' d' (x' :: xs'))
    inversion Rxs; subst.
f: nat -> nat -> nat
f': N -> N -> N
Rf: (Rnat ==> Rnat ==> Rnat)%rel f f'
d: nat
d': N
Rd: Rnat d d'
x: nat
xs: seq nat
IHxs: forall y : seq N,
list_R Rnat xs y ->
Rnat (foldr f d xs) (foldr f' d' y)
x': N
xs': seq N
Rxs: list_R Rnat (x :: xs) (x' :: xs')
a_R: Rnat x x'
l_R: list_R Rnat xs xs'
Rnat (foldr f d (x :: xs)) (foldr f' d' (x' :: xs'))
    by simpl; apply Rf; [ done | apply IHxs]. }
Qed.

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:
    forall (R : T1 -> bool) (R' : T2 -> bool) (F : T1 -> nat) (F' : T2 -> N),
    forall (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']).
T1, T2: Type
xs: seq T1
xs': seq T2
forall (R : T1 -> bool) (R' : T2 -> bool)
  (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines (rT ==> bool_R) R R' ->
refines Rnat (\sum_(x <- xs | R x) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x'])
  Proof.
T1, T2: Type
xs: seq T1
xs': seq T2
forall (R : T1 -> bool) (R' : T2 -> bool)
  (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines (rT ==> bool_R) R R' ->
refines Rnat (\sum_(x <- xs | R x) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x'])
    move=> R R' F F' rT Rxs Rf Rr.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines Rnat (\sum_(x <- xs | R x) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x'])
    have ->: \sum_(x <- xs | R x) F x = foldr addn 0 [seq F x | x <- xs & R x].
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
\sum_(x <- xs | R x) F x =
foldr addn 0 [seq F x | x <- xs & R x]
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines Rnat (foldr addn 0 [seq F x | x <- xs & R x])
  (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x'])
    {
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
\sum_(x <- xs | R x) F x =
foldr addn 0 [seq F x | x <- xs & R x] by rewrite foldrE big_map big_filter. }
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines Rnat (foldr addn 0 [seq F x | x <- xs & R x])
  (foldr +%C 0%C [seq F' x' | x' <- xs' & R' x'])
    refines_apply.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R) map map
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0) filter
  filter
    Unshelve.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R) map map
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0) filter
  filter
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
seq nat -> seq N -> Type
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
seq T1 -> seq T2 -> Type
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr by rewrite refinesE=> b b' Rb z z' Rz l l' Rl; eapply foldr_R; eauto.
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat) map map by rewrite refinesE => g g' Rg l l' Rl; eapply map_R; eauto.
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)
  filter filter by rewrite refinesE => p p' Rp l l' Rl; eapply filter_R; eauto.
  Qed.

  (** Next, we prove a refinement for the [foldr] function when applied to a
      [map] operation. *)
  Lemma refine_uncond_foldr :
    forall (F : T1 -> nat) (F' : T2 -> N),
    forall (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']).
T1, T2: Type
xs: seq T1
xs': seq T2
forall (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines Rnat (\sum_(x <- xs) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs'])
  Proof.
T1, T2: Type
xs: seq T1
xs': seq T2
forall (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines Rnat (\sum_(x <- xs) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs'])
    move=> F F' rT Rxs Rf.
T1, T2: Type
xs: seq T1
xs': seq T2
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
refines Rnat (\sum_(x <- xs) F x)
  (foldr +%C 0%C [seq F' x' | x' <- xs'])
    have ->: \sum_(x <- xs) F x = foldr addn 0 [seq F x | x <- xs] by rewrite foldrE big_map.
T1, T2: Type
xs: seq T1
xs': seq T2
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
refines Rnat (foldr addn 0 [seq F x | x <- xs])
  (foldr +%C 0%C [seq F' x' | x' <- xs'])
    refines_apply.
T1, T2: Type
xs: seq T1
xs': seq T2
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
refines
  ((Rnat ==> Rnat ==> Rnat) ==>
   Rnat ==> list_R Rnat ==> Rnat) foldr foldr
    by apply refine_foldr_lemma.
  Qed.

  (** 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 :
    forall (R : T1 -> bool) (R' : T2 -> bool)
      (F : T1 -> nat) (F' : T2 -> N),
    forall (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']).
T1, T2: Type
xs: seq T1
xs': seq T2
forall (R : T1 -> bool) (R' : T2 -> bool)
  (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines (rT ==> bool_R) R R' ->
refines Rnat (\max_(x <- xs | R x) F x)
  (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x'])
  Proof.
T1, T2: Type
xs: seq T1
xs': seq T2
forall (R : T1 -> bool) (R' : T2 -> bool)
  (F : T1 -> nat) (F' : T2 -> N)
  (rT : T1 -> T2 -> Type),
refines (list_R rT) xs xs' ->
refines (rT ==> Rnat) F F' ->
refines (rT ==> bool_R) R R' ->
refines Rnat (\max_(x <- xs | R x) F x)
  (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x'])
    move=> R R' F F' rT Rxs Rf Rr.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines Rnat (\max_(x <- xs | R x) F x)
  (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x'])
    have ->: \max_(x <- xs | R x) F x = foldr maxn 0 [seq F x | x <- xs & R x]
                                         by rewrite foldrE big_map big_filter.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines Rnat (foldr maxn 0 [seq F x | x <- xs & R x])
  (foldr maxn_T 0%C [seq F' x' | x' <- xs' & R' x'])
    refines_apply.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R) map map
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0) filter
  filter
    Unshelve.
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R) map map
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0) filter
  filter
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
seq nat -> seq N -> Type
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
seq T1 -> seq T2 -> Type
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines
  ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)
  foldr foldr by rewrite refinesE=> b b' Rb z z' Rz l l' Rl; eapply foldr_R; eauto.
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat) map map by rewrite refinesE => g g' Rg l l' Rl; eapply map_R; eauto.
    -
T1, T2: Type
xs: seq T1
xs': seq T2
R: T1 -> bool
R': T2 -> bool
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat) F F'
Rr: refines (rT ==> bool_R) R R'
refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)
  filter filter by rewrite refinesE => p p' Rp l l' Rl; eapply filter_R; eauto.
  Qed.

End GenericLists.