The Coq mailing list

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

Dear Yishuai,

Thanks for the quick response. I shall surely look into it. Besides this, any info on Program Fixpoint and proofs involving them will be of great help to me.

Regards,

Suneel

On Tue, Aug 11, 2020 at 1:18 PM Yishuai Li <yishuai AT cis.upenn.edu> wrote:

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
>