Cody Roux (Apr 24 2022 at 17:51): Cody Roux (Apr 24 2022 at 17:51):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
Yannick Forster (Apr 24 2022 at 17:54):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
Yannick Forster (Apr 24 2022 at 17:54):Initial proof by Simon Spies with maintainability improvements by Andrej Dudenhefner
Yannick Forster (Apr 24 2022 at 17:55):I can think a bit more about your case tomorrow
Cody Roux (Apr 24 2022 at 18:31):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
Yannick Forster (Apr 27 2022 at 16:55):Oops, sorry. The cdot I think was extending a substitution at point 0, so a cons operation
Cody Roux (Apr 28 2022 at 01:18):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: Apr 19 2024 at 22:01 UTC