Hi all! I'm having trouble defining (and proving!) unification of terms with binders, using autosubst 2.

This sounds a bit scary, but I'm not trying to do any clever higher-order unification (for now). Just boring old first-order unification, which sometimes needs to "avoid" bound variables.

The basic idea is: I want to build a `match p t`

function such that: if `match p t = Success u`

, then `p[u..] = t`

.

So far so good. I've defined the result of a match as follows: `Inductive Match := Fail | Empty | Success (_ : tm)`

and the usual `join`

operation for pattern matching:

```
Definition join (l r : Match) : Match :=
match pair l r with
| pair Empty r => r
| pair l Empty => l
| pair (Success t1) (Success t2) => if t1 == t2 then Success t1 else Fail
| pair Fail _ => Fail
| pair _ Fail => Fail
end.
```

Great! Now the bad: I don't even know how to elegantly express the variable case! I'd be tempted to do this:

```
Definition match_var (v : fin) (t : tm) : Match :=
if v == 0 then Success t else match t with | var v' => if shift v' == v then Empty else Fail | _ => Fail end.
```

Ok that's pretty ugly, and worse, doesn't work at all with binders! I need something like

```
Definition match_var (level v : fin) (t : tm) : Match := ...
```

and cases for `v < level`

, `v == level`

and `level < v`

. Eesh. I have tried this, but I cannot for the life of me get the lemmas right.

It feels like I'm working against the grain here, and I should be passing around renamings (somehow). Any ideas?

@Yannick Forster @Gert Smolka

I'm not sure whether that's helpful, but off the top of my head I can tell you that we have a decision procedure for the first-order case of higher order unification here: https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.15/theories/HOU/firstorder.v

Initial proof by Simon Spies with maintainability improvements by Andrej Dudenhefner

I can think a bit more about your case tomorrow

Ok that's very cool!

Can you remind me what the \cdot notation is here? https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.15/theories/HOU/firstorder.v#L21

Oops, sorry. The cdot I think was extending a substitution at point 0, so a cons operation

In the spirit of following up with my silly questions, here's how I eventually solved it, (in a somewhat unsatisfying way):

I defined a function

```
Fixpoint lower_tm (level : fin) (t : tm) : option tm :=
match t with
| var_tm v => if v <? level then None else Some (var_tm (v - level))
| Z => Some Z
| Succ t' => option_map Succ (lower_tm level t')
| Add t1 t2 => option_map2 Add (lower_tm level t1) (lower_tm level t2)
| Mult t1 t2 => option_map2 Mult (lower_tm level t1) (lower_tm level t2)
end.
```

And then defined matching:

```
Definition match_var (level : fin) (v : fin) (t : tm) : Match tm :=
if v <? level then
match t with
| var_tm v' => if v =? v' then Empty
else Fail
| _ => Fail
end
else if v =? level then
match lower_tm level t with
| Init.Datatypes.Some t => Success t
| None => Fail
end
else
match t with
| var_tm v' => if v =? shift v' then Empty
else Fail
| _ => Fail
end.
(*
We want:
match_tm (Add (var_tm 0) (var_tm 1)) (Add Z (var_tm 0)) = Success Z
*)
Fixpoint match_tm (level : fin) (p : tm) (t : tm) : Match tm :=
match pair p t with
| pair (var_tm v) t' => match_var level v t
| pair Z Z => Empty
| pair (Succ p') (Succ t') => match_tm level p' t'
| pair (Add p1 p2) (Add t1 t2) =>
join (match_tm level p1 t1) (match_tm level p2 t2)
| pair (Mult p1 p2) (Mult t1 t2) =>
join (match_tm level p1 t1) (match_tm level p2 t2)
| _ => Fail
end.
```

Finally, I defined a generalized `scons`

function:

```
Definition ncons {X : Type}{var : Var fin X} (level : fin) (x : X) (xi : fin -> X) :=
fun n =>
if n <? level then var n
else if n =? level then x
else xi (Nat.pred n).
Lemma ncons_0 : forall X (Vinst : Var fin X) x xi k,
ncons 0 x xi k = scons x xi k.
Proof.
...
Qed.
Lemma ncons_scons : forall k level u, (var_tm 0, ncons level u ids >> ren_tm ↑) k = ncons (↑ level) u⟨↑⟩ ids k.
Proof.
...
Qed.
```

The crucial lemma then is stated:

```
Lemma match_var_subst_success : forall v t u level, match_var level v t = Success u -> (var_tm v)[ncons level (lift_tm_n level u) ids] = t.
```

I'm not really satisfied though: it only matches 1 variable at a time, which can bring pain, and generalizing it seems like it will be torture, not to talk about matching against 2nd order vars.

I wonder if I would have been better off with metavars. Probably not.

Last updated: Jan 27 2023 at 02:04 UTC