syntactic unification of propositional formulas

Stream: general

[Paige Thomas]

I have been trying to find, implement and verify a syntactic unification algorithm for formulas in propositional logic. The simplest that I have found so far is an adaption of Robinson's algorithm, and below is my attempt to code it in Lean. A couple of experiments with evaluating it shows that it may be correct. I'm not sure how to prove that it terminates though, even on paper. I'm wondering if anyone might know how to do so, or may have any other advice on implementing a syntactic unification algorithm for formulas in propositional logic that is efficient enough for practical purposes and not too difficult to program and prove correct.

import Mathlib.Tactic


set_option autoImplicit false



def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


  inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_


open Formula_


/--
  `atom_occurs_in A F` := True if and only if there is an occurrence of the atom `A` in the formula `F`.
-/
def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_ => False
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | or_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | imp_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi

instance
  (A : String)
  (F : Formula_) :
  Decidable (atom_occurs_in A F) :=
  by
  induction F
  all_goals
    unfold atom_occurs_in
    infer_instance


/--
  `Formula_.atom_list F` := The list of all of the atoms that have an occurrence in the formula `F`.
-/
def Formula_.atom_list :
  Formula_ → List String
  | false_ => []
  | true_ => []
  | atom_ X => [X]
  | not_ phi => phi.atom_list
  | and_ phi psi => phi.atom_list ++ psi.atom_list
  | or_ phi psi => phi.atom_list ++ psi.atom_list
  | imp_ phi psi => phi.atom_list ++ psi.atom_list
  | iff_ phi psi => phi.atom_list ++ psi.atom_list


/--
  `replace_atom_all_rec τ F` := The simultaneous replacement of each occurrence of any atom `A` in the formula `F` by `τ A`.
-/
def replace_atom_all_rec
  (τ : String → Formula_) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => τ X
  | not_ phi => not_ (replace_atom_all_rec τ phi)
  | and_ phi psi => and_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | or_ phi psi => or_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | imp_ phi psi => imp_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | iff_ phi psi => iff_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)


structure Equation : Type where
  (lhs : Formula_)
  (rhs : Formula_)
  deriving Inhabited, DecidableEq, Repr

def Equation.atom_list
  (E : Equation) :
  List String :=
  E.lhs.atom_list ∪ E.rhs.atom_list


partial
def unify
  (E : Equation) :
  Option (String → Formula_) :=
  match E with
  | ⟨false_, false_⟩
  | ⟨true_, true_⟩ => Option.some atom_
  | ⟨atom_ X, F⟩ =>
    if atom_ X = F
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨F, atom_ X⟩ =>
    if F = atom_ X
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨not_ phi, not_ phi'⟩ => unify ⟨phi, phi'⟩
  | ⟨and_ phi psi, and_ phi' psi'⟩
  | ⟨or_ phi psi, or_ phi' psi'⟩
  | ⟨imp_ phi psi, imp_ phi' psi'⟩
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ =>
    match unify ⟨phi, phi'⟩ with
    | Option.some σ_1 =>
      match unify ⟨replace_atom_all_rec σ_1 psi, replace_atom_all_rec σ_1 psi'⟩ with
      | Option.some σ_2 => Option.some ((replace_atom_all_rec σ_2) ∘ σ_1)
      | Option.none => Option.none
    | Option.none => Option.none
  | _ => Option.none


def print_unify
  (E : Equation) :
  Option (String → Formula_) → Option (List (Formula_ × Formula_))
  | Option.none => Option.none
  | Option.some σ => Option.some (List.map (fun (X : String) => (atom_ X, σ X)) E.atom_list)


#eval! let E : Equation := ⟨atom_ "P", atom_ "Q"⟩; print_unify E (unify E)

#eval! let E : Equation := ⟨atom_ "X", not_ (atom_ "X")⟩; print_unify E (unify E)

