Stream: Coq users

Topic: Mutual recursion function in type


view this post on Zulip Julin S (Jun 13 2022 at 06:22):

Can we not use one of the mutually recursive functions as part of the type?

I tried:

Fixpoint iseven (n:nat) : Prop :=
  let hrv := helper n in (* Just to use helper *)
  match n with
  | O => True
  | S n' => isodd n'
  end
with isodd (n:nat) : Prop :=
  let hrv := helper n in (* Just to use helper *)
  match n with
  | O => False
  | S n' => iseven n'
  end
with helper (n:nat) : {iseven n} + {isodd n}.

got error as:

The reference iseven was not found in the current environment.

But a version without occurrence of one of those functions in the type worked:

Fixpoint iseven (n:nat) : Prop :=
  let hrv := helper n in (* Just to use helper *)
  match n with
  | O => True
  | S n' => isodd n'
  end
with isodd (n:nat) : Prop :=
  let hrv := helper n in (* Just to use helper *)
  match n with
  | O => False
  | S n' => iseven n'
  end
with helper (n:nat) : Prop :=
  let e := iseven n in     (* Just to use iseven *)
  let o := isodd n in       (* Just to use isodd *)
  False.

Is there a way around this?

view this post on Zulip Kenji Maillard (Jun 13 2022 at 07:56):

I don't think there is currently a way to write exactly this kind of "recursion-recursion" in Coq, but you can often encode it with a dependent sum.
For instance in your setting you could write a single function

Fixpoint iseven_isodd_helper (n : nat) : { iseven : Prop & { isodd : Prop & { iseven } + {isodd} } := ...

Definition iseven (n : nat) : Prop := proj_sigT1 (iseven_isodd_helper n).
Definition isodd (n : nat) : Prop := proj_sigT1 (proj_sigT2 (iseven_isodd_helper n)).
Definition helper (n : nat) : {iseven n} + {isodd n} := proj_sigT2 (proj_sigT2 (iseven_isodd_helper n)).

view this post on Zulip Julin S (Jun 13 2022 at 09:00):

Which module is needed to have proj_sigT1?

Has it got something to do with sigT?

view this post on Zulip Julin S (Jun 13 2022 at 09:06):

And is the & same as the one in sigT?

Inductive sigT (A : Type) (P : A -> Type) : Type :=
    existT : forall x : A, P x -> {x : A & P x}

Locate "{_ & _}". didn't show anything.

view this post on Zulip Gaëtan Gilbert (Jun 13 2022 at 09:16):

Locate "{ _ & _ }". with spaces

view this post on Zulip Gaëtan Gilbert (Jun 13 2022 at 09:17):

Julin S said:

Which module is needed to have proj_sigT1?

Has it got something to do with sigT?

they probably meant projT1


Last updated: Feb 04 2023 at 21:02 UTC