Context: I have been trying to implement the unification algorithm (the algorithm to find the most general unifier of two abstract syntax trees). Since a unifier is a substitution, algorithm requires defining composition of substitutions.
To be specific, given a type treeSigma dependent on another type X, a substitution is a function of type:
X -> treeSigma X
and the function substitute takes a substitution as an input and has type
substitute: (X-> (treeSigma X))-> (treeSigma X) -> (treeSigma X)
I need to define a function to compose two substitutions:
compose_kleisli (rho1 rho2: X->(treeSigma X)) : (treeSigma X) := ...
such that,
forall tr: treeSigma X,
substitute (compose_kleisli rho1 rho2) tr = substitute rho1 (substitute rho2 tr).
I am fairly new to coq and have been stuck with defining this composition. How can I define this composition?
I tried to define it using Record like this:
Record compose {X s} (rho1 rho2: X-> treeSigma X):= mkCompose{
RHO: X-> treeSigma X;
CONDITION: forall t, substitute RHO t = substitute rho2 (substitute rho1 t)
}.
but along with this, I would need to prove the result that the composition can be defined for any two substitutions. Something like:
Theorem composeTotal: forall {X s} (rho1 rho2: X-> treeSigma s X), exists rho3,
forall t, substitute rho3 t = substitute rho2 (substitute rho1 t).
Proving this would require a construction of rho3 which circles back to the same problem of defining compose.
treeSigma is defined as:
(* Signature *)
Record sigma: Type := mkSigma {
symbol : Type;
arity : symbol -> nat
}.
Record sigmaLeaf (s:sigma): Type := mkLeaf {
cLeaf: symbol s;
condLeaf: arity s cLeaf = 0
}.
Record sigmaNode (s:sigma): Type := mkNode {
fNode: symbol s;
condNode: arity s fNode <> 0
}.
(* Sigma Algebra *)
Record sigAlg (s:sigma) (X:Type) := mkAlg {
Carrier: Type;
meaning: forall f:(sigmaNode s), (Vector.t Carrier (arity s (fNode s f))) -> Carrier;
meanLeaf: forall f:(sigmaLeaf s), Vector.t Carrier 0 -> Carrier
}.
(* Abstract tree on arbitrary signature. *)
Inductive treeSigma (s:sigma) (X:Type):=
| VAR (x:X)
| LEAF (c: sigmaLeaf s)
| NODE (f: sigmaNode s) (sub: Vector.t (treeSigma s X) (arity s (fNode s f)) ).
(* Defining abstract syntax as a sigma algebra. *)
Definition meanTreeNode {s X} (f:sigmaNode s) (sub: Vector.t (treeSigma s X) (s.(arity)
(fNode s f))): treeSigma s X:= NODE s X f sub.
Definition meanTreeLeaf {s X} (c:sigmaLeaf s) (sub: Vector.t (treeSigma s X) 0) := LEAF s X c.
Definition treeSigAlg {s X} := mkAlg s X (treeSigma s X) meanTreeNode meanTreeLeaf.
The substitution function is defined as:
Fixpoint homoSigma1 {X:Type} {s} (A: sigAlg s X) (rho: X-> (Carrier s X A))
(wft: (treeSigma s X)) {struct wft}: (Carrier s X A) :=
match wft with
| VAR _ _ x => rho x
| LEAF _ _ c => meanLeaf s X A c []
| NODE _ _ f l2 => meanNode s X A f (
(fix homoSigVec k (l2:Vector.t _ k):= match l2 with
| [] => []
| t::l2s => (homoSigma1 A rho t):: (homoSigVec (vlen _ l2s) l2s)
end)
(arity s (fNode s f)) l2)
end.
Definition substitute {X s} (rho: X-> treeSigma s X) (t: treeSigma s X) := @homoSigma1 X s treeSigAlg rho t.
To be particular, a substitution is the homomorphic extension of rho (which is a variable valuation).
Definitions like this are challenging to work with because the tree type occurs recursively inside of another inductive type. Coq has trouble generating induction principles for these types on its own, so you need to help it a little bit. Here is a possible solution, for a slightly simplified set up:
Require Import Coq.Vectors.Vector.
Import VectorNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Dev.
Variable symbol : Type.
Variable arity : symbol -> nat.
Record alg := Alg {
alg_sort :> Type;
alg_op : forall f : symbol, Vector.t alg_sort (arity f) -> alg_sort;
}.
Arguments alg_op {_} f _.
(* Turn off the automatic generation of induction principles.
This tree type does not distinguish between leaves and nodes,
since they only differ in their arity. *)
Unset Elimination Schemes.
Inductive treeSigma (X:Type) :=
| VAR (x:X)
| NODE (f: symbol) (args : Vector.t (treeSigma X) (arity f)).
Arguments NODE {X} _ _.
Set Elimination Schemes.
(* Manual definition of a custom induction principle for treeSigma.
HNODE is the inductive case for the NODE constructor; the vs argument is
saying that the induction hypothesis holds for each tree in the vector of
arguments. *)
Definition treeSigma_rect (X : Type) (T : treeSigma X -> Type)
(HVAR : forall x, T (VAR x))
(HNODE : forall f (ts : Vector.t (treeSigma X) (arity f))
(vs : Vector.fold_right (fun t V => T t * V)%type ts unit),
T (NODE f ts)) :
forall t, T t :=
fix loopTree (t : treeSigma X) : T t :=
match t with
| VAR x => HVAR x
| NODE f ts =>
let fix loopVector n (ts : Vector.t (treeSigma X) n) :
Vector.fold_right (fun t V => T t * V)%type ts unit :=
match ts with
| [] => tt
| t :: ts => (loopTree t, loopVector _ ts)
end in
HNODE f ts (loopVector (arity f) ts)
end.
Definition treeSigma_ind (X : Type) (T : treeSigma X -> Prop) :=
@treeSigma_rect X T.
Definition treeSigma_alg (X:Type) : alg := {|
alg_sort := treeSigma X;
alg_op := @NODE X;
|}.
Fixpoint homoSigma {X : Type} {Y : alg} (ρ : X -> Y) (t : treeSigma X) : Y :=
match t with
| VAR x => ρ x
| NODE f xs => alg_op f (Vector.map (homoSigma ρ) xs)
end.
Definition substitute X (ρ : X -> treeSigma X) (t : treeSigma X) : treeSigma X :=
@homoSigma X (treeSigma_alg X) ρ t.
(* You can define composition simply by applying using substitution. *)
Definition compose X (ρ1 ρ2 : X -> treeSigma X) : X -> treeSigma X :=
fun x => substitute ρ1 (ρ2 x).
(* The property you are looking for follows by induction on the tree. Note
that this requires a nested induction on the vector of arguments. *)
Theorem composeP X (ρ1 ρ2 : X -> treeSigma X) t :
substitute (compose ρ1 ρ2) t = substitute ρ1 (substitute ρ2 t).
Proof.
unfold compose, substitute.
induction t as [x|f ts IH]; trivial.
simpl; f_equal.
induction ts as [|n t ts IH']; trivial.
simpl.
destruct IH as [e IH].
rewrite e.
f_equal.
now apply IH'.
Qed.
End Dev.