# Library Term

This library defines the type term of infinite terms.

Require Export List.
Require Import Bool_nat.
Require Export Vector.
Require Export Signature.
Require Export Variables.
Require Import FiniteTerm.

Set Implicit Arguments.

Section Term.

Terms are defined coinductively over a signature F and a set of variables X.

Variable F : signature.
Variable X : variables.

CoInductive term : Type :=
| Var : X -> term
| Fun : forall f : F, vector term (arity f) -> term.

Notation terms := (vector term).
Notation fterm := (finite_term F X).
Notation fterms := (vector fterm).

Definition root (t : term) : X + F :=
match t with
| Var x => inl _ x
| Fun f v => inr _ f
end.

Definition is_var (t : term) : bool :=
match t with
| Var _ => true
| _ => false
end.

Trivial image of finite_term in term.
Fixpoint finite_term_as_term (t : fterm) : term :=
match t with
| FVar x => Var x
| FFun f args => Fun f (vmap finite_term_as_term args)
end.

The following definition and lemma seem quite pointless. However, they can be used to take apart a coinductive term up to depth 1, i.e. unfold its corecursive definition.

Definition peek (t : term) : term :=
match t with
| Var x => Var x
| Fun f args => Fun f args
end.

Lemma peek_eq : forall (t : term), t = peek t.
destruct t; reflexivity.
Qed.

End Term.

Implicit Arguments Var [F X].

Coercion finite_term_as_term : finite_term >-> term.

Notation position := (list nat).

Section Position.

Positions in terms are lists of natural numbers.

Variable F : signature.
Variable X : variables.

Notation term := (term F X).
Notation fterm := (finite_term F X).

Definition position_depth (p : position) := length p.

Subterm of a term at some position.
Fixpoint subterm (t : term) (p : position) {struct p} : option term :=
match p with
| nil => Some t
| n :: p => match t with
| Var _ => None
| Fun f args => match lt_ge_dec n (arity f) with
| left h => subterm (vnth h args) p
| right _ => None
end
end
end.

Subterm of a finite term at some position is again finite.
Fixpoint finite_subterm (t : fterm) (p : position) {struct p} : option fterm :=
match p with
| nil => Some t
| n :: p => match t with
| FVar _ => None
| FFun f args => match lt_ge_dec n (arity f) with
| left h => finite_subterm (vnth h args) p
| right _ => None
end
end
end.

Coinductive infinite predicate.
CoInductive term_inf : term -> Prop :=
| Fun_inf : forall f v i, term_inf (v i) -> term_inf (Fun f v).

Alternative infinite predicate via positions.
Definition infinite (t : term) : Prop :=
forall d,
exists p : position,
position_depth p = d /\ subterm t p <> None.

I guess we should be able to prove these predicates to define the same subset of infinite terms, but my (small) tries below did not succeed.

Require Import Equality.

Lemma infinite_implies_term_inf :
forall t, infinite t -> term_inf t.
Proof.
cofix co.
intros [x | f v] H.
unfold infinite in H.
specialize H with 1.
destruct H as [[| a p] [D H]].
inversion D.
reflexivity.
We need to establish that there is an n such that for every depth there exists a p with n::p etc.

I don't see how to get there, but it ought to be possible since (arity f) is finite, using something akin to the pigeon hole principle.

Lemma term_inf_implies_infinite :
forall t, term_inf t -> infinite t.
Proof.
intros t H d.
revert t H.
induction d as [| d IH]; intros t H.
exists nil.
split.
reflexivity.
discriminate.
destruct H.
specialize IH with (v i).
destruct IH as [p [D IH]].
assumption.

revert IH.
dependent induction i.
intro IH.
exists (0 :: p).
split.
simpl.
reflexivity.
simpl.
destruct (arity f).
inversion i0.
simpl.