The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

I have a little development that defines freely generated terms of a
signature of symbols with arities.  It uses vectors to ensure that
terms are well-formed.  (I know this was also done in the CoLoR
library.)  Additionally, I want to define terms with holes, so I use a
derived signature with an option type for the one extra symbol.  Now
let's say I want to write a function over these contexts to determine
whether a hole symbol appears in a term.  How does one do this?

You can step through the code below and see that my first attempt,
"no_hole", fails the termination-checker, even though the extremely
similar function "all_term" passes it.  They're so similar, in fact,
that "no_hole" is actually just a specific instance of "all_term", as
you can see from the definition of "no_hole_from_all_term".  So why
does the definition of "no_hole" fail???

Now you ask, "why do I care if I already found a way to define the
function?"  OK, well tell me now how to define a function that tests
whether exactly one hole symbol appears in a term...

 - Aaron

---- Coq code ----

Set Implicit Arguments.

Inductive vector (A: Type): nat -> Type :=
| vnil: vector A O
| vcons: forall len, A -> vector A len -> vector A (S len).
Implicit Arguments vnil [A].

Definition vall (A: Type) (P: A -> Prop)
: forall len: nat, vector A len -> Prop :=
  fix vall' (len: nat) (xs: vector A len) {struct xs}: Prop :=
    match xs in vector _ len' return Prop with
    | vnil => True
    | vcons len1 a xs1 => P a /\ vall' len1 xs1
    end.

Record signature: Type := mk_signature {
  symbol: Set;
  arity: symbol -> nat
}.

Inductive term (S: signature): Type :=
| term_app: forall a: symbol S, vector (term S) (arity S a) -> term S.

Fixpoint all_term
  (S: signature) (P: symbol S -> Prop) (t: term S) {struct t}: Prop :=
  match t with
  | term_app a ts => P a /\ vall (@all_term S P) ts
  end.

Definition context_signature (S: signature): signature :=
  let context_symbol := option (symbol S) in
  let context_arity a :=
    match a with
    | Some a1 => arity S a1
    | None => 0
    end
  in
  @mk_signature context_symbol context_arity.

Definition context (S: signature): Type :=
  term (context_signature S).

Fixpoint no_hole (S: signature) (c: context S) {struct c}: Prop :=
  match c with
  | term_app (Some a) cs => vall (@no_hole S) cs
  | term_app None _ => False
  end.

Definition no_hole_from_all_term (S: signature): context S -> Prop :=
  let isnt_hole (a: symbol (context_signature S)): Prop :=
    match a with
    | Some _ => True
    | None => False
    end
  in
  all_term isnt_hole.