The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Jul 15, 2013 at 1:16 PM, Jacques-Henri Jourdan
<jacques-henri.jourdan AT inria.fr>
 wrote:
>>
>> But it's structurally decreasing through both `lst` and `pair`, and
>> basic `Fixpoint` only understands *really trivial* structural
>> decreasing arguments.
>>
>
> Well, but it does works when it is through pair then lst, but not through 
> lst then pair, which is really confusing.

Here's one way to define a recursion principle on pairs in A * mylist A:

Inductive mylist (A:Type) : Type :=
| mynil : mylist A
| mycons : A * mylist A -> mylist A.

Definition mylist_rect' {A:Type} (P:mylist A -> Type)
  (Pnil : P (mynil A)) (Pcons : forall (x:A) (l:mylist A),
                          P l -> P (mycons A (x, l))) :
  forall l : mylist A, P l :=
fix F (l : mylist A) : P l :=
match l return P l with
| mynil => Pnil
| mycons (x, l') => Pcons x l' (F l')
end.

Definition mylist_pair_rect {A:Type}
  (P : A * mylist A -> Type) (Pnil : forall x:A, P (x, mynil A))
  (Pcons : forall (x:A) (pr:A * mylist A), P pr -> P (x, mycons A pr))
  (pr : A * mylist A) : P pr.
destruct pr as [x l].
revert x.
induction l using mylist_rect'.
exact Pnil.
intros.
apply Pcons.
apply IHl.
Defined.

(* Which expands to: *)
Definition mylist_pair_rect' {A:Type}
  (P : A * mylist A -> Type) (Pnil : forall x:A, P (x, mynil A))
  (Pcons : forall (x:A) (pr:A * mylist A), P pr -> P (x, mycons A pr))
  (pr : A * mylist A) : P pr :=
let (x, l) as p return (P p) := pr in
  mylist_rect' (fun m:mylist A => forall x:A, P (x, m))
  Pnil
  (fun (x':A) (l':mylist A) (IHl : forall x'':A, P (x'', l')) (x'':A) =>
  Pcons x'' (x', l') (IHl x'))
  l x.
-- 
Daniel Schepler