## Stream: Coq users

### Topic: ✔ Extracting Inductives

#### Matthis Kruse (Jun 26 2023 at 14:27):

Hey, so I've been wondering what the current solution to "I want to extract an `Inductive` relation" is.
To describe my question further, is there an automated way to turn this:

``````Inductive is_fib : nat -> nat -> Prop :=
| fib0 : is_fib 0 0
| fib1 : is_fib 1 1
| fibN : forall n m0 m1, is_fib n m0 -> is_fib (S n) m1 -> is_fib (S(S n)) (m0 + m1)
.
``````

into this, either by means of extracting to e.g. Ocaml or perform some transformation within Coq:

``````Fixpoint is_fib' (n : nat) {struct n} :=
match n with
| 0 => 0
| S n' => match n' with
| 0 => 1
| S n'' => is_fib' n'' + is_fib' n'
end
end
.
Lemma sound_is_fib' n m :
is_fib' n = m -> is_fib n m.
Proof.
(* ... *)
Qed.
``````

Thanks in advance! :)

#### Karl Palmskog (Jun 26 2023 at 14:29):

plenty of work in the literature in this direction, most recent I know: https://dl.acm.org/doi/abs/10.1145/3519939.3523707

#### Notification Bot (Jun 26 2023 at 14:35):

Matthis Kruse has marked this topic as resolved.

Last updated: Jun 22 2024 at 15:01 UTC