Julin S (Jun 13 2022 at 06:22): 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?
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)).
Which module is needed to have proj_sigT1?
Has it got something to do with sigT?
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.
Gaëtan Gilbert (Jun 13 2022 at 09:16):Locate "{ _ & _ }". with spaces
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: Oct 01 2023 at 19:01 UTC