HORS を Coq で扱うにはどうしたらいいんでしょーか．

hors.v

(* HORS? *)

Set Implicit Arguments.
Require Import List.

CoInductive List (A: Set): Set :=
| Nil | Cons (head: A)(tail: List A).
Arguments Nil {A}.
Arguments Cons {A}(head)(tail).

Fixpoint Nth {A: Set}(n: nat)(l: List A): option A :=
  match n, l with
    | 0, Cons h _ => Some h
    | S n, Cons _ t => Nth n t
    | _, _ => None
  end.

Notation "[]" := Nil.
Notation "[ X ; .. ; Y ]" := (Cons X .. (Cons Y Nil) .. ) (at level 50, no associativity).

CoInductive Tree (A: Set): Set :=
| Leaf | Node (label: A)(child: List (Tree A)).
Arguments Leaf {A}.
Arguments Node {A}(label)(child).

Notation "a :< l" := (Node a l) (at level 60, right associativity).
Notation "b :>" := (fun x => b:<[x]) (at level 50, left associativity).
Definition Path := list nat.

Fixpoint Traverse {A: Set}(path: Path)(t: Tree A): option (Tree A) :=
  match path, t with
    | nil, _ => Some t
    | n::t, _:< child =>
      match Nth n child with
        | Some c => Traverse t c
        | None => None
      end
    | _, _ => None
  end.


Section HORS.
  
  Variables (T: Set)(a b c: T).

  (* order-0
     S -> a c B
     B -> b S *)
  CoFixpoint GS0 :=
    a :< [ c:<[] ; GB0 ]
  with GB0 :=
    b :< [ GS0 ].

  Eval compute in (Traverse (1::0::1::0::nil) GS0).

  (* order-1
     S -> A c
     A -> \x => a x (A b x) *)
  CoFixpoint GA1 (x: Tree T) :=
    a :< [ x ; GA1 (Node b ([ x ]))].
  Definition GS1 := GA1 (c:<[]).

  Eval compute in (Traverse (1::1::0::0::nil) GS1).

  (* order-2 
     S -> A b
     A -> \f => a (f c) (A (T f))
     T -> \f x => f (f x) *)
  (* . order-2 *)
  Definition GT2 (f: Tree T -> Tree T)(x: Tree T): Tree T := f (f x).
  (* . order-1 *)
  CoFixpoint GA2 (f: Tree T -> Tree T): Tree T :=
    a :< [ f (c:<[]) ; GA2 (GT2 f)].
  (* . order-0 *)
  Definition GS2 := GA2 (b:>).

  Eval compute in (Traverse (1::1::0::0::nil) GS2).


  (* exercise 1  *)
  Variables (br e: T).
  Definition GC2 (x y: Tree T -> Tree T)(w: Tree T): Tree T := x (y w).
  CoFixpoint GF2 (x y z: Tree T -> Tree T): Tree T :=
    br :< ([ x (y (z (e:<[]))) ; GF2 (GC2 (a:>) x) (GC2 (b:>) y) (GC2 (c:>) z) ]).
  Definition GS := GF2 (a:>) (b:>) (c:>).

  (* *)
  CoFixpoint GF' (x: Tree T) := a :< [x ; GF' ((b:>x))].
  Definition GS' := GF' (c:<[]).

End HORS.