Hello! I'm very new to Coq and I'm currently stuck on getting a function definition to unfold in the correct way. The function is:

```
Require Import List Arith.
Open Scope nat_scope.
Require Import Sorted.
Require Import Recdef.
Function bubble (l: list nat) {measure length} :=
match l with
| h1 :: h2 :: tl =>
if h1 <=? h2
then h1 :: (bubble (h2 :: tl))
else h2 :: (bubble (h1 :: tl))
| _ => l
end.
Proof.
- intros.
simpl.
apply Nat.lt_succ_diag_r.
- intros.
simpl.
apply Nat.lt_succ_diag_r.
Defined.
```

What I'm trying to figure out now is how to go from `bubble (h1 :: h2 :: tl)`

to ```
if h1 <=? h2 then
h1 :: (bubble (h2:: tl)) else h2 :: (bubble (h1 :: tl))
```

. I expected `unfold bubble`

to this, but instead it unfolds it to `(let (v, _) := bubble_terminate (x :: y :: l) in v)`

.

We recommend using Equations rather than the `Function`

package. Then, you get unfolding lemmas for free (do `Search my_defn_name.`

to see related lemmas after defining some function with `Equations`

)

Ah, this helped me find what I was looking for. Apparently the `Function`

package automatically defines `bubble_equation`

, which is the unfolding lemma I wanted. I will definitely look into `Equations`

though, thank you!

Eduardo Freire has marked this topic as resolved.

You have equation and induction lemmas defined automatically (for non dependently typed functions only). But indeed Function is getting old and Equations subsumes it almost every aspects.

Last updated: Oct 03 2023 at 02:34 UTC