# "Coordinates" in tree-like structure

I have this datatype:

``````Inductive formula :=
| var: nat -> formula
| neg: formula -> formula
| conj: formula -> formula -> formula
| disj: formula -> formula -> formula
| impl: formula -> formula -> formula
| equiv: formula -> formula -> formula.
``````

It’s easy to substitute all instances of some variable with a formula, but how to substitute only one specific instance? For example, in ‘conj (var 0) (var 0)’ substitute only the first ‘var 0’ with something.

How to define position in the tree? In a way that allows to say easily (to Coq) - substitute ‘var n’ at ‘position x’ with a formula.

What I would do (caveat emptor, this is written off the top of my head):

Define a type for “paths” inside a formula:

``````Inductive path :=
| Root
| Left: path -> path
| Right: path -> path.
``````

The representation is the obvious one, ie `Left (Left (Right Root))` means “go left, go left, go right, you are there!”.

Valid paths in a given formula are supposed to point to a subterm, as per:

``````Inductive points: path -> formula -> formula -> Prop :=
| points_root: forall F, points Root F
| points_neg: forall P F H, points P F H -> points (Left P) (neg F) H
| points_conj_left: forall P F G H, points P F H -> points (Left P) (conj F G) H
| points_conj_right: forall P F G H, points P G H -> points (Right P) (conj F G) H
| (* etc *)
``````

In words: `points P F G` means that the path `P` points to a subterm `G` inside `F`. A valid path `P` relative a formula `F` is one such that there exists `G` such that `points P F G`:

``````Definition valid (P : path) (F : formula) : Prop := exists G, points P F G.
``````

One can use a path to retrieve the subterm it points to:

``````Fixpoint get (P : path) (F : formula) : option formula :=
match P, F with
| Root, F => Some F
| Left P, (neg F | equiv F | conj F _ | disj F _ | impl F _) => get P F
| Right P, (conj _ F | disj _ F | impl _ F) => get P F
| _ => None
end.
``````

We should have the following equivalence:

``````Lemma points_get: forall P F G,
points P F G <-> get P F = Some G.
``````

You can define a function `subst: path -> formula -> formula -> option formula`:

``````Fixpoint subst (P : path) (F : formula) (G : formula) : option formula :=
match P, G with
| Root, _ => F
| Left P, neg G => neg (subst P F G)
| Left P, conj G H => conj (subst P F G) H
| Right P, conj G H => conj G (subst P F H)
| (* etc *)
| _ => None
end.
``````

In words: `subst P F G` is `Some H` where `H` is `G` with the term pointed to by `P` replaced by `F`, if `P` is valid in `G` and `None` otherwise.

This is made explicit by the following result:

``````Lemma valid_subst: forall P F G H,
valid P G -> subst P F G = Some H /\ points P H F.