The Coq mailing list

[Jerome Hugues <jhugues AT andrew.cmu.edu>]

Hi,

 

I am using CPDT by Adam Chipala and try to apply the content of “Nested Inductive Types” from http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html on the code below.

 

I tried to adjust it for the following type:

 

Inductive componentInstance :=

    | component_instance : nat -> list subcomponentInstance -> componentInstance

with subcomponentInstance :=

    | subcomponent_instance : nat -> componentInstance -> subcomponentInstance.

 

(see full code at the end)

 

The original code works with my Coq installation.  But my adaptation fails to pass type checking.

I end up with the following error:

 

In environment

Pc : componentInstance -> Prop

Ps : subcomponentInstance -> Prop

Pls : list subcomponentInstance -> Prop

component_case : forall (n : nat) (ls : list subcomponentInstance),

                 All Ps ls -> Pc (component_instance n ls)

componentInstance_ind' : forall c : componentInstance, Pc c

c : componentInstance

n : nat

ls : list subcomponentInstance

subcomponentInstance_ind : list subcomponentInstance -> All Ps ls

lsi : list subcomponentInstance

The term "I" has type "True" while it is expected to have type "All Ps ls".

Not in proof mode.

 

What bugs me is that All Ps ls computes to a Prop, therefore the code should work. I tried obvious modifications but could not work around this.

Is there anything obvious that I missed here?

 

Thanks for any pointers.

 

(***************************)

 

From Coq Require Import List.

 

Set Implicit Arguments.

Set Asymmetric Patterns.

 

Inductive componentInstance :=

    | component_instance : nat -> list subcomponentInstance -> componentInstance

with subcomponentInstance :=

    | subcomponent_instance : nat -> componentInstance -> subcomponentInstance.

 

Section All.

 

    Variable T : Set.

    Variable P : T -> Prop.

 

    Fixpoint All (ls : list T) : Prop :=

      match ls with

        | nil => True

        | h :: t => P h /\ All t

      end.

 

  End All.

 

Section componentInstance_ind'.

 

  Variable Pc : componentInstance -> Prop.

  Variable Ps : subcomponentInstance -> Prop.

  Variable Pls : list subcomponentInstance -> Prop.

 

  Hypothesis component_case : forall (n : nat) (ls : list subcomponentInstance),

     All Ps ls -> Pc (component_instance n ls).

 

  Definition f (ls : list subcomponentInstance) := All Ps ls. Check f.

  Definition g := All Ps nil. Check g.

  Check True. Check I.

 

Fixpoint componentInstance_ind' (c : componentInstance) : Pc c :=

  match c with

  | component_instance n ls =>

    component_case n ls

    ((fix subcomponentInstance_ind (lsi : list subcomponentInstance) : All (Ps) (ls) :=

      match lsi with

      | nil => I (* True *) (* All Ps nil *)

      | subcomponent_instance _ c' :: lsii => (componentInstance_ind' c') /\

          (subcomponentInstance_ind lsii)

      end)

    ls)

end.

 

End componentInstance_ind'.