Proving well-founded recursion using the Program module

Using Coq
1

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.

2

You got that right. More precisely, you have to prove that rest as given by get_section is less than rows. And your goal is missing that piece of information. The issue here is that Program is full of heuristics to decide which information matters and it got it wrong on your example. If you rewrite your function as follows, then you will be able to prove it. (This version is strictly equivalent to yours, but the different syntax triggers different heuristics in Program.)

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 =>
    match get_section rs with
    | (rest_of_sect, rest) =>
      let sect := DataRow r :: rest_of_sect in
      (Section sect) :: get_sections rest
    end
  end.
3

That makes sense and has gotten me further in the context. Thank you for your help : )