#eval! let E : Equation := ⟨and_ (atom_ "X") (atom_ "Y"), and_ (atom_ "Y") (atom_ "Z")⟩; print_unify E (unify E)

[Alfredo Moreira-Rosa]

I would base my tree on an existing tree structure already implemented in lean/mathlib.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Tree/Basic.html

[Alexander Bentkamp]

For a paper proof, have a look here: https://en.wikipedia.org/wiki/Unification_%28computer_science%29 (Section: Proof of termination)

[Paige Thomas]

ecyrbe said:

I would base my tree on an existing tree structure already implemented in lean/mathlib.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Tree/Basic.html

I'm sorry, which tree are you referring to?

[Paige Thomas]

Alexander Bentkamp said:

For a paper proof, have a look here: https://en.wikipedia.org/wiki/Unification_%28computer_science%29 (Section: Proof of termination)

I guess I'm not entirely certain how to apply that proof to this particular algorithm.

[Paige Thomas]

Something starting along these lines?

import Mathlib.Tactic


set_option autoImplicit false



def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


  inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_


open Formula_


/--
  `Formula_.size F` := The number of subformulas in the formula `F`.
-/
def Formula_.size :
  Formula_ → Nat
  | false_ => 1
  | true_ => 1
  | atom_ _ => 1
  | not_ phi => phi.size + 1
  | and_ phi psi => phi.size + psi.size + 1
  | or_ phi psi => phi.size + psi.size + 1
  | imp_ phi psi => phi.size + psi.size + 1
  | iff_ phi psi => phi.size + psi.size + 1


/--
  `atom_occurs_in A F` := True if and only if there is an occurrence of the atom `A` in the formula `F`.
-/
def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_ => False
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | or_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | imp_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi

instance
  (A : String)
  (F : Formula_) :
  Decidable (atom_occurs_in A F) :=
  by
  induction F
  all_goals
    unfold atom_occurs_in
    infer_instance


/--
  `Formula_.atom_list F` := The list of all of the atoms that have an occurrence in the formula `F`.
-/
def Formula_.atom_list :
  Formula_ → List String
  | false_ => []
  | true_ => []
  | atom_ X => [X]
  | not_ phi => phi.atom_list
  | and_ phi psi => phi.atom_list ++ psi.atom_list
  | or_ phi psi => phi.atom_list ++ psi.atom_list
  | imp_ phi psi => phi.atom_list ++ psi.atom_list
  | iff_ phi psi => phi.atom_list ++ psi.atom_list


/--
  `replace_atom_all_rec τ F` := The simultaneous replacement of each occurrence of any atom `A` in the formula `F` by `τ A`.
-/
def replace_atom_all_rec
  (τ : String → Formula_) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => τ X
  | not_ phi => not_ (replace_atom_all_rec τ phi)
  | and_ phi psi => and_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | or_ phi psi => or_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | imp_ phi psi => imp_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | iff_ phi psi => iff_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)


structure Equation : Type where
  (lhs : Formula_)
  (rhs : Formula_)
  deriving Inhabited, DecidableEq, Repr

def Equation.atom_list
  (E : Equation) :
  List String :=
  E.lhs.atom_list ∪ E.rhs.atom_list


/--
  `List.dup_count_aux acc L` := Helper function for `List.dup_count`.
-/
def List.dup_count_aux
  {α : Type}
  [DecidableEq α]
  (acc : Finset α) :
  List α → Nat
  | [] => 0
  | hd :: tl =>
    if hd ∈ tl ∧ hd ∉ acc
    then 1 + List.dup_count_aux (acc ∪ {hd}) tl
    else List.dup_count_aux acc tl

/--
  `List.dup_count L` := The number of elements that occur more than once in the list `L`.
-/
def List.dup_count
  {α : Type}
  [DecidableEq α]
  (L : List α) :
  Nat :=
  List.dup_count_aux {} L

#eval [0].dup_count
#eval [0, 0].dup_count
#eval [0, 0, 0].dup_count
#eval [0, 0, 1].dup_count
#eval [0, 0, 1, 1].dup_count
#eval [1, 0, 0, 1].dup_count
#eval [0, 1, 0, 1].dup_count


--partial
def unify
  (E : Equation) :
  Option (String → Formula_) :=
  match E with
  | ⟨false_, false_⟩
  | ⟨true_, true_⟩ => Option.some atom_
  | ⟨atom_ X, F⟩ =>
    if atom_ X = F
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨F, atom_ X⟩ =>
    if F = atom_ X
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨not_ phi, not_ phi'⟩ => unify ⟨phi, phi'⟩
  | ⟨and_ phi psi, and_ phi' psi'⟩
  | ⟨or_ phi psi, or_ phi' psi'⟩
  | ⟨imp_ phi psi, imp_ phi' psi'⟩
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ =>
    match unify ⟨phi, phi'⟩ with
    | Option.some σ_1 =>
      match unify ⟨replace_atom_all_rec σ_1 psi, replace_atom_all_rec σ_1 psi'⟩ with
      | Option.some σ_2 => Option.some ((replace_atom_all_rec σ_2) ∘ σ_1)
      | Option.none => Option.none
    | Option.none => Option.none
  | _ => Option.none
  termination_by (E.atom_list.dup_count, E.lhs.size + E.rhs.size)
  decreasing_by
  all_goals
    sorry


def print_unify
  (E : Equation) :
  Option (String → Formula_) → Option (List (Formula_ × Formula_))
  | Option.none => Option.none
  | Option.some σ => Option.some (List.map (fun (X : String) => (atom_ X, σ X)) E.atom_list)


#eval! let E : Equation := ⟨atom_ "P", atom_ "Q"⟩; print_unify E (unify E)

#eval! let E : Equation := ⟨atom_ "X", not_ (atom_ "X")⟩; print_unify E (unify E)

#eval! let E : Equation := ⟨and_ (atom_ "X") (atom_ "Y"), and_ (atom_ "Y") (atom_ "Z")⟩; print_unify E (unify E)

[Paige Thomas]

This is an attempt at formalizing the algorithm in the Wikipedia article. I'm not so certain I did this right though, especially where I put in the match unify Γ with.

import Mathlib.Tactic


set_option autoImplicit false



def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


  inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_


open Formula_


/--
  `Formula_.size F` := The number of subformulas in the formula `F`.
-/
def Formula_.size :
  Formula_ → Nat
  | false_ => 1
  | true_ => 1
  | atom_ _ => 1
  | not_ phi => phi.size + 1
  | and_ phi psi => phi.size + psi.size + 1
  | or_ phi psi => phi.size + psi.size + 1
  | imp_ phi psi => phi.size + psi.size + 1
  | iff_ phi psi => phi.size + psi.size + 1


/--
  `atom_occurs_in A F` := True if and only if there is an occurrence of the atom `A` in the formula `F`.
-/
def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_ => False
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | or_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | imp_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi

instance
  (A : String)
  (F : Formula_) :
  Decidable (atom_occurs_in A F) :=
  by
  induction F
  all_goals
    unfold atom_occurs_in
    infer_instance


/--
  `Formula_.atom_list F` := The list of all of the atoms that have an occurrence in the formula `F`.
-/
def Formula_.atom_list :
  Formula_ → List String
  | false_ => []
  | true_ => []
  | atom_ X => [X]
  | not_ phi => phi.atom_list
  | and_ phi psi => phi.atom_list ++ psi.atom_list
  | or_ phi psi => phi.atom_list ++ psi.atom_list
  | imp_ phi psi => phi.atom_list ++ psi.atom_list
  | iff_ phi psi => phi.atom_list ++ psi.atom_list


/--
  `replace_atom_one_rec A F P` :=

  `A → F` in `P` for each occurrence of the atom `A` in the formula `P`

  The result of simultaneously replacing each occurrence of the atom `A` in the formula `P` by an occurrence of the formula `F`.
