tactic for partial orders

Stream: mathlib4

[Vasilii Nesterov]

Would it be useful to have a tactic in Mathlib that can solve goals in partial order theory? It is easy to implement, and I'd like to create one to practice metaprogramming.

[Kim Morrison]

What goals would this tactic solve?

[Vasilii Nesterov]

Those that can be closed by applying reflexivity, transitivity, or antisymmetry to local hypotheses and the goal. It would also use the linearity of the order when applicable.

In both cases (partial order and linear order), the quantifier-free theory is decidable in linear time.

[Kevin Buzzard]

Is it this ?

[Vasilii Nesterov]

Hmm, I'm not sure if an aesop-based approach is the best here because it searches for the proof using tree search by guessing proof steps, whereas in this case, it can be done without guessing.

By the way, it's easy to add support for lattices in the tactic I have in mind.

[Bhavik Mehta]

Heather and I have discussed this a bit - I agree this would be nice to have. For the tactic you have in mind, would it be able to prove that a <= b <= c <= d <= e and b != d implies a != e in a partial order?

[Peter Nelson]

It would be nice to have something work for lattices, as well, even if it is just as simple as adding all the trivial inequalities that come from le_sup_iff, sup_le_iff, le_sup_left, le_sup_right and similar for inf.

[Bhavik Mehta]

(The thread that Kevin links to does this, but I think Vasily's idea would perform better than the aesop approach. It might work to just preprocess like nlinarith does to add all those inequalities, then running the partial/linear order version)

[Vasilii Nesterov]

Bhavik Mehta said:

Heather and I have discussed this a bit - I agree this would be nice to have. For the tactic you have in mind, would it be able to prove that a <= b <= c <= d <= e and b != d implies a != e in a partial order?

Thank you for this example! Everything turned out to be more complicated than I initially thought. Anyway, it seems that the problem can be solved in quadratic time (not linear as I promised).

Let me describe my algorithm for partial orders.

1. First, we negate the goal, so our new goal is to prove False.
2. We collect all facts in the form of x = y, x ≤ y, x < y, x ≠ y, ¬(x ≤ y), and ¬(x < y) from the context. Here, we split conjunctions. Splitting disjunctions would result in exponential blow-up, and I guess we can't do anything smart about it here. However, there should be an option to enable this splitting if needed.
3. We replace each fact of the form x < y with two equivalent facts: x ≤ y and x ≠ y.
4. We replace each fact of the form ¬(x ≤ y) with two equivalent facts: ¬(x < y) and x ≠ y.

5. We define the ≤-graph as a directed graph whose vertices are variables and whose edges correspond to facts of the form x ≤ y. Similarly, we define (undirected) =-graph.
   We then find all connected components in =-graph. Variables within the same component are be provably equal. Thus, we can "compress" them into a single vertex. During this process, we check that no fact of the form x ≠ y leads to a contradiction — otherwise, we have found a contradiction, and the goal is accomplished. After this step, we may assume that the remaining facts are in one of three forms: x ≤ y, x ≠ y, and ¬(x < y).

6. We identify all (directed) cycles in the ≤-graph. All variables within such a cycle must be equal, so we perform compression as before. After this step, we can assume that the ≤-graph is acyclic.

7. For each fact of the form ¬(x < y), we check whether y is reachable from x in the ≤-graph. If it is, then x ≤ y, which implies x = y, allowing us to compress the graph further.

At each step, we replace our set of facts with an equisatisfiable one. If no contradiction is found by the end, then there exists a model satisfying the final set of facts: one can use the set of variables with x R y holds iff y is reachable from x in the ≤-graph. In this case, it is impossible to derive a contradiction from the theory of partial orders.

[Vasilii Nesterov]

In your example, after negation, we would have a ≤ b ≤ c ≤ d ≤ e, b ≠ d, and a = e. After step 5, a and e would be compressed into a single variable, say s. Then, in step 6, we would detect the cycle s ≤ b ≤ c ≤ d ≤ s, and compressing it would lead to a contradiction with b ≠ d.

[Bhavik Mehta]

Nice, I can see this working! Indeed the reason I shared that example is that we'd also come up with the "do search in the directed graph on ≤" approach, but I didn't get time to think about how to make this example work (ie I just had a preorder tactic), I'm glad to hear it helped you figure out your algorithm!

[Vasilii Nesterov]

Here is the PR: #21877.

[Vasilii Nesterov]

While coding I simplified the algorithm and also added a Preorder version.

[Jireh Loreaux]

feature request:

order [h1, h2, h3]

Allow the user to supply inequalities.

[Bhavik Mehta]

Second feature request (which can and maybe should be a secondary PR to make this one easier to review): a preprocessing step which runs the lemmas that Peter mentions first, and then does order. I don't think this will be complete for lattices, but it could be convenient nonetheless (similar to how linarith is complete for linear arithmetic and nlinarith is not complete for nonlinear arithmetic, but it's still sometimes pretty useful!)

