Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint definition


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
  • Cc: Michiel Helvensteijn <mhelvens AT gmail.com>, Pierre Casteran <pierre.casteran AT labri.fr>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Fixpoint definition
  • Date: Mon, 15 Jul 2013 17:42:43 -0700

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



Archive powered by MHonArc 2.6.18.

Top of Page