The Coq mailing list

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

Sorry to come after the battle, but you also could use Inductive.
ie.

Inductive VarIn: toto -> Prop :=
| IsVar: VarIn Var
| LeftPlus: forall t, VarIn t -> forall u, VarIn (Plus t u)
| RightPlus: forall t, VarIn t -> forall u,
             ~VarIn u -> VarIn (Plus u t).

Such a definition can be more handy since you often have less things to
destruct.

For instance, if you want to prove something having (VarIn x) as
hypothesis, then in the fixpoint version, you will may have to perform
something like:

induction x as [|left right|].
  (* Var *)
  ...
 (* Plus *)
 case_eq (bVarIn left)
  (* left contains Var *)
  ...
 (* right contains Var *)
 ...
(* Unit *)
destruct H.
Qed.

but with the inductive construction, you may just have to do:

induction x as [|left IHleft right|right IHright left IHleft].
  (* Var *)
  ...
 (* Plus left *)
 ...
(* Plus right *)
 ...
Qed.

That is you won't have to refine your case_eq and the Unit case
doesn't even exists; and your Prop is self contained (doesn't rely on
a decision procedure).

The (~VarIn u) in PlusRight is only here to ensure your proof unicity.

Le Mon, 11 Oct 2010 15:25:29 -0400,
Adam Chlipala 
<adam AT chlipala.net>
 a écrit :

> Gyesik Lee wrote:
> > I just defined a boolean version of [VarIn] and used it to do a
> > decision. Here is my solution.
> >
> > Fixpoint bVarIn (r:Rep) : bool :=
> >    match r with
> >      | Var        =>  true
> >      | Plus r0 r1 =>  if (bVarIn r0) then true else (bVarIn r1)
> >      | Unit          =>  false
> >    end.
> >
> > Fixpoint VarIn (r:Rep) : Prop :=
> >    match r with
> >      | Var        =>  True
> >      | Plus r0 r1 =>  if (bVarIn r0) then VarIn r0 else VarIn r1
> >      | Unit         =>  False
> >    end.
> >    
> 
> My suggestion was more along the lines of replacing the second 
> definition by:
>      Definition VarIn r := bVarIn r = true.
>