How to work with clauses efficiently

Stream: metaprogramming / tactics

[Daniel Weber]

I want to work with clauses, disjunctions of literals, and I'm not sure how to do this. Concretely, here are a few things I'm unsure about:

• Given a proof of (a ∨ b ∨ c) ∨ (d ∨ e ∨ f), what's the best way to get a proof of a ∨ b ∨ c ∨ d ∨ e ∨ f, and vice versa (that is, use associativity)?
• Given a proof of a ∨ b ∨ c ∨ d, what's the best way to get a proof of c ∨ a ∨ d ∨ b (or any other permutation)?

I need this for https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1076.20!.3D.3E.203, where it will probably run tens of thousands of times, so efficiency is quite important

[Kyle Miller]

How big of clauses are you going to work with? One idea is to precompute a number of these lemmas if it's feasible.

[Daniel Weber]

Around 9 literals. I think it'd be feasible for associativity, but not for permutations. There could be lemmas for swapping every pair, and then I could find the swaps representing the permutation

[Daniel Weber]

Would using swaps be better than using a bunch of docs#Or.elim, docs#Or.inr, docs#Or.inl ?

[Timo Carlin-Burns]

does ac_rfl help?

example : ((a ∨ b ∨ c) ∨ (d ∨ e ∨ f)) = (a ∨ b ∨ c ∨ d ∨ e ∨ f) := by
  ac_rfl

[Daniel Weber]

I don't think it'd be efficient enough, but I could try to start with it, thanks

[Daniel Weber]

Does it have an ac_exact variant?

[Damiano Testa]

Also, calling simp with or_comm, or_assoc, or_left_comm should prove reorderings.

[Damiano Testa]

(That is how move_add works internally and it can be configured to work with and/or.)

[Timo Carlin-Burns]

I don't think there's an ac_exact variant but here's a naive implementation

macro "ac_exact" e:term : tactic => `(tactic| exact cast (by ac_rfl) $e)

example (h : (a ∨ b ∨ c) ∨ (d ∨ e ∨ f)) : a ∨ b ∨ c ∨ d ∨ e ∨ f := by
  ac_exact h