The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Since Coqs positivity check will actually inspect the constructors of any
inductives used in a constructor declaration (in this case fhlist), if you
define fhlist as an inductive family instead of a function the definition of
term is accepted.
The fhmember and fhget functions are roughly the same but without proof
irrelevance there are some times when writing functions over inductive
families can be very difficult in comparison so I just include this code in
case it is interesting.


Require Import List.

Section fhlist_indfamily.

Variable A: Type.

Variable B: A -> Type.

Inductive fhlist : list A -> Type :=
| fhnil : fhlist nil
| fhcons : forall a xs, B a -> fhlist xs -> fhlist (a::xs).

Variable a: A.

Fixpoint fmember {xs} (ls: fhlist xs): Type :=
  match ls with
    | fhnil => Empty_set
    | fhcons a' _ _ ls' => ((a' = a) + fmember ls')%type
  end.

Fixpoint fhget {xs} (ls : fhlist xs) : fmember ls -> B a :=
  match ls return fmember ls -> B a with
    | fhnil =>
      fun i => match i with end
    | fhcons _ _ Ba ls' =>
      fun i =>
        match i with
          | inl p =>
            match p with
              | refl_equal => Ba
            end
          | inr i' => fhget ls' i'
        end
  end.

End fhlist_indfamily.

(* Fixed set of types. *)
Parameter type: Set.

(* Give myself a type to play with. *)
Parameter Unit: type.

(* Terms are indexed by types. *)
Inductive term: type -> Type :=
    (* Vars are of type Unit for now *)
    | Var: term Unit
    (* Fixed arity: imagine this is an application of a function of
type a -> b -> c *)
    | App2 (a b c: type): term a -> term b -> term c
    (* Variable arity *)
    | App (ls: list type) (c: type): fhlist type term ls -> term c.


(note: If you added another constructor similar to:
| break_positivity_for_term : forall a, (B a -> True) -> fhlist nil.
to fhlist, then it would still be accepted as strictly positive, but term
will be rejected)

-- 
View this message in context: 
http://www.nabble.com/Heterogenous-lists-and-variable-arity-constructors-tp21329660p21351832.html
Sent from the Coq mailing list archive at Nabble.com.