The Coq mailing list

[Yishuai Li <yishuai AT cis.upenn.edu>]

Hi Suneel,

I've asked a similar question before:
https://coq.discourse.group/t/fixpoint-with-two-decreasing-arguments/544
Alternative solution are internal auxiliary fixpoint and Equations,
which are shown under that thread.

Hope it helps,
Yishuai

Suneel Sarswat <suneel.sarswat AT gmail.com> 于2020年8月11日周二 上午3:27写道：
>
> 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
>