The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Mon, 12 Apr 2010 07:28:54 +0200, Jianzhou Zhao  
<jianzhou AT seas.upenn.edu> a écrit:

> Hi All,
>
> Consider a definition:
>
> Inductive A : Set :=
> | A1 : A
> | A2 : A ->A.
>
> If we have a recursion on a prod of A
>
> Fixpoint test' (aa:A*A) : bool :=
> match aa with
> | (A1, A1) => true
> | (A2 a1, A2 a1') => test' (a1, a1')
> | (_, _) => false
> end.
>
> It is ill-formed:
> Recursive call to test' has principal argument equal to
> "(a1, a1')"
> instead of a subterm of aa.
>
> With a measure function, a recursion can be defined:
>
> Fixpoint Asize (a:A) : nat :=
> match a with
> | A1 => 1
> | A2 a' => 1+ Asize a'
> end.
>
> Definition Asize2 (aa:A*A) :=
> match aa with
> | (a1, a2) => Asize a1 + Asize a2
> end.
>
> Function test (aa:A*A) {measure Asize2} : bool :=
> match aa with
> | (A1, A1) => true
> | (A2 a1, A2 a1') => test (a1, a1')
> | (_, _) => false
> end.
>
> But (a1, a1') seems a subtern of (A2 a1, A2 a1')
> to me, because a1 and a1' are subterms of
> A2 a1 and A2 a1' respectively.
>
> Thanks

As Pierre replied, (a1, a1') is not a subterm of (A2 a1, A2 a1').

When you want to do a recursion, you must think of what is the decreasing  
argument.

Here, it is the first (or the second, if you don't want the first)  
projection of your couple.
It is far more convenient than sum of depth of first and second projection.
(try:
Function test (aa:A*A) {measure (fun x => Asize (fst x))} : bool :=
match aa with
| (A1, A1) => true
| (A2 a1, A2 a1') => test (a1, a1')
| (_, _) => false
end.
intros _ _ _ a1 _ a1' _ _.
simpl.
left.
Qed.

The proof is easier than with Asize2)


Do not forget that in Coq, with can use higher order, so that with  
curryfication/decurryfication,
a simple way to see you function is
a function which for every A associates a function from A to bool.

Then your function can be written:

Fixpoint test'' (aa bb: A) : bool :=
match aa, bb with
| A1, A1 => true
| A2 a1, A2 a1' => test'' a1 a1'
| _, _ => false
end.


Definition test' (aa: A*A): bool := test'' (fst aa) (snd aa).

(syntactic sugar for:

fix test'' (aa bb : A) : bool :=
  match aa with
  | A1 => match bb with
          | A1 => true
          | A2 _ => false
          end
  | A2 a1 => match bb with
             | A1 => false
             | A2 a1' => test'' a1 a1'
             end
  end
     : A -> A -> bool

as you can see by "Print test''."
)

Or you can use this form which is more complicate but nearer of what I  
said earlier:


Fixpoint test'' (aa: A) : A -> bool :=
match aa with
| A1 => fun (bb: A) => match bb with A1 => true | _ => false end
| A2 a1 => let recursively_defined := test'' a1 in
           fun (bb: A) => match bb with A2 a1' => recursively_defined a1'
                                      | _ => false end
end.

It is not as readable, but the fact that calls of recursive test'' is well  
formed is obvious.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay