The Coq mailing list

[Paul Brauner <paul.brauner AT loria.fr>]

Hello,

I'm having some (I guess) usual problem with dependent types, and I
don't know the (I hope) usual way to handle it. In the following
example, I've tried to reproduce the minimal subset of my problem :

    Inductive Nat : nat -> Prop :=
     | c0 : Nat 0
     | cn : forall n, Nat n -> Nat (S n)
    .

    Variable F :  Set.
    Variable h : F -> nat.
    Inductive T : Set := 
      | app : forall (s:F) (t:Nat (h s)), T
    .


What's releveant is that Nat is a dependent inductive type and that app
put a constraint on the type of t.

Then, if we define a predicate G like this :

    Definition G (n:nat) (l:Nat n) := True.

Dependent inversion on l for the following goal succeeds.

    Coq < Goal forall (s:F) (n:Nat (h s)), G (h s) n.
    1 subgoal
  
      ============================
       forall (s : F) (n : Nat (h s)), G (h s) n

    Unnamed_thm < dependent inversion n.
    2 subgoals
  
      s : F
      n : Nat (h s)
      H0 : 0 = h s
      ============================
       G 0 c0

    subgoal 2 is:
     G (S n0) (cn n0 n1)

Whereas dependent with the following definition :

    Definition G (n:nat) (t:T) (l:Nat n) := True.

the following goal does not allow dependent inversion.

    Coq < Goal forall (s:F) (n:Nat (h s)), G (h s) (app s n) n.
    1 subgoal
  
      ============================
       forall (s : F) (n : Nat (h s)), G (h s) (app s n) n

    Unnamed_thm < dependent inversion n.
    Toplevel input, characters 0-21
    > dependent inversion n.
    > ^^^^^^^^^^^^^^^^^^^^^
    Error: Illegal application (Type Error): 
    The term "app" of type "forall s : F, Nat (h s) -> T"
    cannot be applied to the terms
     "s" : "F"
     "n1" : "Nat n0"
    The 2nd term has type "Nat n0" which should be coercible to 
    "Nat (h s)"

 
This is partly explained by the fact that the following fails:

    Coq < Goal forall (s:F) (n:Nat (h s)), G (h s) (app s n) n.
    1 subgoal
  
      ============================
       forall (s : F) (n : Nat (h s)), G (h s) (app s n) n

    Unnamed_thm < intros.
    1 subgoal
  
      s : F
      n : Nat (h s)
      ============================
       G (h s) (app s n) n

    Unnamed_thm < generalize (h s).
    Toplevel input, characters 0-16
    > generalize (h s).
    > ^^^^^^^^^^^^^^^^
    Error: Illegal application (Type Error): 
    The term "G" of type "forall n : nat, T -> Nat n -> Prop"
    cannot be applied to the terms
     "n0" : "nat"
     "app s n" : "T"
     "n" : "Nat (h s)"
    The 3th term has type "Nat (h s)" which should be coercible to 
    "Nat n0"


My guess is that I should write some inversion principle by hand which
would look like :

  forall n, n=(h s) -> ....

but I didn't manage to.

Thanks in advance for your answers.