Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
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. *)

refines (unify (A:=N) ==> Rnat)%rel nat_of_bin id

refines (unify (A:=N) ==> Rnat)%rel nat_of_bin id
n, n': N
Rn: refines (unify (A:=N)) n n'

refines Rnat n n'
n': N

refines Rnat n' n'
by apply trivial_refines. Qed. (** Second, we prove a refinement for the predecessor function. *)

refines (Rnat ==> Rnat)%rel predn predn_T

refines (Rnat ==> Rnat)%rel predn predn_T
a: nat
a': N
Ra: Rnat a a'

Rnat a.-1 (predn_T a')
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. *)

refines (Rnat ==> Rnat ==> bool_R)%rel dvdn dvdn_T

refines (Rnat ==> Rnat ==> bool_R)%rel dvdn dvdn_T
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. *)

refines (Rnat ==> Rnat ==> Rnat)%rel div_ceil div_ceil_T

refines (Rnat ==> Rnat ==> Rnat)%rel 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)
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)
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'
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')
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)
x: nat
x': N
Rx: refines Rnat x x'
y: nat
y': N
Ry: refines Rnat y y'
B: (y %| x) = true

refines Rnat (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 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) = true

refines Rnat (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) = true

refines (?R ==> Rnat)%rel (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) = true
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) = true

refines Rnat y y'
by 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
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)%rel 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 Rnat (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)%rel (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 Rnat y y'
by exact Ry. } Qed. (** Next, we prove a refinement for the minimum function. *)

refines (Rnat ==> Rnat ==> Rnat)%rel minn minn_T

refines (Rnat ==> Rnat ==> Rnat)%rel 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')
a', b': N

Rnat (if a' < b' then a' else b') (if (a' < b')%C then a' else b')
a, b: N

Rnat (if a < b then a else b) (if (a < b)%C then a else b)
a, b: N

(a < b) = (a < b)%C
a, b: N

(a < b) = (a <? b)%N
a, b: N
EQ: (a < b) = false

(a <? b)%N = false
a, b: N
EQ: (a < b) = false

(b <= a)%N
a, b: N
EQ: b <= a

(b <= a)%N
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. *)

refines (Rnat ==> Rnat ==> Rnat)%rel maxn maxn_T

refines (Rnat ==> Rnat ==> Rnat)%rel 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')
a', b': N

Rnat (if a' < b' then b' else a') (if (a' < b')%C then b' else a')
a, b: N

Rnat (if a < b then b else a) (if (a < b)%C then b else a)
a, b: N

(a < b) = (a < b)%C
a, b: N

(a < b) = (a <? b)%N
a, b: N
EQ: (a < b) = false

(a <? b)%N = false
a, b: N
EQ: (a < b) = false

(b <= a)%N
a, b: N
EQ: b <= a

(b <= a)%N
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]. *)

forall p : positive, N.pos p <> 0

forall p : positive, N.pos p <> 0

forall p : positive, N.pos p <> bin_of_nat 0
p: positive
EQ: N.pos p = bin_of_nat 0

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

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
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
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]. *)

forall (b : nat) (p : positive), 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)
b: nat
p: positive

Rnat b.+1 (N.pos p) -> Rnat b (Pos.pred_N p)
b: nat
p: positive
EQ: N.pos p = b.+1

Pos.pred_N p = b
b: nat
p: positive
EQ: N.pos p = b + 1

Pos.pred_N p = b
b: nat
p: positive
EQ: N.pos p = b + 1

Pos.pred_N p + 1 = N.pos p
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']. *)

forall (a : nat) (a' : N) (b : nat) (b' : N), 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
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'

bool_R (a < b) (a' < b')%C
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'

((1 + a')%N <= b')%C = (a' < b')%C
a: nat
a': N
b: nat
b': N
Ra: Rnat a a'
Rb: Rnat b b'

(1 + a' <=? b')%N = (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
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
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 = 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 = 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 = 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. *)

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)%rel F F' -> refines (list_R rB) [seq F i | i <- xs] [seq F' i | i <- 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)%rel F F' -> refines (list_R rB) [seq F i | i <- xs] [seq F' i | i <- 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)%rel F F'

list_R rB [seq F i | i <- xs] [seq F' i | i <- 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)%rel 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)%rel F F'
forall (H : A) (H0 : A'), ?T1_R H H0 -> rB (F H) (F' H0)
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)%rel 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)%rel F F'
forall (H : A) (H0 : A'), ?T1_R H H0 -> rB (F H) (F' H0)
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)%rel F F'

forall (H : A) (H0 : A'), rA H H0 -> rB (F H) (F' H0)
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)%rel F F'

forall (H : A) (H0 : A'), rA H H0 -> rB (F H) (F' H0)
by intros x x' Rx; rewrite refinesE in RF; apply RF. Qed. (** Second, we prove a refinement for the [zip] function. *)

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))%rel zip zip
by rewrite refinesE => xs xs' Rxs ys ys' Rys; apply zip_R. Qed. (** Next, we prove a refinement for the [all] function. *)

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)%rel all all
A, A': Type
rA: A -> A' -> Type

