Stream: Coq users

Topic: Proof mode def for mutual recursion

Julin S (Jun 12 2022 at 15:47):

I needed to define a function like:

Fixpoint zero (n:nat) : nat :=
  match n with
  | S (S n') => two n'
  | S n' => one n'
  | O => 0
  end
with one (n:nat) : nat :=
  match n with
  | S (S n') => zero n'
  | S n' => two n'
  | O => 1
  end
with two (n:nat) : nat :=
  match n with
  | S (S n') => one n'
  | S n' => zero n'
  | O => 2
  end.

Is it possible to do just one of these three definitions in proof mode?

As in:

Fixpoint zero (n:nat) : nat :=
  match n with
  | S (S n') => two n'
  | S n' => one n'
  | O => 0
  end.
with one (n:nat).  (* proof mode definition *)
with two (n:nat) : nat :=
  match n with
  | S (S n') => one n'
  | S n' => zero n'
  | O => 2
  end.

Or can't we mix usual definition and proof mode definitons?

Li-yao (Jun 12 2022 at 15:52):

You can define the body of one function as a function of the others:

Section One.
Context (zero two : nat -> nat).
Definition one_body (n : nat) : nat.
Proof.
...
Defined.
End One.

Fixpoint zero ...
with one := one_body zero two
with two ...

Julin S (Jun 12 2022 at 16:09):

Just out of curiosity, how can we define one here in proof mode?

I sort of blindly tried till:

Section mutrec.
  Context (zero two: nat -> bool).
  Definition one_body (n:nat) : bool.
  Proof.
    induction n.
    - exact true. (* n = 0 *)
    - destruct n. (* n = 1 *)
      *

Julin S (Jun 12 2022 at 16:34):

I finished that (probably incorrectly) and made this:

Section mutrec.
  Context (zero two: nat -> nat).
  Definition one_body (n:nat) : nat.
  Proof.
    induction n.
    - exact 0. (* n = 0 *)
    - destruct IHn. (* n = 1 *)
      * exact (two n).
      * exact (zero n).
  Defined.
End mutrec.

  Fixpoint zero (n:nat) : nat :=
    match n with
    | S (S n') => two n'
    | S n' => one n'
    | O => 0
    end
  with one (n:nat) := one_body zero two
  with two (n:nat) : nat :=
    match n with
    | S (S n') => one n'
    | S n' => zero n'
    | O => 2
    end.

but it says:

The term "one_body zero two" has type "nat -> nat"
while it is expected to have type "nat".

How can that be fixed?

Julin S (Jun 12 2022 at 16:36):

I get a different error if I remove the (n:nat) part of the definition of one.

A fixpoint needs at least one parameter

Julin S (Jun 12 2022 at 16:37):

And why is it one := one_body zero two? Why not just one (n:nat) := one_body n?

Pierre Castéran (Jun 12 2022 at 16:39):

Did you try with one (n:nat) := one_body zero two n ?

Julin S (Jun 12 2022 at 16:40):

That worked!

Julin S (Jun 12 2022 at 16:44):

My proof mode version of one isn't working though. Could anyone spot from where I went wrong?

Julin S (Jun 12 2022 at 16:45):

The term looks like:

one_body =
fun (zero two : nat -> nat) (n : nat) =>
nat_rec (fun _ : nat => nat) 0
  (fun n0 IHn : nat => match IHn with
                       | 0 => two n0
                       | S _ => zero n0
                       end) n
     : (nat -> nat) -> (nat -> nat) -> nat -> nat

Arguments one_body (_ _)%function_scope _%nat_scope

Julin S (Jun 12 2022 at 16:46):

After seeing the beginning of this term, I get why the one_body zero two n was needed.

Julin S (Jun 12 2022 at 16:49):

Okay, for starters, the exact 0. should've been exact 1..

Pierre Castéran (Jun 12 2022 at 17:14):

Here is an interactive definition of one_body.

  Definition one_body (n:nat) : nat.
  Proof.
    induction n as [|p recp].
    - exact 1. (* n = 0 *)
    - destruct p as [| q].
      * exact (two 0).
      * exact (zero q).
  Defined.

But I don't think it is as readable (assuming it is correct!) as the direct one.
I think that interactive definitions are OK if the considered type is informative enough (e.g with sumbool, sumor, sig, etc. ) to make you sure that you obtain interactively the "good" function you want to define. Otherwise, you have to look carefully at the proof script and verify it's OK.

Gaëtan Gilbert (Jun 12 2022 at 17:59):

Julin S said:

I needed to define a function like:

Fixpoint zero (n:nat) : nat :=
  match n with
  | S (S n') => two n'
  | S n' => one n'
  | O => 0
  end
with one (n:nat) : nat :=
  match n with
  | S (S n') => zero n'
  | S n' => two n'
  | O => 1
  end
with two (n:nat) : nat :=
  match n with
  | S (S n') => one n'
  | S n' => zero n'
  | O => 2
  end.

Is it possible to do just one of these three definitions in proof mode?

As in:

Fixpoint zero (n:nat) : nat :=
  match n with
  | S (S n') => two n'
  | S n' => one n'
  | O => 0
  end.
with one (n:nat).  (* proof mode definition *)
with two (n:nat) : nat :=
  match n with
  | S (S n') => one n'
  | S n' => zero n'
  | O => 2
  end.

Or can't we mix usual definition and proof mode definitons?

you want

Fixpoint zero (n:nat) : nat :=
  match n with
  | S (S n') => two n'
  | S n' => one n'
  | O => 0
  end
with one (n:nat) : nat
with two (n:nat) : nat :=
  match n with
  | S (S n') => one n'
  | S n' => zero n'
  | O => 2
  end.
Proof. (* whtevr *) Defined.

(no . between one and two)

Julin S (Jun 12 2022 at 18:15):

Ah.. that was the way that I was looking for first.

But having the bodies defined separately feels nice. Probably because that's what I got to work first.

Julin S (Jun 13 2022 at 06:20):

<deleted>

(Posting as a new topic):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Mutual.20recursion.20function.20in.20type

Last updated: Feb 08 2023 at 23:03 UTC