Hi.

First time posting but after some extensive googling and reading I’m still not quite sure how I should go about proving that a function that I’m writing is a well-founded relation for a non-trivial recursion. I am using the Program module in order to get the proof obligations in order to prove to Coq that my function will terminate but I’ve having difficulty understanding the proof structure needed. Here is the program that I have now:

```
Require Import Nat String List.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.
Open Scope list_scope.
Open Scope string_scope.
Inductive row :=
| EmptyRow : row
| DataRow : list string -> row
.
Inductive section : Type :=
| Section : list row -> section
.
Fixpoint get_section rows :=
match rows with
| nil => (nil, nil)
| EmptyRow :: rs => (nil, rs)
| DataRow r :: rs =>
let (sect, rst) := get_section rs in
((DataRow r :: sect), rst)
end.
Program Fixpoint get_sections (rows : list row) {measure (length rows) } : list section :=
match rows with
| nil => nil
| EmptyRow :: rs => get_sections rs
| DataRow r :: rs =>
let (rest_of_sect, rest) := get_section rs in
let sect := DataRow r :: rest_of_sect in
(Section sect) :: get_sections rest
end.
```

The example this program is implementing is this: Imagine a spreadsheet where you have several “sections” composed of several rows of non-empty data. To illustrate, here is the test file I am working with:

```
Doc,Citation
val11,val12,
val21,val22,
,,
Type,Field,Size
val13,val14,val15
val23,val24,val25
```

This file is composed of two “sections”, each with a header row and subsequent data rows. The above fixpoint function is passed in this CSV data in a typed format so the `get_sections`

function will be fed this list:

```
[
DataRow ["Doc"; "Citation"];
DataRow ["val11"; "val12"];
DataRow ["val21"; "val22"];
EmptyRow;
DataRow ["Type"; "Field"; "Size"];
DataRow ["val13"; "val14"; "val15"];
DataRow ["val23"; "val24"; "val25"];
]
```

The goal of the `get_sections`

functions is to convert this list of type row to a list of type section, or more concretely:

```
[
Section [
DataRow ["Doc"; "Citation"];
DataRow ["val11"; "val12"];
DataRow ["val21"; "val22"];
];
Section [
DataRow ["Type"; "Field"; "Size"];
DataRow ["val13"; "val14"; "val15"];
DataRow ["val23"; "val24"; "val25"];
]
]
```

The way I previous had written this function had used a gas parameter, which of course worked, but I am interested in learning how to prove to Coq that the relation is well-founded and will be guaranteed to terminate over any finite list of rows. Running the current version of the program posted above generates the following obligations:

```
1 subgoal
r : list string
rs : list row
get_sections : forall rows : list row,
Datatypes.length rows < Datatypes.length (DataRow r :: rs) ->
list section
rest_of_sect, rest : list row
============================
Datatypes.length rest < Datatypes.length (DataRow r :: rs)
```

I’m still fairly new to this side of Coq development but my understanding of this is that I have to prove to Coq that `rest`

is strictly less than `rows`

. This is obviously true as `rest`

is just a sublist of rows as seen with `let (rest_of_sect, rest) := get_section rs in ...`

where `get_section`

is well-founded relation.

My question: What do I have to do to show Coq that? I’m not clear how this proof would actually proceed in order to demonstrate the well-foundedness of the `get_sections`

relation.