-/
def replace_atom_one_rec
  (A : String)
  (F : Formula_ ) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => if A = X then F else atom_ X
  | not_ phi => not_ (replace_atom_one_rec A F phi)
  | and_ phi psi => and_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | or_ phi psi => or_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | imp_ phi psi => imp_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | iff_ phi psi => iff_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)


/--
  `replace_atom_all_rec τ F` := The simultaneous replacement of each occurrence of any atom `A` in the formula `F` by `τ A`.
-/
def replace_atom_all_rec
  (τ : String → Formula_) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => τ X
  | not_ phi => not_ (replace_atom_all_rec τ phi)
  | and_ phi psi => and_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | or_ phi psi => or_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | imp_ phi psi => imp_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | iff_ phi psi => iff_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)


structure Equation : Type where
  (lhs : Formula_)
  (rhs : Formula_)
  deriving Inhabited, DecidableEq, Repr

def Equation.atom_list
  (E : Equation) :
  List String :=
  E.lhs.atom_list ∪ E.rhs.atom_list


/--
  `List.dup_count_aux acc L` := Helper function for `List.dup_count`.
-/
def List.dup_count_aux
  {α : Type}
  [DecidableEq α]
  (acc : Finset α) :
  List α → Nat
  | [] => 0
  | hd :: tl =>
    if hd ∈ tl ∧ hd ∉ acc
    then 1 + List.dup_count_aux (acc ∪ {hd}) tl
    else List.dup_count_aux acc tl

/--
  `List.dup_count L` := The number of elements that occur more than once in the list `L`.
-/
def List.dup_count
  {α : Type}
  [DecidableEq α]
  (L : List α) :
  Nat :=
  List.dup_count_aux {} L

#eval [0].dup_count
#eval [0, 0].dup_count
#eval [0, 0, 0].dup_count
#eval [0, 0, 1].dup_count
#eval [0, 0, 1, 1].dup_count
#eval [1, 0, 0, 1].dup_count
#eval [0, 1, 0, 1].dup_count


def var_elim
  (X : String)
  (F : Formula_)
  (L : List Equation) :
  List Equation :=
  L.map (fun (E : Equation) => ⟨replace_atom_one_rec X F E.lhs, replace_atom_one_rec X F E.rhs⟩)


partial
def unify :
  List Equation → Option (List Equation)
  | [] => Option.some []
  | ⟨false_, false_⟩ :: Γ => unify Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        if ∃ (E : Equation), E ∈ Γ ∧ (atom_occurs_in X E.lhs ∨ atom_occurs_in X E.rhs)
        then unify (⟨atom_ X, F⟩ :: var_elim X F Γ)
        else
          match unify Γ with
          | Option.none => Option.none
          | Option.some Γ' => Option.some (⟨atom_ X, F⟩ :: Γ')
  | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ)
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none


#eval! unify [⟨atom_ "P", atom_ "Q"⟩]

#eval! unify [⟨atom_ "X", not_ (atom_ "X")⟩]

#eval! unify [⟨and_ (atom_ "X") (atom_ "Y"), and_ (atom_ "Y") (atom_ "Z")⟩]

[Alexander Bentkamp]

Maybe you should deviate a bit from the wikipedia article and handle the atom case like this:

  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some Γ' => Option.some (⟨atom_ X, F⟩ :: Γ')

and then use the following measure:

• number of distinct variables occurring in the given equations
• sum of the sizes of the given equations

[Alexander Bentkamp]

But the result you get is not a standard (simultaneous) substitution. You would have to convert if you want one.

[Alexander Bentkamp]

The result substitution you get must be applied in sequence left to right.

[Paige Thomas]

Hmm. Does changing the code make it easier to prove termination?

[Paige Thomas]

Actually, it looks like that code may be wrong as I have it:

#eval! unify [⟨or_ (and_ (atom_ "X") (atom_ "Y")) (atom_ "Z"), or_ (and_ (atom_ "Y") (atom_ "Z")) (atom_ "X")⟩]

