Databases
StackOverflow2013
Postsdbo
POHow to get an induction principle for nested fix
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POHow to get an induction principle for nested fix
    primarykey
    data
    text
    <p>I am working with a function that searches through a range of values.</p> <pre><code>Require Import List. (* Implementation of ListTest omitted. *) Definition ListTest (l : list nat) := false. Definition SearchCountList n := (fix f i l := match i with | 0 =&gt; ListTest (rev l) | S i1 =&gt; (fix g j l1 := match j with | 0 =&gt; false | S j1 =&gt; if f i1 (j :: l1) then true else g j1 l1 end) (n + n) (i :: l) end) n nil . </code></pre> <p>I want to be able to reason about this function.</p> <p>However, I can't seem to get coq's built-in induction principle facilities to work.</p> <pre><code>Functional Scheme SearchCountList := Induction for SearchCountList Sort Prop. Error: GRec not handled </code></pre> <p>It looks like coq is set up for handling mutual recursion, not nested recursion. In this case, I have essentially 2 nested for loops.</p> <p>However, translating to mutual recursion isn't so easy either:</p> <pre><code>Definition SearchCountList_Loop := fix outer n i l {struct i} := match i with | 0 =&gt; ListTest (rev l) | S i1 =&gt; inner n i1 (n + n) (i :: l) end with inner n i j l {struct j} := match j with | 0 =&gt; false | S j1 =&gt; if outer n i (j :: l) then true else inner n i j1 l end for outer . </code></pre> <p>but that yields the error</p> <blockquote> <p>Recursive call to inner has principal argument equal to "<code>n + n</code>" instead of "<code>i1</code>".</p> </blockquote> <p>So, it looks like I would need to use measure to get it to accept the definition directly. It is confused that I reset j sometimes. But, in a nested set up, that makes sense, since i has decreased, and i is the outer loop.</p> <p>So, is there a standard way of handling nested recursion, as opposed to mutual recursion? Are there easier ways to reason about the cases, not involving making separate induction theorems? Since I haven't found a way to generate it automatically, I guess I'm stuck with writing the induction principle directly.</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. USAnton Trunov
    1. USscubed
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. This table or related slice is empty.
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload