The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

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