CODEWITHSUNDEEP
coq
nobody
nobody

Reputation: 4264

Recursive function definition in coq with limit on set of possible inputs

I need to define a recursive function with no easily measurable argument. I keep a list of used arguments to ensure that each one is used at most once, and the input space is finite.

Using a measure (inpspacesize - (length l)) works mostly, but I get stuck in one case. It seems I'm missing the information that previous layers of l have been constructed correctly, i. e. there are no duplicates and all entries are really from the input space.

Now I'm searching for a list replacement that does what I need.

Edit I've reduced this to the following now:

I have nats smaller than a given max and need to ensure that the function is called at most once for every number. I've come up with the following:

(* the condition imposed *)
Inductive limited_unique_list (max : nat) : list nat -> Prop :=
  | LUNil  : limited_unique_list max nil
  | LUCons : forall x xs, limited_unique_list max xs
             -> x <= max
             -> ~ (In x xs)
             -> limited_unique_list max (x :: xs).

(* same as function *)
Fixpoint is_lulist (max : nat) (xs0 : list nat) : bool :=
  match xs0 with
  | nil     => true
  | (x::xs) => if (existsb (beq_nat x) xs) || negb (leb x max)
                 then false
                 else is_lulist max xs
  end.

(* really equivalent *)
Theorem is_lulist_iff_limited_unique_list : forall (max:nat) (xs0 : list nat),
    true = is_lulist max xs0 <-> limited_unique_list max xs0.
Proof. ... Qed.

(* used in the recursive function's step *)
Definition lucons {max : nat} (x : nat) (xs : list nat) : option (list nat) :=
  if is_lulist max (x::xs)
    then Some (x :: xs)
    else None.

(* equivalent to constructor *)
Theorem lucons_iff_LUCons : forall max x xs, limited_unique_list max xs ->
    (@lucons max x xs = Some (x :: xs) <-> limited_unique_list max (x::xs)).
Proof. ... Qed.

(* unfolding one step *)
Theorem lucons_step : forall max x xs v, @lucons max x xs = v ->
  (v = Some (x :: xs) /\ x <= max /\ ~ (In x xs)) \/ (v = None).
Proof. ... Qed.

(* upper limit *)
Theorem lucons_toobig : forall max x xs, max < x
    -> ~ limited_unique_list max (x::xs).
Proof. ... Qed.

(* for induction: increasing max is ok *)
Theorem limited_unique_list_increasemax : forall max xs,
  limited_unique_list max xs -> limited_unique_list (S max) xs.
Proof. ... Qed.

I keep getting stuck when trying to prove inductively that I cannot insert an element into the full list (either the IH comes out unusable or I can't find the information I need). As I think this non-insertability is crucial for showing termination, I've still not found a working solution.

Any suggestions on how to prove this differently, or on restructuring the above?

Upvotes: 1

Views: 571

Answers (1)

akoprowski
akoprowski

Reputation: 3315

Hard to say much without more details (please elaborate!), but:

  • Are you using the Program command? It's certainly very helpful for defining functions with non-trivial measures.
  • For uniqueness wouldn't it work if you tried sets? I remember writing ones a function that sounds very much like what you are saying: I had a function for which an argument contained a set of items. This set of items was growing monotonously and was limited to a finite space of items, giving the termination argument.

Upvotes: 1

Related Questions