CODEWITHSUNDEEP
coq
FH35
FH35

Reputation: 97

Another question about how to make Coq accept a Fixpoint definition

I have trees :

Inductive tree : Set :=
  | Node : list tree -> tree.

and a collection of Definitions I'd like to use, all with a structure of the form :

Fixpoint getThemAll_aux (trees: list tree) (maxIter:nat): list tree :=
 
  match maxIter with
   | O => nil
   | S n => 
       match trees with
             | nil => nil
             | xx::rest =>  let newCandidates := generateCandidates xx in
                                  let newRest := addAllIfDifferent tree eq_tree newCandidates rest in 
                                     addAllIfDifferent tree eq_tree newCandidates (getThemAll_aux newRest n)
       end
    end.

Definition getThemAll (seed:tree) : list tree :=
    getThemAll_aux (seed::nil) 999.

Because of maxIter , this function is accepted whatever we have for generateCandidates of type tree -> list tree, eq_tree and addAllIfDifferent.

Now suppose that I have a proof that generateCandidates produces lists of trees with the same number of Nodes as the argument, and that eq_tree and addAllIfDifferent have the expected semantics.

Is that case, the function always terminates.

Is there then a way to get rid of the maxIter parameter, in the definition of the Fixpoint ?

Upvotes: 1

Views: 73

Answers (1)

Lolo
Lolo

Reputation: 649

The main problem of your definition is this 999. If you are sure your function terminates, maybe you are capable to write a function f that bounds the number of iterations you need. so you can define

 Definition getThemAll (seed:tree) : list tree :=
    getThemAll_aux (seed::nil) (f seed).

and prove the theorem

forall trees,
getThemAll trees = 
       match trees with
             | nil => nil
             | xx::rest =>  let newCandidates := generateCandidates xx in
                                  let newRest := addAllIfDifferent tree eq_tree newCandidates rest in 
                                     addAllIfDifferent tree eq_tree newCandidates (getThemAll newRest)
       end.

Upvotes: 1

Related Questions