gives

some [{ lhs := Formula_.atom_ "X", rhs := Formula_.atom_ "Y" },
 { lhs := Formula_.atom_ "Y", rhs := Formula_.atom_ "Z" }]

which isn't right.

[Paige Thomas]

at least not for a simultaneous substitution. hmm.

[Paige Thomas]

I see, that is what you already pointed out. I was assuming that was just the case for the changed code.

[Paige Thomas]

It would probably be preferable to prove the single equation one:

partial
def unify
  (E : Equation) :
  Option (String → Formula_) :=
  match E with
  | ⟨false_, false_⟩
  | ⟨true_, true_⟩ => Option.some atom_
  | ⟨atom_ X, F⟩ =>
    if atom_ X = F
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨F, atom_ X⟩ =>
    if F = atom_ X
    then Option.some atom_
    else
      if atom_occurs_in X F
      then Option.none
      else Option.some (Function.updateITE atom_ X F)
  | ⟨not_ phi, not_ phi'⟩ => unify ⟨phi, phi'⟩
  | ⟨and_ phi psi, and_ phi' psi'⟩
  | ⟨or_ phi psi, or_ phi' psi'⟩
  | ⟨imp_ phi psi, imp_ phi' psi'⟩
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ => do
    let σ_1 ← unify ⟨phi, phi'⟩
    let σ_2 ← unify ⟨replace_atom_all_rec σ_1 psi, replace_atom_all_rec σ_1 psi'⟩
    (replace_atom_all_rec σ_2) ∘ σ_1
  | _ => Option.none

[Alexander Bentkamp]

Yes, I think my suggestion would make it easier to prove termination.

If you insist on your original implementation, you can probably prove termination using this measure:

• number of distinct variables in E
• syntactic size of E

But you would have to simultaneously prove that the substitutions that unify E returns have the property that all nonidentity values of the substitution contain only variables from E and do not contain the mapped variable itself.

I am not sure how you can prove such a property in Lean while you still have to prove termination. Maybe dependent types are the only option here.

[Alexander Bentkamp]

Actually, here is another idea, similar to what I proposed, but returning simultaneous substitutions:

partial
def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ => unify Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ)
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none

[Alexander Bentkamp]

You should be able to prove this terminating using:

• number of distinct variables occurring in the given equations
• sum of the sizes of the given equations

[Paige Thomas]

Do you mean something like

def equation_list_atom_list
  (L : List Equation) :
  List String :=
    List.foldr (fun (next : Equation) (prev : List String) => next.lhs.atom_list ++ next.rhs.atom_list ++ prev) [] L

#eval equation_list_atom_list []
#eval equation_list_atom_list [⟨atom_ "P", atom_ "Q"⟩]
#eval equation_list_atom_list [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "Q", atom_ "R"⟩]
#eval equation_list_atom_list [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "R", atom_ "S"⟩]


def equation_list_size
  (L : List Equation) :
  Nat :=
  List.foldr (fun (next : Equation) (prev : Nat) => next.lhs.size + next.rhs.size + prev) 0 L


def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ)
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none
  termination_by L => ((equation_list_atom_list L).dedup.length, equation_list_size L)
  decreasing_by
  all_goals
    sorry

?

[Alexander Bentkamp]

Yes! However, instead of creating a list of atoms and then calling dedup, it will probably easier to prove things if you use a Finset instead of a List to collect the atoms. Then dedup will happen automatically.

[Paige Thomas]

It seems that it is only looking at the first of the pair of terms being used to show termination? At least, it won't let me apply Prod.Lex.right in the first goal of the decreasing_by. Is there another theorem that would allow me to use the second term? Or another approach?

import Mathlib.Tactic


set_option autoImplicit false



def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


  inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_


open Formula_


/--
  `Formula_.size F` := The number of subformulas in the formula `F`.
