Stream: Coq users

Topic: Beginner's question, about `Program Fixpoint`

view this post on Zulip lengyijun (Jun 06 2022 at 11:38):

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <=? y1
        then x1::(merge xs y)
        else y1::(merge x ys)
      | _ => x
    end
  | _ => y
  end.
Next Obligation.
  apply Nat.add_le_lt_mono; auto.
Qed.

Program Fixpoint mergesort (x : list nat) {measure (length x)}: list nat :=
  match x with
  | nil => nil
  | x :: nil => x :: nil
  | x :: y :: nil => if x <=? y
    then (x :: y :: nil)
    else (y :: x :: nil)
  | x :: y :: z :: rest =>
    let a := (x :: y :: z :: rest) in
    let p := (Nat.div2 (length a)) in
    merge (mergesort (firstn p a)) (mergesort (skipn p a))
  end.
Next Obligation.
  rewrite firstn_length.
  simpl.
  apply lt_n_S.
  apply Nat.min_lt_iff.
  left.
  destruct (length rest).
  auto.
  apply lt_n_S.
  destruct n.
  auto.
  rewrite Nat.lt_div2.
  auto.
  apply Nat.lt_0_succ.
Qed.
Next Obligation.
  rewrite skipn_length.
  simpl.
  destruct (length rest).
  auto.
  destruct Nat.div2.
  auto.
  rewrite Nat.lt_succ_r.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_sub_le_add_r.
  apply le_plus_l.
Qed.

Lemma mergesort_1 : forall x, mergesort (x :: nil ) = x :: nil.
Proof.
intros.
unfold mergesort;  unfold merge;  unfold merge_func;
 rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
auto.
Qed.

Lemma mergesort_nil : mergesort nil = nil.
Proof.
intuition.
Qed.

Lemma mergesort_merge : forall il ,  merge (mergesort (firstn (Nat.div2 (length il)) il))
    (mergesort (skipn  (Nat.div2 (length il)) il)) = mergesort il.
Proof.
destruct il.
intuition.

destruct il.
simpl.
intuition.

destruct il.
simpl.
repeat rewrite mergesort_1.
unfold mergesort;
  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
 unfold merge; unfold merge_func;
    rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl.
remember ( n <=? n0 ).
destruct b; intuition.

simpl.
(* blocked here *)

view this post on Zulip Notification Bot (Jun 06 2022 at 13:17):

lengyijun has marked this topic as resolved.

view this post on Zulip Notification Bot (Jun 06 2022 at 13:17):

lengyijun has marked this topic as unresolved.

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 16:03):

At the high level, this problem would be avoided by either the old Function feature, or the new Equation plugin: they will prove for you that merge and mergesort satisfy an _unfolding lemma_, which basically shows that the function you defined actually matches the definition (or recursive equation) you wrote (example in a minute, if you want).

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 16:04):

Once you have an unfolding lemma, you can use it instead of having to do what you're doing. With Program you can do it by hand but it's not easy...

view this post on Zulip Ana de Almeida Borges (Jun 06 2022 at 21:06):

You can prove the unfolding lemma by hand, it should not be that hard. I've done this a couple of times and got the impression the idea was always the same. Here's an example in ssreflect, and here's an example without (it doesn't compile, but you can read the proof and look for the similarities with the other example):

Program Fixpoint o (w:Worm) {measure (size w)} : Epsilon0.T1 :=
  match w with
  | T => Epsilon0.zero
  | w => Epsilon0.plus (o (body  w)) (Epsilon0.ocons (o (demote (head  0 w) 1)) 0 Epsilon0.zero)
  end.
Next Obligation.
  apply body_wf; auto.
Defined.
Next Obligation.
  apply demote_head_wf; auto.
Defined.

(** Lemma that allows us to use [o] as a usual function *)
Lemma o_eq : forall w, o w =
  match w with
  | T => Epsilon0.zero
  | w => Epsilon0.plus (o (body  w)) (Epsilon0.ocons (o (demote (head  0 w) 1)) 0 Epsilon0.zero)
  end.
Proof.
  intros. unfold o. rewrite fix_sub_eq. repeat fold o.
  - simpl. destruct w. reflexivity. reflexivity.
  - intros. destruct x.
    + reflexivity.
    + repeat f_equal.
