The Coq mailing list

["Lasser, Samuel M." <Samuel.Lasser AT tufts.edu>]

Hi Suneel,

Here's a pattern that I sometimes use to define these kinds of functions without Program Fixpoint. You can add, as an extra parameter, a proof term showing that (length l1 + length l2) is accessible in the lt relation.

===

Require Import List Omega.

Ltac inv H := inversion H; subst; clear H.

Fixpoint either' (l1 l2 : list nat)

                            (Ha : Acc lt (length l1 + length l2))

                            {struct Ha} : list nat.

  refine (match (l1, l2) as pr return (l1, l2) = pr -> _ with

               | (nil, _) => fun _ => nil

               | (_, nil) => fun _ => nil

               |(a1 :: l1', a2 :: l2') =>

                   fun Heq =>

                     match Nat.leb a1 a2 with

                     | true  => a1 :: either' l1' ((a2 - a1) :: l2') _

                     | false => a2 :: either' ((a1 - a2) :: l1') l2' _

                     end

               end eq_refl).

  - inv Heq.

    eapply Acc_inv; eauto.

  - inv Heq.

    eapply Acc_inv; eauto; simpl.

    omega.

Defined.

===

Then you can define a top-level function that calls either' with an appropriate initial Acc term:

===

Definition either (l1 l2 : list nat) : list nat := 

  either' l1 l2 (lt_wf (length l1 + length l2)). 

===

Best of luck,

Sam

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Suneel Sarswat <suneel.sarswat AT gmail.com>
Sent: Tuesday, August 11, 2020 3:26 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] Program Fixpoint and a function involving two lists

 

I am trying to write a function involving two lists. In each iteration, one of the lists decreases strictly. The Fixpoint doesn't work so tried Program Fixpoint with the measure on the sum of the length of the two lists. Here is a minimum working example

Require Import Wf.
Program Fixpoint either (l1:list nat) (l2: list nat) {measure (|l1| + |l2|)}:=
match (l1,l2) with
|(nil, _) => nil
|(_,nil) => nil
|(a1::l1',a2::l2') => match (Nat.leb a1 a2) with
  |true  => a1::either l1' ((a2 -a1)::l2')
  |false => a2::either ((a1-a2)::l1') l2'
  end
  end.

Next Obligation.
simpl. omega. Qed.

Lemma trivial1 (l1: list nat) (l2: list nat): (hd (either l1 l2)) = (hd l1)\/(hd (either l1 l2)) = (hd l2).
Proof. simpl. induction l1 as [| a1 l1']. left. auto. case l2 as [|a2 l2']. right. auto.
destruct (Nat.leb a1 a2) eqn:H1. right. unfold either. unfold either_func.    

After the last tactic, I got stuck. It gives me a huge goal which let alone proving, I don't even understand.

I tried finding this out on the internet. I got a post on stack exchange regarding this but that is not working. I got an error "fix_sub_eq_ext" not recognized when I run 'rewrite fix_sub_eq_ext' as per the instruction on the post. Besides this, I also did not understand how do these tactics work. Is there any tutorial or paper where I can learn more about Program Fixpoint related tactics with a lot of examples?

Besides this, is there an alternative way to write functions involving two or more lists where only one of them is strictly decreasing in each iteration. And prove their properties.

Thanks,

Suneel