-/
def Formula_.size :
  Formula_ → Nat
  | false_ => 1
  | true_ => 1
  | atom_ _ => 1
  | not_ phi => phi.size + 1
  | and_ phi psi => phi.size + psi.size + 1
  | or_ phi psi => phi.size + psi.size + 1
  | imp_ phi psi => phi.size + psi.size + 1
  | iff_ phi psi => phi.size + psi.size + 1


/--
  `atom_occurs_in A F` := True if and only if there is an occurrence of the atom `A` in the formula `F`.
-/
def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_ => False
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | or_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | imp_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi

instance
  (A : String)
  (F : Formula_) :
  Decidable (atom_occurs_in A F) :=
  by
  induction F
  all_goals
    unfold atom_occurs_in
    infer_instance


/--
  `Formula_.atom_set F` := The set of all of the atoms that have an occurrence in the formula `F`.
-/
def Formula_.atom_set :
  Formula_ → Finset String
  | false_ => ∅
  | true_ => ∅
  | atom_ X => {X}
  | not_ phi => phi.atom_set
  | and_ phi psi => phi.atom_set ∪ psi.atom_set
  | or_ phi psi => phi.atom_set ∪ psi.atom_set
  | imp_ phi psi => phi.atom_set ∪ psi.atom_set
  | iff_ phi psi => phi.atom_set ∪ psi.atom_set


/--
  `replace_atom_one_rec A F P` :=

  `A → F` in `P` for each occurrence of the atom `A` in the formula `P`

  The result of simultaneously replacing each occurrence of the atom `A` in the formula `P` by an occurrence of the formula `F`.
-/
def replace_atom_one_rec
  (A : String)
  (F : Formula_ ) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => if A = X then F else atom_ X
  | not_ phi => not_ (replace_atom_one_rec A F phi)
  | and_ phi psi => and_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | or_ phi psi => or_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | imp_ phi psi => imp_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | iff_ phi psi => iff_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)


/--
  `replace_atom_all_rec τ F` := The simultaneous replacement of each occurrence of any atom `A` in the formula `F` by `τ A`.
-/
def replace_atom_all_rec
  (τ : String → Formula_) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => τ X
  | not_ phi => not_ (replace_atom_all_rec τ phi)
  | and_ phi psi => and_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | or_ phi psi => or_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | imp_ phi psi => imp_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | iff_ phi psi => iff_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)


structure Equation : Type where
  (lhs : Formula_)
  (rhs : Formula_)
  deriving Inhabited, DecidableEq, Repr


def var_elim
  (X : String)
  (F : Formula_)
  (L : List Equation) :
  List Equation :=
  L.map (fun (E : Equation) => ⟨replace_atom_one_rec X F E.lhs, replace_atom_one_rec X F E.rhs⟩)


def equation_list_atom_set
  (L : List Equation) :
  Finset String :=
    List.foldr (fun (next : Equation) (prev : Finset String) => next.lhs.atom_set ∪ next.rhs.atom_set ∪ prev) {} L

#eval equation_list_atom_set {}
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩]
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "Q", atom_ "R"⟩]
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "R", atom_ "S"⟩]


def equation_list_size
  (L : List Equation) :
  Nat :=
  List.foldr (fun (next : Equation) (prev : Nat) => next.lhs.size + next.rhs.size + prev) 0 L


def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ)
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none
  termination_by L => ((equation_list_atom_set L).card, equation_list_size L)
  decreasing_by
  all_goals
    sorry

Γ : List Equation
⊢ Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) ((equation_list_atom_set Γ).card, equation_list_size Γ)
  ((equation_list_atom_set ({ lhs := false_, rhs := false_ } :: Γ)).card,
    equation_list_size ({ lhs := false_, rhs := false_ } :: Γ))

[Paige Thomas]

