Nested recursion with partial application

Question

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?

Anton Trunov · Accepted Answer · 2017-10-21 19:29:20Z

2

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.

edited Oct 21, 2017 at 19:29

answered Oct 21, 2017 at 19:13

Anton Trunov

15.5k2 gold badges30 silver badges50 bronze badges

Sign up to request clarification or add additional context in comments.

2 Comments

authchir Over a year ago

Thanks, it works! Is there some literature to get to know the termination oracle better?

Anton Trunov Over a year ago

There is this description in the manual. And, perhaps, this Cocrico article might help.

Collectives™ on Stack Overflow

Nested recursion with partial application

1 Answer 1

2 Comments

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

2 Comments

Your Answer

Sign up or log in

Post as a guest

Linked

Related