|
| 1 | +import LambdaLab.Unification.Basic |
| 2 | + |
| 3 | +/-! # Completeness of `unify` |
| 4 | +
|
| 5 | +If any unifier exists, the algorithm succeeds. Carries over from the |
| 6 | +fat-typeclass version on `archive/fat-unification`; the proof structure |
| 7 | +is the same, only the names of the bridge lemmas change. -/ |
| 8 | + |
| 9 | +/-- **Completeness of `unify`.** If any unifier exists for `eqs`, then |
| 10 | +`unify eqs` succeeds. Equivalently — and more usefully in this |
| 11 | +contrapositive form — if `unify eqs = none`, no unifier exists. Proved by |
| 12 | +induction on `unify.induct`: success branches close trivially; failure |
| 13 | +branches each contradict the unifier-exists hypothesis using one of |
| 14 | +`occurs_no_unifier`, `decomp_none_no_unifier`, or `unifier_absorb`. -/ |
| 15 | +theorem unify_complete {α : Type} [Signature α] : |
| 16 | + ∀ (eqs : Equations α) (σ : Unifier α), |
| 17 | + σ.Unifies eqs → unify eqs ≠ none := by |
| 18 | + intro eqs |
| 19 | + induction eqs using unify.induct with |
| 20 | + | case1 => |
| 21 | + intro σ _ heq |
| 22 | + rw [unify] at heq |
| 23 | + cases heq |
| 24 | + | case2 x y eqs' m hxv hyv ih => |
| 25 | + intro σ hσ |
| 26 | + have hbody : unify ((x, y) :: eqs') = unify eqs' := by |
| 27 | + rw [unify, hxv]; simp [hyv] |
| 28 | + rw [hbody] |
| 29 | + exact ih σ (fun p hp => hσ p (List.mem_cons_of_mem _ hp)) |
| 30 | + | case3 x y eqs' m hxv hyv hocc => |
| 31 | + intro σ hσ _ |
| 32 | + have hxy : σ.apply x = σ.apply y := |
| 33 | + by simpa using hσ (x, y) List.mem_cons_self |
| 34 | + have hxeq : x = Signature.var m := Signature.var_of_isVar x m hxv |
| 35 | + rw [hxeq] at hxy |
| 36 | + exact Signature.occurs_no_unifier y m σ hocc hyv hxy |
| 37 | + | case4 x y eqs' m hxv hyv hocc rest hrest _ => |
| 38 | + intro _ _ heq |
| 39 | + have hbody : unify ((x, y) :: eqs') = some ((m, y) :: rest) := by |
| 40 | + rw [unify, hxv]; simp [hyv, hocc, hrest] |
| 41 | + rw [hbody] at heq |
| 42 | + cases heq |
| 43 | + | case5 x y eqs' m hxv hyv hocc hnone ih => |
| 44 | + intro σ hσ _ |
| 45 | + have hxy : σ.apply x = σ.apply y := |
| 46 | + by simpa using hσ (x, y) List.mem_cons_self |
| 47 | + have hxeq : x = Signature.var m := Signature.var_of_isVar x m hxv |
| 48 | + rw [hxeq] at hxy |
| 49 | + have hσ_sub : σ.Unifies (HasSubst.single eqs' m y) := by |
| 50 | + intro p hp |
| 51 | + rw [Equations.single_eq] at hp |
| 52 | + rcases List.mem_map.mp hp with ⟨q, hq, hqeq⟩ |
| 53 | + subst hqeq |
| 54 | + have hq_unif := hσ q (List.mem_cons_of_mem _ hq) |
| 55 | + rw [Signature.unifier_absorb σ q.1 m y hxy, |
| 56 | + Signature.unifier_absorb σ q.2 m y hxy] |
| 57 | + exact hq_unif |
| 58 | + exact ih σ hσ_sub hnone |
| 59 | + | case6 x y eqs' hxv m hyv hocc => |
| 60 | + intro σ hσ _ |
| 61 | + have hxy : σ.apply x = σ.apply y := |
| 62 | + by simpa using hσ (x, y) List.mem_cons_self |
| 63 | + have hyeq : y = Signature.var m := Signature.var_of_isVar y m hyv |
| 64 | + rw [hyeq] at hxy |
| 65 | + have hxv' : Signature.isVar x ≠ some m := by rw [hxv]; intro h; cases h |
| 66 | + exact Signature.occurs_no_unifier x m σ hocc hxv' hxy.symm |
| 67 | + | case7 x y eqs' hxv m hyv hocc rest hrest _ => |
| 68 | + intro _ _ heq |
| 69 | + have hbody : unify ((x, y) :: eqs') = some ((m, x) :: rest) := by |
| 70 | + rw [unify, hxv, hyv]; simp [hocc, hrest] |
| 71 | + rw [hbody] at heq |
| 72 | + cases heq |
| 73 | + | case8 x y eqs' hxv m hyv hocc hnone ih => |
| 74 | + intro σ hσ _ |
| 75 | + have hxy : σ.apply x = σ.apply y := |
| 76 | + by simpa using hσ (x, y) List.mem_cons_self |
| 77 | + have hyeq : y = Signature.var m := Signature.var_of_isVar y m hyv |
| 78 | + rw [hyeq] at hxy |
| 79 | + have hxy' : σ.apply (Signature.var m) = σ.apply x := hxy.symm |
| 80 | + have hσ_sub : σ.Unifies (HasSubst.single eqs' m x) := by |
| 81 | + intro p hp |
| 82 | + rw [Equations.single_eq] at hp |
| 83 | + rcases List.mem_map.mp hp with ⟨q, hq, hqeq⟩ |
| 84 | + subst hqeq |
| 85 | + have hq_unif := hσ q (List.mem_cons_of_mem _ hq) |
| 86 | + rw [Signature.unifier_absorb σ q.1 m x hxy', |
| 87 | + Signature.unifier_absorb σ q.2 m x hxy'] |
| 88 | + exact hq_unif |
| 89 | + exact ih σ hσ_sub hnone |
| 90 | + | case9 x y eqs' hxv hyv xs hdec ih => |
| 91 | + intro σ hσ |
| 92 | + have hbody : unify ((x, y) :: eqs') = unify (xs ++ eqs') := by |
| 93 | + rw [unify, hxv, hyv, hdec] |
| 94 | + rw [hbody] |
| 95 | + have hxy : σ.apply x = σ.apply y := |
| 96 | + by simpa using hσ (x, y) List.mem_cons_self |
| 97 | + have hσ' : σ.Unifies (xs ++ eqs') := by |
| 98 | + intro p hp |
| 99 | + rcases List.mem_append.mp hp with hp_xs | hp_eqs' |
| 100 | + · exact Signature.decomp_unifier_sound x y xs σ hdec hxy p hp_xs |
| 101 | + · exact hσ p (List.mem_cons_of_mem _ hp_eqs') |
| 102 | + exact ih σ hσ' |
| 103 | + | case10 x y eqs' hxv hyv hdec => |
| 104 | + intro σ hσ _ |
| 105 | + have hxy : σ.apply x = σ.apply y := |
| 106 | + by simpa using hσ (x, y) List.mem_cons_self |
| 107 | + exact Signature.decomp_none_no_unifier x y σ hxv hyv hdec hxy |
0 commit comments