The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello Randy,

Here is my usual trick, illustrated on a very simple example:
div2 on even numbers. See also the short proof of 
(exists n, P n) -> {n:nat | P n} for decidable P,
in ConstructiveEpsilon.v

------------------------------------------------------------
(* Division by 2 of even numbers *)

Inductive even : nat -> Prop :=
  | E0 : even O
  | E2 : forall n, even n -> even (S (S n)).

Definition pos n := match n with S _ => True | _ => False end.
Definition testpos n : option (pos n) :=
  match n with 
  | O => None
  | S n => Some I
  end.

(* Returns a structurally smaller term in *EACH* case of [e] *)
Definition even_pred2 n (e:even n) : pos n -> even (pred (pred n)) :=
  match e in even n return (pos n -> even (pred (pred n))) with
    | E0 => fun F => match F return (even 0) with end
    | E2 _ e0 => fun _ => e0
  end.

(* Pitfall:
   destruct [n] doesn't work, the structural relationship with [e] is lost;
   a structurally smaller [e'] is provided using the another match done
   in [even_pred2]
*)
Fixpoint div2 (n: nat)(e: even n) {struct e} : nat :=
  match (testpos n) with
  | None => O
  | Some pn => div2 (pred (pred n)) (even_pred2 n e pn)
  end.

------------------------------------------------------------

Hope this helps,
Jean-Francois

On Fri, Nov 04, 2011 at 04:53:44PM -0400, Randy Pollack wrote:
> I have some inductively defined set, say of terms
> 
>    Inductive Term : Set := ...
> 
> and some inductively defined relation, say of reduction
> 
>   Inductive Red : Term -> Term -> Prop := ...
> 
> I want to do induction on the size of derivations of the Red relation.
>  So I try to define
> 
>   Fixpoint RedSize : (M N: Term) (r:Red M N) {struct r} : nat :=
>      match r with ...
>      end.
> 
> This fails, because Red is a Prop, not a Set.  How is this usually done?
> 
> One could index the relation Red with size, as is necessary in (simply
> typed) HOL, but it seems we should do better with dependent types.
> 
> Thanks,
> Randy
> 
>