The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Fri, 12 Oct 2007 13:02:49 +0100, Edsko de Vries 
<devriese AT cs.tcd.ie>
a écrit:
> 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.


My way of doing this is to define the foo function and use functional
induction.

Pierre Coutieu


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.

Function foo (l: L) : nat := match l with
  | Base => 0
  | Ind l' => match l' with
    | Base => 0
    | Ind l'' => foo l''
    end
  end. 

(* By the way notice that there is a relation R_foo, that looks very
much like Foo. *)

Theorem foo2 : forall (l:L), Foo l 0.
Proof.
  intros l.
  functional induction (foo l).
  constructor.
  constructor.
  constructor. assumption.
Qed.


Cheers,
Pierre Courtieu