"Coordinates" in tree-like structure

Using Coq
1

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.

Thanks in advance.

2

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

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

Best wishes,
Nicolás

1 Like