1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
Require Import List.
Require Import Arith.
Require Import Recdef.
Require Import Lia.
Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
match xys with
| (nil, _) => snd xys
| (_, nil) => fst xys
| (x :: xs', y :: ys') => match Nat.compare x y with
| Lt => x :: foo (xs', y :: ys')
| Eq => x :: foo (xs', ys')
| Gt => y :: foo (x :: xs', ys')
end
end.
Proof.
all: simpl; lia.
Qed.
Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
let (xs, ys) := xys in
match (xs, ys) with
| (nil, _) => ys
| (_, nil) => xs
| (x :: xs', y :: ys') => match Nat.compare x y with
| Lt => x :: foo (xs', ys)
| Eq => x :: foo (xs', ys')
| Gt => y :: foo (xs, ys')
end
end.
Proof.
Defined.
|