refines ((rA ==> bool_R) ==> list_R rA ==> bool_R)%rel all all
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')
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 (H : A) (H0 : A'), rA H H0 -> bool_R (P H) (P' H0)
by intros x x' Rx; apply RP. Qed. (** Next, we prove a refinement for the [flatten] function. *)

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)%rel flatten flatten
by intros; rewrite refinesE => xss xss' Rxss; eapply flatten_R. Qed. (** Next, we prove a refinement for the [cons] function. *)
A, C: Type
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)%rel 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. *)
A, C: Type
rAC: A -> C -> Type

refines (list_R rAC) [::] [::]
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. *)

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)%rel last last
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')
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')
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
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
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
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'))
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
Rab: rA a b
Rxs: list_R rA xs xs'

rA (last d (a :: xs)) (last d' (b :: xs'))
by simpl; apply IHxs. Qed. (** Next, we prove a refinement for the [size] function. *)
A, C: Type
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)%rel size size_T
A, C: Type
rAC: A -> C -> Type
h: seq A

forall y : seq C, list_R rAC h y -> Rnat (size h) (size_T y)
A, C: Type
rAC: A -> C -> Type
a: A
h: seq A
IHh: forall y : seq C, list_R rAC h y -> Rnat (size h) (size_T y)
h': seq C
Rh: list_R rAC (a :: h) h'

Rnat (size (a :: h)) (size_T h')
A, C: Type
rAC: A -> C -> Type
a: A
h: seq A
IHh: forall y : seq C, list_R rAC h y -> Rnat (size h) (size_T y)
c: C
h': seq C
Rh: list_R rAC (a :: h) (c :: h')

Rnat (size (a :: h)) (size_T (c :: h'))
A, C: Type
rAC: A -> C -> Type
a: A
h: seq A
IHh: forall y : seq C, list_R rAC h y -> Rnat (size h) (size_T y)
c: C
h': seq C
X1: rAC a c
X4: list_R rAC h h'

Rnat (size (a :: h)) (size_T (c :: h'))
A, C: Type
rAC: A -> C -> Type
a: A
h: seq A
c: C
h': seq C
X1: rAC a c
X4: Rnat (size h) (size_T h')

Rnat (size h).+1 (1 + size_T h')%C
by have H := Rnat_S; rewrite refinesE in H; specialize (H _ _ X4). Qed. (** Next, we prove a refinement for the [iota] function when applied to the successor of a number. *)

forall (a : N) (p : positive), 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)
a: N
p: positive

iota_T a (N.succ (Pos.pred_N p)) = a :: iota_T (succN a) (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)
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)
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)
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
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
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
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. *)

refines (Rnat ==> Rnat ==> list_R Rnat)%rel iota (fun a b : N => iota_T a b)

refines (Rnat ==> Rnat ==> list_R Rnat)%rel iota (fun a b : N => 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')
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')
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')
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))
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)%rel succn succN

list_R Rnat (iota a b.+1) (iota_T a' (N.pos p))
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))
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))
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))
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))
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. *)

refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel shift_points_pos shift_points_pos_T

refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel 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 (shift_points_pos xs s) (shift_points_pos_T xs' s')
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']
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'

refines (Rnat ==> Rnat)%rel (addn s) [eta +%C s']
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. *)

refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel shift_points_neg shift_points_neg_T

refines (list_R Rnat ==> Rnat ==> list_R Rnat)%rel 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 (shift_points_neg xs s) (shift_points_neg_T xs' s')
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]
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)%rel (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]
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (?rA ==> Rnat)%rel (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'

forall (H : nat) (H0 : N), Rnat H H0 -> bool_R (s <= H) (s' <= H0)%C
xs: seq nat
xs': seq N
Rxs: list_R Rnat xs xs'
s: nat
s': N
Rs: Rnat s s'
refines (Rnat ==> Rnat)%rel (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 (Rnat ==> Rnat)%rel (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 (Rnat ==> Rnat)%rel (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'
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. *)

forall xs : seq N, refines (list_R Rnat) [seq i | i <- xs] xs

forall xs : seq N, refines (list_R Rnat) [seq i | i <- xs] xs
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)
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. *)

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> list_R Rnat ==> Rnat)%rel foldr foldr

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> list_R Rnat ==> Rnat)%rel foldr foldr
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')
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'))
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')
X: Rnat x x'
X0: 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. *)
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)%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)%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
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)%rel F F'
Rr: 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
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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)%rel 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. *)
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)%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)%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
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: 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
F: T1 -> nat
F': T2 -> N
rT: T1 -> T2 -> Type
Rxs: refines (list_R rT) xs xs'
Rf: refines (rT ==> Rnat)%rel F F'

refines Rnat (foldr addn 0 [seq F x | x <- xs]) (foldr +%C 0%C [seq F' x' | x' <- xs'])
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)%rel F F'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> list_R Rnat ==> Rnat)%rel 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. *)
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)%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)%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
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)%rel F F'
Rr: 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
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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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'])
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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((Rnat ==> Rnat ==> Rnat) ==> Rnat ==> ?R ==> Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> Rnat) ==> ?R0 ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R0)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> Rnat) ==> ?R ==> list_R Rnat)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'
refines ((rT ==> bool_R) ==> list_R rT ==> ?R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)%rel 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)%rel F F'
Rr: refines (rT ==> bool_R)%rel R R'

refines ((rT ==> bool_R) ==> list_R rT ==> list_R rT)%rel filter filter
by rewrite refinesE => p p' Rp l l' Rl; eapply filter_R; eauto. Qed. End GenericLists.