Stream: Coq users

Topic: ✔ Correctly unfold function definition

Eduardo Freire (Aug 11 2022 at 16:18):

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).

Karl Palmskog (Aug 11 2022 at 16:58):

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)

Eduardo Freire (Aug 11 2022 at 17:26):

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!

Notification Bot (Aug 11 2022 at 17:27):

Eduardo Freire has marked this topic as resolved.

Pierre Courtieu (Aug 12 2022 at 08:44):

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