If I swap the order I can make progress, but then I get stuck on

  termination_by L => (equation_list_size L, (equation_list_atom_set L).card)
  decreasing_by
  · apply Prod.Lex.left
    simp only [equation_list_size]
    simp only [List.foldr_cons]
    simp only [Formula_.size]
    linarith
  · apply Prod.Lex.left
    simp only [equation_list_size]
    simp only [List.foldr_cons]
    simp only [Formula_.size]
    linarith
  · apply Prod.Lex.left
    simp only [equation_list_size]
    simp only [List.foldr_cons]
    simp only [Formula_.size]
    linarith
  · simp only [Prod.lex_def]
    sorry
  all_goals
    sorry

X : String
F : Formula_
Γ : List Equation
h✝¹ : ¬atom_ X = F
h✝ : ¬atom_occurs_in X F
⊢ equation_list_size (var_elim X F Γ) < equation_list_size ({ lhs := atom_ X, rhs := F } :: Γ) ∨
  equation_list_size (var_elim X F Γ) = equation_list_size ({ lhs := atom_ X, rhs := F } :: Γ) ∧
    (equation_list_atom_set (var_elim X F Γ)).card < (equation_list_atom_set ({ lhs := atom_ X, rhs := F } :: Γ)).card

[Paige Thomas]

If I change it to this, I make further progress:

def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        have : (var_elim X F Γ).length < Γ.length + 1 :=
        by
          unfold var_elim
          simp only [List.length_map]
          apply lt_add_one
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ)
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none
  termination_by L => (L.length, (equation_list_atom_set L).card)

I then get to the case | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ). It would seem like I should be able to use an induction hypothesis here, but there isn't one?

[Paige Thomas]

Ok, I think I see a way forward now.

[Alexander Bentkamp]

Try Prod.Lex.right' instead. I've made a proposal where to use left and where to use right' below.

And definitely use the measure ((equation_list_atom_set L).card, equation_list_size L), in this order. The other measures you are proposing will not work in my opinion.

One thing I missed is the case | ⟨F, atom_ X⟩ :: Γ => unify (⟨atom_ X, F⟩ :: Γ). My measure works only if you merge it with the previous case as follows.

def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ
  | ⟨F, atom_ X⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none
  termination_by L => ((equation_list_atom_set L).card, equation_list_size L)
  decreasing_by
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.left
    sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.left
    sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry

Full code here:

Full code

import Mathlib.Tactic


set_option autoImplicit false



def Function.updateITE
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a : α)
  (b : β)
  (c : α) :
  β :=
  if c = a then b else f c


  inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_


open Formula_


/--
  `Formula_.size F` := The number of subformulas in the formula `F`.
-/
def Formula_.size :
  Formula_ → Nat
  | false_ => 1
  | true_ => 1
  | atom_ _ => 1
  | not_ phi => phi.size + 1
  | and_ phi psi => phi.size + psi.size + 1
  | or_ phi psi => phi.size + psi.size + 1
  | imp_ phi psi => phi.size + psi.size + 1
  | iff_ phi psi => phi.size + psi.size + 1


/--
  `atom_occurs_in A F` := True if and only if there is an occurrence of the atom `A` in the formula `F`.
-/
def atom_occurs_in
  (A : String) :
  Formula_ → Prop
  | false_ => False
  | true_ => False
  | atom_ X => A = X
  | not_ phi => atom_occurs_in A phi
  | and_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | or_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | imp_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi
  | iff_ phi psi => atom_occurs_in A phi ∨ atom_occurs_in A psi

instance
  (A : String)
  (F : Formula_) :
  Decidable (atom_occurs_in A F) :=
  by
  induction F
  all_goals
    unfold atom_occurs_in
    infer_instance


/--
  `Formula_.atom_set F` := The set of all of the atoms that have an occurrence in the formula `F`.
-/
def Formula_.atom_set :
  Formula_ → Finset String
  | false_ => ∅
  | true_ => ∅
  | atom_ X => {X}
  | not_ phi => phi.atom_set
  | and_ phi psi => phi.atom_set ∪ psi.atom_set
  | or_ phi psi => phi.atom_set ∪ psi.atom_set
  | imp_ phi psi => phi.atom_set ∪ psi.atom_set
  | iff_ phi psi => phi.atom_set ∪ psi.atom_set


