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