CODEWITHSUNDEEP
recursioncoq
authchir
authchir

Reputation: 1635

Nested recursion with partial application

I am trying to define a nested recursive function over two parameters in Coq.

Require Import List.
Import ListNotations.

Fixpoint map_sequence2 {A B C : Set} (f : A -> B -> option C)
  (xs : list A) (ys : list B) : option (list C) :=
match xs, ys with
| [], [] => Some []
| x :: xs, y :: ys =>
  match f x y, map_sequence2 f xs ys with
  | Some z, Some zs => Some (z :: zs)
  | _, _ => None
  end
| _, _ => None
end.

Inductive T : Set := TA | TB : list T -> T.

Definition max n m := if Nat.leb n m then m else n.

Fixpoint height (t : T) : nat :=
match t with
| TA => 1
| TB xs => 1 + List.fold_left max (List.map height xs) 0
end.

Function bar (t1 : T) (t2 : T) {measure height t2} : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match map_sequence2 bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.
Proof.
Abort.

But I get the following error:

Error: No such section variable or assumption: bar.

The documentation of Function explicitly says:

Function does not support partial application of the function being defined.

But this is exactly my case. What is the the strategy for such cases?

Upvotes: 3

Views: 235

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

If you slightly redefine the map_sequence2 function (I just moved fix a bit to the right)

Definition map_sequence2 {A B C : Set} (f : A -> B -> option C) :=
  fix map_sequence2 (xs : list A) (ys : list B) : option (list C) :=
match xs, ys with
| [], [] => Some []
| x :: xs, y :: ys =>
  match f x y, map_sequence2 xs ys with
  | Some z, Some zs => Some (z :: zs)
  | _, _ => None
  end
| _, _ => None
end.

then the totality checker accepts your definition with just Fixpoint instead of Function or Program Fixpoint:

Fixpoint bar (t1 : T) (t2 : T) : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match map_sequence2 bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.

This solution is just like this one by @gallais. And if you Print fold_left. which is used in that solution, you'll see that it has been defined in the same style.

Let me add that this behavior of the totality checker is surprising for me. I stumbled upon this while trying to simplify your definition:

Section liftA2.
Variables A B C : Type.
Definition liftA2_option (f : A -> B -> C) : option A -> option B -> option C :=
  fun ox oy =>
    match ox, oy with
    | Some x, Some y => Some (f x y)
    | _, _ => None
    end.
End liftA2.
Arguments liftA2_option {A B C}.

Section Combine_with_option.
Variables A B C : Set.
Variable f : A -> B -> option C.

Fixpoint combine_with_option (xs : list A) (ys : list B) : option (list C) :=
  match xs,ys with
  | x::xs', y::ys' => liftA2_option cons (f x y) (combine_with_option xs' ys') 
  | [], [] => Some []
  | _, _ => None
  end.
End Combine_with_option.
Arguments combine_with_option {A B C}.

Fixpoint bar (t1 : T) (t2 : T) : option T :=
match t1, t2 with
| TA, TA => Some TA
| TB xs, TB ys =>
  match combine_with_option bar xs ys with
  | Some zs => Some (TB zs)
  | None => None
  end
| _, _ => None
end.

When one uses the section mechanism with Fixpoints one gets fix after the "shared" (unchanged) parameters.

Upvotes: 2

Related Questions