/--
  `replace_atom_one_rec A F P` :=

  `A → F` in `P` for each occurrence of the atom `A` in the formula `P`

  The result of simultaneously replacing each occurrence of the atom `A` in the formula `P` by an occurrence of the formula `F`.
-/
def replace_atom_one_rec
  (A : String)
  (F : Formula_ ) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => if A = X then F else atom_ X
  | not_ phi => not_ (replace_atom_one_rec A F phi)
  | and_ phi psi => and_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | or_ phi psi => or_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | imp_ phi psi => imp_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)
  | iff_ phi psi => iff_ (replace_atom_one_rec A F phi) (replace_atom_one_rec A F psi)


/--
  `replace_atom_all_rec τ F` := The simultaneous replacement of each occurrence of any atom `A` in the formula `F` by `τ A`.
-/
def replace_atom_all_rec
  (τ : String → Formula_) :
  Formula_ → Formula_
  | false_ => false_
  | true_ => true_
  | atom_ X => τ X
  | not_ phi => not_ (replace_atom_all_rec τ phi)
  | and_ phi psi => and_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | or_ phi psi => or_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | imp_ phi psi => imp_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)
  | iff_ phi psi => iff_ (replace_atom_all_rec τ phi) (replace_atom_all_rec τ psi)


structure Equation : Type where
  (lhs : Formula_)
  (rhs : Formula_)
  deriving Inhabited, DecidableEq, Repr


def var_elim
  (X : String)
  (F : Formula_)
  (L : List Equation) :
  List Equation :=
  L.map (fun (E : Equation) => ⟨replace_atom_one_rec X F E.lhs, replace_atom_one_rec X F E.rhs⟩)


def equation_list_atom_set
  (L : List Equation) :
  Finset String :=
    List.foldr (fun (next : Equation) (prev : Finset String) => next.lhs.atom_set ∪ next.rhs.atom_set ∪ prev) {} L

#eval equation_list_atom_set {}
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩]
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "Q", atom_ "R"⟩]
#eval equation_list_atom_set [⟨atom_ "P", atom_ "Q"⟩, ⟨atom_ "R", atom_ "S"⟩]


def equation_list_size
  (L : List Equation) :
  Nat :=
  List.foldr (fun (next : Equation) (prev : Nat) => next.lhs.size + next.rhs.size + prev) 0 L


def unify :
  List Equation → Option (String → Formula_)
  | [] => Option.some atom_
  | ⟨false_, false_⟩ :: Γ
  | ⟨true_, true_⟩ :: Γ => unify Γ
  | ⟨atom_ X, F⟩ :: Γ
  | ⟨F, atom_ X⟩ :: Γ =>
    if atom_ X = F
    then unify Γ
    else
      if atom_occurs_in X F
      then Option.none
      else
        match unify (var_elim X F Γ) with
        | Option.none => Option.none
        | Option.some τ => Option.some (Function.updateITE τ X (replace_atom_all_rec τ F))
  | ⟨not_ phi, not_ phi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: Γ)
  | ⟨and_ phi psi, and_ phi' psi'⟩ :: Γ
  | ⟨or_ phi psi, or_ phi' psi'⟩ :: Γ
  | ⟨imp_ phi psi, imp_ phi' psi'⟩ :: Γ
  | ⟨iff_ phi psi, iff_ phi' psi'⟩ :: Γ =>
      unify (⟨phi, phi'⟩ :: ⟨psi, psi'⟩ :: Γ)
  | _ => Option.none
  termination_by L => ((equation_list_atom_set L).card, equation_list_size L)
  decreasing_by
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.left
    sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.left
    sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry
  · apply Prod.Lex.right'
    all_goals sorry

[Paige Thomas]

Thank you! I'm working my way through the proof.