coq + inlining + "merge right"

[gds]

Некоторые люди прочитали статью http://alaska-kamtchatka.blogspot.com/2012/08/merge-right.html , где была показана весьма общая функция для слияния/пересечения/разницы списков.
А господин ygrek в камлочятике прилюдно мучил MetaOCaml для инлайнинга функций-аргументов merge. Я не мог на это смотреть спокойно. Однако и сразу разобраться не смог, так как не знал многого, но вполне так узнал.
Чтобы было хоть сколько-нибудь интересно читать, рекомендую прочитать сначала исходную статью.
Потому что сейчас будет простыня.


Require Import List.
Require Import Wf.
Require Import Wf_nat.
Require Import Omega.

Definition nat_lt := lt.

Inductive cmp_res :=
| Lt
| Eq
| Gt
.

Definition merge : forall
{A : Type}
(cmp : A -> A -> cmp_res)
(ln rn : list A -> list A)
(lt eq gt : A -> list A -> list A)
(l r : list A),
list A.
refine
(fun {A} cmp ln rn lt eq gt l r =>
(fix go l r (H : Acc nat_lt (length l + length r)) {struct H} :=
match H with
| Acc_intro H1 =>
match l as l1, r as r1
return l = l1 -> r = r1 -> list A
with
| nil, _ => fun _Leq _Req => ln r
| _, nil => fun _Leq _Req => rn l
| cons x xs, cons y ys =>
fun Leq Req =>
match cmp x y with
| Lt => lt x (go xs (y :: ys) (H1 _ _))
| Eq => eq x (go xs ys (H1 _ _))
| Gt => gt y (go (x :: xs) ys (H1 _ _))
end
end
(eq_refl l)
(eq_refl r)
end
)
l r
(Acc_intro _ _)
);
intros;
try rewrite Leq;
try rewrite Req;
simpl;
unfold nat_lt;
try omega;
try apply lt_wf.
Defined.

Definition self {A} (xs : list A) : list A := xs .
Definition null {A} (_ : list A) : list A := nil.
Definition cons {A} (x : A) (xs : list A) : list A := x :: xs.
Definition tail {A} (_ : A) (xs : list A) : list A := xs.

Extraction Inline merge self null cons tail.

Definition union {A} cmp (l : list A) r :=
merge cmp self self cons cons cons l r.
Definition inter {A} cmp (l : list A) r :=
merge cmp null null tail cons tail l r.
Definition diff {A} cmp (l : list A) r :=
merge cmp null self cons tail tail l r.

Extraction Inline union inter diff.

Axiom int' : Type.
Extract Constant int' => "int".
Definition int := int'.

Axiom cmp_int : int -> int -> cmp_res.
Extract Inlined Constant cmp_int =>
"(fun (a : int) b -> if a < b then Lt else if a = b then Eq else Gt)".

Definition union_int := @union int cmp_int.

Require Import ExtrOcamlBasic.

Extraction union_int.

-----

(** val union_int : int list -> int list -> int list **)

let rec union_int l0 r0 =
match l0 with
| [] -> r0
| x :: xs ->
(match r0 with
| [] -> l0
| y :: ys ->
(match (fun (a : int) b -> if a < b then Lt else if a = b then Eq else Gt)
x y with
| Lt -> x :: (union_int xs (y :: ys))
| Eq -> x :: (union_int xs ys)
| Gt -> y :: (union_int (x :: xs) ys)))

Вроде ЗБС.
Можно было бы сравнение не инлайнить, но избавиться от вызова функции (будь то "(fun (a : int) b -> ...)", будь то Pervasives.compare) не получается сходу.
Мне Coq нужен не только для зависимых типов и доказательств кода, но и для инлайнинга. Я -- практичная скотина, да!
Если будут вопросы -- поясню. Потому что всё сразу пояснять -- руки устанут.