Qed.

You can find similarities in both examples:

- Defined instead of Qed in the proof obligations of Program Fixpoint;
- judiciously unfolding and refolding;
- fix_sub_eq;
- case distinction (destruct or case)
- f_equal (or its ssreflect counterpart, congr).

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:34):

That makes sense, except you only need Defined when proving that your measure is well-founded, not when proving side conditions like measure rec_call_args < measure input_args

view this post on Zulip lengyijun (Jun 07 2022 at 10:54):

Done with unfold !

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.
Require Import Coq.Logic.FunctionalExtensionality.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <=? y1
        then x1::(merge xs y)
        else y1::(merge x ys)
      | _ => x
    end
  | _ => y
  end.
Next Obligation.
  apply Nat.add_le_lt_mono; auto.
Qed.

Program Fixpoint mergesort (x : list nat) {measure (length x)}: list nat :=
  match x with
  | nil => nil
  | x :: nil => x :: nil
  | x :: y :: nil => if x <=? y
    then (x :: y :: nil)
    else (y :: x :: nil)
  | x :: y :: z :: rest =>
    let a := (x :: y :: z :: rest) in
    let p := (Nat.div2 (length a)) in
    merge (mergesort (firstn p a)) (mergesort (skipn p a))
  end.
Next Obligation.
  rewrite firstn_length.
  simpl.
  apply lt_n_S.
  apply Nat.min_lt_iff.
  left.
  destruct (length rest).
  auto.
  apply lt_n_S.
  destruct n.
  auto.
  rewrite Nat.lt_div2.
  auto.
  apply Nat.lt_0_succ.
Qed.
Next Obligation.
  rewrite skipn_length.
  simpl.
  destruct (length rest).
  auto.
  destruct Nat.div2.
  auto.
  rewrite Nat.lt_succ_r.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_succ_r.
  left.
  rewrite Nat.le_sub_le_add_r.
  apply le_plus_l.
Qed.


Lemma mergesort_refl : forall (x : list nat) , mergesort x =
  match x with
  | nil => nil
  | x :: nil => x :: nil
  | x :: y :: nil => if x <=? y
    then (x :: y :: nil)
    else (y :: x :: nil)
  | x :: y :: z :: rest =>
    let a := (x :: y :: z :: rest) in
    let p := (Nat.div2 (length a)) in
    merge (mergesort (firstn p a)) (mergesort (skipn p a))
  end.
Proof.
intros.
destruct x; auto.
destruct x; auto.
destruct x; auto.
simpl.
unfold mergesort at 1.
rewrite fix_sub_eq; simpl.
repeat f_equal.
intros.
destruct x0; auto.
destruct x0; auto.
destruct x0; auto.
simpl.
repeat f_equal.

apply functional_extensionality_dep.
intros.
apply functional_extensionality_dep.
intros.
apply H.

apply functional_extensionality_dep.
intros.
apply functional_extensionality_dep.
intros.
apply H.
Qed.


Lemma mergesort_merge : forall il ,  merge (mergesort (firstn (Nat.div2 (length il)) il))
    (mergesort (skipn  (Nat.div2 (length il)) il)) = mergesort il.
Proof.
  intros.
  rewrite (mergesort_refl il).
  destruct il; auto.
  destruct il; auto.
  destruct il; auto.
Qed.

view this post on Zulip lengyijun (Jun 07 2022 at 10:55):

or the new Equation plugin: they will prove for you that merge and mergesort satisfy an _unfolding lemma_, which basically shows that the function you defined actually matches the definition (or recursive equation) you wrote (example in a minute, if you want).

Do you mean https://github.com/mattam82/Coq-Equations ?

view this post on Zulip Ana de Almeida Borges (Jun 13 2022 at 15:28):

Paolo Giarrusso said:

That makes sense, except you only need Defined when proving that your measure is well-founded, not when proving side conditions like measure rec_call_args < measure input_args

Are you sure of this? I just tested it on one of the examples I gave above (this) and with Qed instead of Defined I believe I would have needed functional extensionality.

Last updated: Apr 16 2024 at 09:01 UTC