Stream: Coq users

Topic: Unification in autosubst 2


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yannick Forster (Apr 24 2022 at 17:54):

Initial proof by Simon Spies with maintainability improvements by Andrej Dudenhefner

view this post on Zulip Yannick Forster (Apr 24 2022 at 17:55):

I can think a bit more about your case tomorrow

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 27 2023 at 02:04 UTC