Stream: Coq users

Topic: ✔ Extracting Inductives


view this post on Zulip 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! :)

view this post on Zulip 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

view this post on Zulip 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