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! :)

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

Matthis Kruse has marked this topic as resolved.

Last updated: Jun 22 2024 at 15:01 UTC