# 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.

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.

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.

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).

| 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.

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.

contradict H.

reflexivity.

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.

contradict H.

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.

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.

unfold vhead.