Composing Propositions

Using Coq
1

Hello again,

Thanks to the help of this community I have been able to successfully get the Programs module to successfully pull in the necessary predicates in order to prove the well-foundedness of my fixpoint function. The version of the file I am currently dealing with is this:

Require Import Nat String List.
Require Import Row.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.

Open Scope list_scope.
Open Scope string_scope.

(*Duplicated for clarity - this inductive definition is in another module in the original*)
Inductive row : Type :=
  | Section : list row -> section
.

Inductive section : Type :=
  | Section : list row -> section
.

Program Fixpoint get_section (rows:list row) : (list row * list row) :=
  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.

Theorem succ_x_less_than_succ_succ_succ_x : forall (x : nat),
    S x < S (S (S x)).
Proof.
  intros. auto.
Defined.

Theorem succ_x_lt_succ_succ_x : forall (x:nat), S x < S (S x).
  Proof. auto. Defined.

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
    (*Section with just a header at the end of the sheet*)
    | (nil, nil) => Section (DataRow r :: nil) :: nil
    (*Section with just a header in the middle or beginning of sheet*)
    | (nil, rest) => (Section (DataRow r :: nil)) :: get_sections rest
    (*Section with datas*)
    | (rest_of_sect, rest) =>
      let sect := DataRow r :: rest_of_sect in
      (Section sect) :: get_sections rest
      end
  end.
Next Obligation.
  destruct rest.
  { apply PeanoNat.Nat.lt_0_succ. }
  { induction rs.
    { discriminate. }
    { simpl. destruct a.
      { simpl in Heq_anonymous. inversion Heq_anonymous. simpl.
        apply succ_x_less_than_succ_succ_succ_x. }
      { simpl in Heq_anonymous.

This function takes a list of rows (of a CSV) and converts them into a list of Sections, separated by blank rows. More visually:

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

to

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

As you can see at the end of the Coq module I have left the proof obligation unfinished as I have run into the following context with which I’m not sure how to proceed:

- rs : list row
- get_sections : forall rows : list row,                                                                                                                 
                 Datatypes.length rows < Datatypes.length (DataRow r :: DataRow l :: rs) -> list section
- r0 : row
- rest : list row
- H : (nil, nil) <> (nil, r0 :: rest)
- Heq_anonymous : (nil, r0 :: rest) = (let (sect, rst) := get_section rs in (DataRow l :: sect, rst))
- IHrs : (forall rows : list row, Datatypes.length rows < Datatypes.length (DataRow r :: rs) -> list section) ->                                         
         (nil, r0 :: rest) = get_section rs -> Datatypes.length (r0 :: rest) < Datatypes.length (DataRow r :: rs)
  ============================
  S (Datatypes.length rest) < S (S (Datatypes.length rs))

My understanding of how to solve this would suggest to me that I need to show that:

  • given a list of rows,
  • and a function that turns it into a list of sections,

with the inductive hypothesis on rs (IHrs) I can successfully construct a proof that solves the goal, modulo the inequalities the previous theorems were defined for. It would seem that I have all of this in my context as propositions that I would want to compose together but in my reading through the Coq documentation I’ve not come across something that looks like that yet. Is that what I need to do to solve this goal or am I fundamentally misunderstanding how to solve this goal? Can one compose propositions in Coq and if so, how?

2

am I fundamentally misunderstanding how to solve this goal?

You have the hypothesis

Heq_anonymous: (nil, r0 :: rest) = (let (sect, rst) := get_section rs in (DataRow l :: sect, rst))

Or put simply, nil = DataRow l :: sect, which is trivially absurd. Just to destruct (get_section rs) to exhibit it.

By the way, your induction hypothesis IHrs looks awful. You might want to clear get_sections before induction rs. Also, never use Program Fixpoint where Fixpoint is sufficient (e.g., get_section); it will make things simpler in the long run. Also, do not use Defined for theorems, unless you really understand what it means; use Qed instead. Finally, do Require Import Arith; it will bring into scope various lemmas about natural numbers and transitivity (which is what you meant by “composing propositions”, I guess).