[Vasilii Nesterov]

Yes, I plan to do this in the next PR.

[Vasilii Nesterov]

I extended the tactic to Lattice (#21966), and it seems to be complete for them as well. I wonder if it would be useful to make it complete for DistribLattice. In any case, it seems to be an interesting and nontrivial task (maybe I should use the M3-N5 theorem somehow).

Btw, the cases of HeytingAlgebra and BooleanAlgebra can be handled by reducing them to intuitionistic or classical logic and then calling itauto or tauto :upside_down: .

[Yaël Dillies]

Vasily Nesterov said:

Btw, the cases of HeytingAlgebra and BooleanAlgebra can be handled by reducing them to intuitionistic or classical logic and then calling itauto or tauto :upside_down: .

This was one of the motivations for getting the theory of Heyting algebras off the ground: to get to write a cool tactic :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Vasilii Nesterov said:

I extended the tactic to Lattice (#21966), and it seems to be complete for them as well.

I just discovered a simple example showing that it isn't complete for LinearOrder at least:

import Mathlib

example {α : Type*} [LinearOrder α] {a b c : α} (hab : a < b)
    (habc : min a b ≤ c) (hcba : min c b ≤ a) : a = c := by
  order -- No contradiction found
  exact le_antisymm (by simpa [hab.le] using habc) (by simpa [hab.not_le] using hcba)

The issue seems to be that order doesn't know about docs#inf_le_iff

[Yaël Dillies]

How I came across this example: This is showing that $v(a) = v(a + b)$ if $v(a) < v(b)$ where $v$ is a valuation

[Edward van de Meent]

this doesn't mean that it's not complete for Lattice, right?

[Edward van de Meent]

(just checking my understanding)

[Jovan Gerbscheid]

Should the plan be to make the tactic complete for LinearOrder, by doing some form of case splitting, like in omega? Or just to let the tactic use the lemma min a b < b → a < b whenever it already knows min a b < b?

[Vasilii Nesterov]

Yes, this tactic is complete for both LinearOrder without lattice operations and for Lattice without assuming linearity.

It seems the problem for linear orders with lattice operations is NP-hard. We can model 3SAT problem like this: add a hypothesis f < t, for each variable x require x₀ ⊓ x₁ ≤ f and x₀ ⊔ x₁ ≥ t and then for a clause x ∨ ¬ y ∨ z require x₁ ⊔ y₀ ⊔ z₁ ≥ t.

[Vasilii Nesterov]

I'd like to solve the case of linear orders by translating the problem from an arbitrary type to Nat, and then running omega. This would save us from having to reimplement all the heuristics needed to make the procedure efficient. I wonder how hard it is to use such an approach.

[Jovan Gerbscheid]

That is a good idea. Although it's probably worth waiting until grind is ready, and then using it instead of omega.

[Yaël Dillies]

Vasilii Nesterov said:

solve the case of linear orders by translating the problem from an arbitrary type to Nat, and then running omega

That's a very interesting idea. How would it work, mathematically? It feels like you're claiming something model-theoretic about linear orders and ℕ. Something like ℕ is a "generic" model of the quantifier-free theory of linear orders? If so, is your idea to turn a proof of this fact into an effective algorithm?

[Jovan Gerbscheid]

One way it could be done (I'm not sure if there is any other way) is to use the same ideas as in to_additive (or to_dual). We could make a tag to_linear, which turns all relevant statements about ℕ or ℤ into the equivalent statements about an arbitrary linear order α. Then using the to_linear machinery, we can transform the obtained proof about ℕ or ℤ into a proof about the given linear order.

Or we can hope that grind will work directly on a LinearOrder.

[Yaël Dillies]

Okay, but for example m + 1 ≤ n ↔ m < n has no analogue in an arbitrary linear order, so not all(/very few) proofs generated by omega/grind will translate to a general linear order

[Yaël Dillies]

You need some kind of encoding of the variables in your problem and their min/max as natural numbers

[Edward van de Meent]

Yaël Dillies said:

Vasilii Nesterov said:

solve the case of linear orders by translating the problem from an arbitrary type to Nat, and then running omega

That's a very interesting idea. How would it work, mathematically? It feels like you're claiming something model-theoretic about linear orders and ℕ. Something like ℕ is a "generic" model of the quantifier-free theory of linear orders? If so, is your idea to turn a proof of this fact into an effective algorithm?

i think the idea is that any first-order statement in the theory of linear orders is true iff there are no counterexamples, which are finite, so must have an equivalent in the natural numbers. As a result, it suffices to check that the natural numbers don't contain a counterexample?

[Edward van de Meent]

although you might need the integers instead

[Edward van de Meent]

because of statements like (∀ a, ∃ b, b < a) → False

[Aaron Liu]

I thought we were working quantifier-free?

[Edward van de Meent]

ah right, that's fair

[Edward van de Meent]

model theory was some time ago

[Edward van de Meent]

in that case indeed Nat is sufficient

[Yaël Dillies]

Edward van de Meent said:

i think the idea is that any first-order statement in the theory of linear orders is true iff there are no counterexamples, which are finite, so must have an equivalent in the natural numbers. As a result, it suffices to check that the natural numbers don't contain a counterexample?

That is indeed the idea, but I am not sure how to prove "effectively".

[Jovan Gerbscheid]

Does Mathlib have some sort of model theory? I think it should be possible to

• define the language of lattices
• define the evaluation of statements in this language inside a given order
• define what a model is
• prove that a model in an arbitrary LinearOrder gives a model in Nat.

Then we use grind/omega to prove that there is no model in Nat, so we conclude there is no model in the given LinearOrder.

[Aaron Liu]

We have file#ModelTheory/Order

[Yaël Dillies]

The model-theoretic language is useful, but I doubt we actually need to prove the model-theoretic statement to implement the tactic. The model theoretic statement is more like a metatheorem that guides tactic-writing.

[Jovan Gerbscheid]

I'm not sure how the tactic would prove this without using the model theoretic theorem.

[Vasilii Nesterov]

Yes, by translation from an arbitrary type to ℕ, I mean interpreting all order operations (<, ≤, ⊓, ⊔) in terms of natural numbers. Any finite linearly ordered set can be embedded into the natural numbers in a way that preserves the order, so this is mathematically correct: if some linearly ordered set satisfies a set of conditions S, then its "ℕ-version" will also satisfy S. Conversely, if S can be satisfied in ℕ, then it is impossible to derive a contradiction from S using only order axioms.

On the implementation side, I had the following idea. We need a lemma stating that for any "valuation" in our type α, we can map α to ℕ in a way that preserves the order on the image of this valuation, like so:

import Mathlib

theorem exists_translation {α : Type*} [LinearOrder α] (val : ℕ → α) : ∃ f : ℕ → ℕ,
    (∀ i j, val i ≤ val j ↔ f i ≤ f j) ∧
    (∀ i j, val i < val j ↔ f i < f j)
    -- maybe more conditions?
    := by sorry

Then we take some val such that val 0, val 1, ... is equal to variables in the context. And using such an f, we can rewrite all hypotheses in the context and run omega.

[Aaron Liu]

You should have val : Fin n → α since this version is not provable.

[Vasilii Nesterov]

Yaël Dillies said:

Okay, but for example m + 1 ≤ n ↔ m < n has no analogue in an arbitrary linear order, so not all(/very few) proofs generated by omega/grind will translate to a general linear order

This is true, but this involves arithmetic. For theories with arithmetic Nat is not a "universal" (I don't remember the right model-theoretic term) model, but it's sufficient for the order theory. Maybe we should use something else and preserve some arithmetic as well.

[Vasilii Nesterov]

Aaron Liu said:

You should have val : Fin n → α since this version is not provable.

Yes, indeed. val 0 > val 1 > val 2 > ... is a counterexample. Maybe we can just use ℤ intead of ℕ here? Fin n is enough though

Edit: no, ℤ doesn't work, val 0 > val 1 > val 2 > ... > 0 is a counterexample :)

[Yaël Dillies]

Jovan Gerbscheid said:

I'm not sure how the tactic would prove this without using the model theoretic theorem.

My hope is that the model-theoretic theorem has an effective proof, and that this proof is the algorithm the tactic should follow.

[Jovan Gerbscheid]

I think the proof of the model-theoretic theorem uses case-splits. So if you were to replay this proof in the tactic, you would be doing too much work (and probably not need to call grind/omega anymore)

[Aaron Liu]

Yaël Dillies said:

Jovan Gerbscheid said:

I'm not sure how the tactic would prove this without using the model theoretic theorem.

My hope is that the model-theoretic theorem has an effective proof, and that this proof is the algorithm the tactic should follow.

I think all you get is a reduction from finite subsets of α to ℕ, not sure how you would extract an algorithm from that.

[Jovan Gerbscheid]

The exists_translation theorem (with val : Fin n → α) captures the essence of the model theoretic statement. The question is whether we want/need to use the model theory to prove it.

[Aaron Liu]

Why would we need model theory? We can just induct on n.

[Jovan Gerbscheid]

At some point I wrote a way to construct efficient Exprs of type ℕ → α (or Fin n → α), using a binary tree. This can be used to construct the val:

Code

import Qq

universe u

inductive BinTree (α : Type u) where
| leaf : α → BinTree α
| node : Nat → BinTree α → BinTree α → BinTree α

namespace BinTree

variable {α : Type u}

def get (tree : BinTree α) (n : Nat) : α :=
  match tree with
  | leaf a => a
  | node m l r => if n < m then l.get n else r.get n

open Lean Qq

def mkExpr {u : Level} {α : Q(Type $u)} (atoms : Array Q($α)) : Q(BinTree $α) :=
  if _ : atoms.size = 0 then
    panic! "empty array"
  else
    go 0 atoms.size
where
  go (lo hi : Nat) (h_lo : lo < hi := by omega) (h_hi : hi ≤ atoms.size := by omega) : Q(BinTree $α) :=
    let mid := (lo + hi)/2
    if h : lo = mid then
      q(leaf $(atoms[lo]))
    else
      let l := go lo mid
      let r := go mid hi
      let n : Q(Nat) := mkNatLit mid
      q(node $n $l $r)
  termination_by hi - lo

def mkFun {u : Level} {α : Q(Type $u)} (atoms : Array Q($α)) : Q(Nat → $α) :=
  let tree := BinTree.mkExpr atoms
  q(($tree).get)

[Aaron Liu]

I've got a working proof of exists_translation, with some nice properties.

Here it is

import Mathlib.Data.Set.Finite.Basic

def translation {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) (k : Fin n) : ℕ :=
  (Finset.image val {u : Fin n | val u < val k}).card

theorem translation_le_translation {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) :
    ∀ i j, translation val i ≤ translation val j ↔ val i ≤ val j := by
  intro i j
  have hi := Finset.mem_univ i
  have hj := Finset.mem_univ j
  generalize @Finset.univ (Fin n) _ = s at hi hj
  induction s using Finset.strongInduction with | _ s ih =>
  have hs : s.Nonempty := ⟨i, hi⟩
  obtain ⟨m, hms, hm⟩ := Set.Finite.exists_maximal_wrt val s s.finite_toSet hs.to_set
  rw [Finset.mem_coe] at hms
  let t : Finset (Fin n) := {u ∈ s | val u < val m}
  have ht : t ⊂ s := by
    rw [Finset.ssubset_def]
    constructor
    · apply Finset.filter_subset
    · intro hst
      apply lt_irrefl (val m)
      exact (Finset.mem_filter.mp (hst hms)).right
  have hmm (k : Fin n) (hk : k ∈ s) : val k ≤ val m :=
    (le_total (val k) (val m)).elim id fun h => by rw [hm k hk h]
  obtain him | him := lt_or_eq_of_le (hmm i hi) <;> obtain hjm | hjm := lt_or_eq_of_le (hmm j hj)
  · exact ih t ht (Finset.mem_filter.mpr ⟨hi, him⟩) (Finset.mem_filter.mpr ⟨hj, hjm⟩)
  · rw [hjm, iff_true_right him.le]
    apply Finset.card_le_card
    apply Finset.image_subset_image
    apply Finset.monotone_filter_right
    intro u hu
    rw [hjm]
    exact hu.trans him
  · rw [him, iff_false_right hjm.not_le, not_le]
    apply Finset.card_lt_card
    rw [him, Finset.ssubset_def]
    constructor
    · apply Finset.image_subset_image
      apply Finset.monotone_filter_right
      intro u hu
      exact hu.trans hjm
    · intro hii
      have hjj :=
        hii (Finset.mem_image.mpr ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ j, hjm⟩, rfl⟩)
      rw [Finset.mem_image] at hjj
      obtain ⟨k, hk, hkj⟩ := hjj
      rw [Finset.mem_filter] at hk
      rw [hkj] at hk
      exact hk.right.false
  · rw [him, hjm, iff_true_right le_rfl, translation, him, translation, hjm]

theorem translation_lt_translation {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) :
    ∀ i j, translation val i < translation val j ↔ val i < val j := by
  intro i j
  simpa using (translation_le_translation val j i).not

theorem translation_eq_translation {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) :
    ∀ i j, translation val i = translation val j ↔ val i = val j := by
  simp_rw [le_antisymm_iff, translation_le_translation, implies_true]

theorem translation_injective {α : Type*} [LinearOrder α] {n : ℕ} {val : Fin n → α}
    (inj : Function.Injective val) : Function.Injective (translation val) := by
  intro i j hij
  rw [translation_eq_translation] at hij
  exact inj hij

[Vasilii Nesterov]

Very nice! Would you like to write a tactic that uses this? I'd like to do this too, but I'm not that fast :)

[Aaron Liu]

What's the spec of this tactic? Gather up all the linear order hypotheses and convert them into ℕ?

[Cameron Zwarich]

Edward van de Meent said:

i think the idea is that any first-order statement in the theory of linear orders is true iff there are no counterexamples, which are finite, so must have an equivalent in the natural numbers. As a result, it suffices to check that the natural numbers don't contain a counterexample?

[probably my fault for not realizing this discussion was in the pure QF context]
A counterexample doesn't necessarily have a finite model. For example, the sentence "there is a least element and a greatest element" has no counterexamples in finite linear orders, but the rationals are a counterexample.

It will probably be much simpler to make a decision procedure for dense linear orders (whose theory has quantifier elimination, with a fairly elementary proof) or the quantifier-free theory of linear orders. The decidability of the theory of all linear orders is usually established by more sophisticated techniques. In practice, I suspect that any decision procedure would need to generate explicit proof terms (possibly using small pockets of proof-by-reflection to compress the proofs) rather than using Mathlib's development of model theory to prove a decision procedure correct outright, because even if the proof effort succeeded, the resulting procedure would run too slowly in Lean's kernel to be useful.

[Aaron Liu]

I think we were focusing on the quantifier-free case

[Vasilii Nesterov]

Aaron Liu said:

What's the spec of this tactic? Gather up all the linear order hypotheses and convert them into ℕ?

Yes, I meant this

[Vasilii Nesterov]

Cameron Zwarich said:

Edward van de Meent said:

i think the idea is that any first-order statement in the theory of linear orders is true iff there are no counterexamples, which are finite, so must have an equivalent in the natural numbers. As a result, it suffices to check that the natural numbers don't contain a counterexample?

A counterexample doesn't necessarily have a finite model. For example, the sentence "there is a least element and a greatest element" has no counterexamples in finite linear orders, but the rationals are a counterexample.

It will probably be much simpler to make a decision procedure for dense linear orders (whose theory has quantifier elimination, with a fairly elementary proof) or the quantifier-free theory of linear orders. The decidability of the theory of all linear orders is usually established by more sophisticated techniques. In practice, I suspect that any decision procedure would need to generate explicit proof terms (possibly using small pockets of proof-by-reflection to compress the proofs) rather than using Mathlib's development of model theory to prove a decision procedure correct outright, because even if the proof effort succeeded, the resulting procedure would run too slowly in Lean's kernel to be useful.

I’ve thought about dense linear orders as well. The problem is that quantifier elimination doesn’t seem very useful in practice and also leads to exponential blow-up.

[Vasilii Nesterov]

Aaron Liu said:

What's the spec of this tactic? Gather up all the linear order hypotheses and convert them into ℕ?

Perhaps it should use order internals to collect variables and facts about them from the context.

[Aaron Liu]

Vasilii Nesterov said:

Aaron Liu said:

What's the spec of this tactic? Gather up all the linear order hypotheses and convert them into ℕ?

Yes, I meant this

what should I call it

[Vasilii Nesterov]

In fact, I think it should be a part of the order tactic. I suggest starting from #21966. You can write a function

def translateToNat (type : Expr) (idxToAtom : Std.HashMap ℕ Expr) (facts : Array AtomicFact) :
    MetaM <| Std.HashMap ℕ Expr × Array AtomicFact :=
  sorry

where type is the original type, idxToAtom maps indexes to variables and facts contains facts about these variables extracted from the context. The function returns new (idxToAtom, facts) about Nats. I believe it's enough to write a lemma for each type of AtomicFact and then just rewrite each fact using the corresponding lemma.

[Vasilii Nesterov]

I'm not sure what we should do with facts of the form x = ⊤. In the order, I replace such facts with new ones of the form y ≤ x for all atoms y. We can apply the same preprocessing here, so you can assume that there are no facts of this type in translateToNat.

[Aaron Liu]

Are all the variables of the same type?

[Vasilii Nesterov]

Yes

[Aaron Liu]

Do I just push to branch#vasnesterov/order_tactic_lattices

[Aaron Liu]

or a new branch

[Vasilii Nesterov]

New, please

[Vasilii Nesterov]

I hope this one will be reviewed and merged soon (it's quite old already)

[Cameron Zwarich]

Vasilii Nesterov said:

I’ve thought about dense linear orders as well. The problem is that quantifier elimination doesn’t seem very useful in practice and also leads to exponential blow-up.

While in general the DEXPTIME nature of most QE procedures seems limiting, I have a suspicion (which might be a misconception on my part) that they could be made practical for Mathlib-sized problems. Maybe I should do some experiments and see how efficient I can make it. If it’s going to work out anywhere, it will be DLO.

[Aaron Liu]

Vasilii Nesterov said:

In fact, I think it should be a part of the order tactic. I suggest starting from #21966. You can write a function

def translateToNat (type : Expr) (idxToAtom : Std.HashMap ℕ Expr) (facts : Array AtomicFact) :
    Std.HashMap ℕ Expr × Array AtomicFact :=
  sorry

where type is the original type, idxToAtom maps indexes to variables and facts contains facts about these variables extracted from the context. The function returns new (idxToAtom, facts) about Nats. I believe it's enough to write a lemma for each type of AtomicFact and then just rewrite each fact using the corresponding lemma.

What do I do with facts of type .isSup and .isInf?

[Vasilii Nesterov]

I guess, rewrite with something like

theorem translation_inf {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) (i j k : Fin n) :
    translation val i = translation val j ⊓ translation val k ↔ val i = val j ⊓ val k := by sorry

[Aaron Liu]

But they don't carry around a proof

[Aaron Liu]

I could modify them to carry around a proof, but then I don't know what would break, and it might take a few hours to debug.

[Vasilii Nesterov]

Yes, for isSup and isInf the proof is always rfl

[Aaron Liu]

But for the translation the proof isn't rfl anymore so it gets complicated

[Aaron Liu]

or, I could try to special-case them but then I would need to do something different on the < and ≤

[Aaron Liu]

I could also just double all the sup and inf and add a lot of .eq

[Vasilii Nesterov]

Yes, I think isSup i j k which states xk := xi ⊔ xj should become aux := ni ⊔ nj plus a new fact nk = aux

[Aaron Liu]

Vasilii Nesterov said:

Yes, I think isSup i j k which states xk := xi ⊔ xj should become aux := ni ⊔ nj plus a new fact nk = aux

How do I generate a new index for aux?

[Vasilii Nesterov]

At first you can map existing variables, like idxToAtomNew[i] = translation val i (q($translation $val $i) using Qq). Then when you face a fact .isSup i j k you add a new atom idxToAtomNew[newIdx] = translation val i ⊔ translation val j (where newIdx = idxToAtomNew.size) and two facts: .isSup i j newIdx and .eq k newIdx. For the latter you need to prove exactly that translation val k = translation val i ⊔ translation val j, and here you use your lemma. Does this work?

[Aaron Liu]

I have this function translateToNat, now what do I do with it?

[Aaron Liu]

I'm also not entirely sure that it works correctly