The Coq mailing list

[Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>]

You can always write your own induction principle or make your goal
stronger as Jean-Francois Monin suggested.

Inductive L : Set :=
  | Base : L
  | Ind : L -> L.

Inductive Foo : L -> nat -> Prop :=
  | FooBase : Foo Base 0
  | FooIndBase : Foo (Ind Base) 0
  | FooIndInd : forall (l: L), Foo l 0 -> Foo (Ind (Ind l)) 0.

Definition Lind (P:L -> Prop) 
 (f:P Base)
 (f0:P (Ind Base))
 (f1:forall l, P l -> P (Ind (Ind l))) :=
 fix F (l:L) : P l :=
  match l return (P l) with
   | Base => f
   | Ind Base => f0
   | Ind (Ind l) => f1 l (F l)
  end.

Hint Constructors Foo.

Theorem foo : forall (l:L), Foo l 0.
 induction l using Lind; auto.
Qed. 

Theorem foo' : forall (l:L), Foo l 0.
 assert (forall l, Foo l 0 /\ Foo (Ind l) 0) by (induction l;
intuition).
 firstorder.
Qed. 

--

On Fri, 2007-10-12 at 13:02 +0100, Edsko de Vries wrote: 
> Hey,
> 
> The Function/functional induction very nicely solved the problem. I was
> wondering if there is a similar thing I can use in this minor variation:
> 
> Inductive L : Set :=
>   | Base : L
>   | Ind : L -> L.
> 
> Inductive Foo : L -> nat -> Prop :=
>   | FooBase : Foo Base 0
>   | FooIndBase : Foo (Ind Base) 0
>   | FooIndInd : forall (l: L), Foo l 0 -> Foo (Ind (Ind l)) 0.
> 
> Theorem foo : forall (l:L), Foo l 0.
> 
> Again, normal proof by induction is no use:
> 
> Proof.
> induction l.
> apply FooBase.
> induction l.
> apply FooIndBase.
> apply FooIndInd.
> 1 subgoal
> l : L
> IHl : Foo (Ind l) 0
> IHl0 : Foo l 0 -> Foo (Ind l) 0
> ______________________________________(1/1)
> Foo l 0
> 
> But when I do the recursion manually, the proof works:
> 
> Proof.
> refine(fix f (l:L) : Foo l 0 := _).
> elim l.
> apply FooBase.
> intros.
> elim l0.
> apply FooIndBase.
> intros.
> apply FooIndInd.
> apply f.
> Qed.
> 
> Of course I just use this style (using the refine to give me access to the
> recursive calls to the proof), but it just seems to me there should be an
> easier way.
> 
> Edsko