The Coq mailing list

[roconnor AT theorem.ca]

Interestingly, the following does work:

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

On Sun, 20 Sep 2009, Aaron Bohannon wrote:

> 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.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''