lengyijun has marked this topic as resolved.

lengyijun has marked this topic as unresolved.

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

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

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`

).

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`

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

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 ?

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: Jan 31 2023 at 14:03 UTC