tactic for "apply in some order"

Stream: new members

[Chris M]

Is there a tactic that allows me to just say: "apply these 3 terms/lemmas in whichever order is needed to prove the result"?

[Alex J. Best]

solve_by_elim might work:

variables {A B C :Prop}

lemma f : A → C := sorry
lemma g : C → B := sorry

example (h : A) : C :=
begin
  solve_by_elim [f, g],
end

[Chris M]

This is motivated by this massively long proof:

import order.lattice
import tactic

variables {α : Type*} [lattice α]
variables x y z : α

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm,
    {
        apply le_inf,
        calc
            (x ⊓ y) ⊓ z  ≤ (x ⊓ y)     : inf_le_left
                        ... ≤  x        : inf_le_left,
        apply le_inf,
        calc
            (x ⊓ y) ⊓ z  ≤ (x ⊓ y)     : inf_le_left
                        ... ≤  y        : inf_le_right,
        calc
            (x ⊓ y) ⊓ z  ≤ z             : inf_le_right
    },
    {
        apply le_inf,
        apply le_inf,
        calc
            x ⊓ (y ⊓ z)  ≤ x     : inf_le_left,
        calc
            x ⊓ (y ⊓ z)  ≤ (y ⊓ z)     : inf_le_right
                        ... ≤  y        : inf_le_left,
        calc
            x ⊓ (y ⊓ z)  ≤ (y ⊓ z)     : inf_le_right
                        ... ≤  z        : inf_le_right
    }
end

Where I want to just say something like:

apply le_antisymm,
repeat {use [inf_le_right, inf_le_left, le_inf]}

[Chris M]

@Alex J. Best The following doesn't work:

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm,
    repeat
    {
        solve_by_elim [inf_le_right, inf_le_left, le_inf]
    }
end

It doesn't improve the goal state.

[Alex J. Best]

(deleted)

[Kenny Lau]

this is like Coq Ltac

[Kenny Lau]

if you rewrite inf_assoc then you have already cleared the goal lol

[Alex J. Best]

oh lol!

[Kenny Lau]

the point is to prove inf_assoc

[Kenny Lau]

using inf_le_left etc

[Kenny Lau]

@Mario Carneiro do you know Coq Ltac?

[Kenny Lau]

they can say things like, "if the goal looks like foo, then apply bar"

[Kenny Lau]

I've been wanting to ask about this

[Mario Carneiro]

you can do that in non-interactive tactics

[Mario Carneiro]

you can also write non-interactive tactics inside a begin-end block if it's not reusable

[Kenny Lau]

but do we have that functionality currently?

[Chris M]

what are non-interactive tactics?

[Kenny Lau]

Ltac perm_aux n :=
  match goal with
  | |- (perm _ ?l ?l) => apply perm_refl
  | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
     let newn := eval compute in (length l1) in
         (apply perm_cons; perm_aux newn)
  | |- (perm ?A (?a :: ?l1) ?l2) =>
     match eval compute in n with
     | 1 => fail
     | _ =>
         let l1' := constr:(l1 ++ a :: nil) in
         (apply (perm_trans A (a :: l1) l1' l2);
         [ apply perm_append | compute; perm_aux (pred n) ])
     end
  end.

[Kenny Lau]

^ an example of Ltac match goal with

[Kenny Lau]

so we can build tactics that apply inf_le_left and le_inf

[Kenny Lau]

like a custom solver for lattice equations

[Mario Carneiro]

private meta def infs :=
`[refl <|> {apply inf_le_left_of_le, infs} <|> {apply inf_le_right_of_le, infs}]
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by apply le_antisymm; repeat {apply le_inf}; {infs}

[Chris M]

@Mario Carneiro Did you define infs specifically for this purpose?

[Mario Carneiro]

yes

[Chris M]

does <|> mean "try either the left or right hand side, whichever works"?

[Kenny Lau]

the left hand side first

[Mario Carneiro]

The only reason it is not literally in the begin-end block of the theorem is because it's recursive and that's annoying to write without a global definition

[Mario Carneiro]

I think that these kind of "light weight custom tactics" are underrated in proof scripts

[Kenny Lau]

import order.lattice

meta def infs :=
`[refl <|> {apply inf_le_left_of_le, infs} <|> {apply inf_le_right_of_le, infs}]

meta def tactic.interactive.lattice :=
`[apply le_antisymm; repeat { apply le_inf }; infs]

variables {L : Type*} [lattice L] {x y z : L}

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by lattice

example : x ⊓ y = y ⊓ x :=
by lattice

[Kenny Lau]

import order.lattice

meta def infs_and_sups :=
`[refl <|> {apply inf_le_left_of_le, infs_and_sups} <|> {apply inf_le_right_of_le, infs_and_sups} <|>
  {apply le_sup_left_of_le, infs_and_sups} <|> {apply le_sup_right_of_le, infs_and_sups}]

meta def tactic.interactive.lattice :=
`[try { apply le_antisymm }; repeat { apply le_inf <|> apply sup_le }; infs_and_sups]

variables {L : Type*} [lattice L] {a b c x y z : L}

example : a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c) :=
by lattice

example : a ⊔ (a ⊓ b) = a :=
by lattice

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by lattice

example : x ⊓ y = y ⊓ x :=
by lattice

[Mario Carneiro]

I think you just wrote a prover for intuitionistic logic

[Kenny Lau]

oh right they're the same as lattices

[Kenny Lau]

where's my complement

[Mario Carneiro]

heyting lattices to be precise

[Chris M]

@Kenny Lau , did you just write the lattice tactic for the first time, or is it already part of the library?

[Kenny Lau]

for the first time

[Chris M]

nice

[Mario Carneiro]

generally speaking if it appears in a code block on zulip it was just written

[Mario Carneiro]

the procedure is pretty simple: split on everything and apply all assumptions

[Scott Morrison]

solve_by_elim is good at this, although note that its default max_depth is very low (3!)

[Scott Morrison]

import order.lattice

meta def tactic.interactive.lattice :=
`[solve_by_elim
  [le_antisymm, le_inf, sup_le, le_refl, inf_le_left_of_le, inf_le_right_of_le,
    le_sup_left_of_le, le_sup_right_of_le]
  {max_depth := 30}]

variables {L : Type*} [lattice L] {a b c x y z : L}

example : a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c) :=
by lattice

example : a ⊔ (a ⊓ b) = a :=
by lattice

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by lattice

example : x ⊓ y = y ⊓ x :=
by lattice

[Scott Morrison]

(In this case, because of the shape of the lemmas, there's no danger setting a high max_depth; it would be fine probably to set it to 1000.)

[Scott Morrison]

I'm not claiming that this is superior to Kenny's hand-rolled tactic; just that this sort of machinery is available "out of the box" as well.

[Chris M]

Mario Carneiro said:

private meta def infs :=
`[refl <|> {apply inf_le_left_of_le, infs} <|> {apply inf_le_right_of_le, infs}]
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by apply le_antisymm; repeat {apply le_inf}; {infs}

I am confused as to why the following doesn't work:

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm;
    {repeat {apply le_inf};
    repeat {refl <|> {apply inf_le_left_of_le} <|> {apply inf_le_right_of_le}}}
end

I would have guessed that this is equivalent to your solution using infs.

[Kenny Lau]

because infs allows for tree-like search while your translation can only apply one tactic at a time

[Chris M]

Ah I see it now, thanks :)

[Chris M]

So a followup question:
In this code by @Mario Carneiro, we use inf_le_left_of_le instead of inf_le_left as I do in the original calc proof:

private meta def infs :=
`[refl <|> {apply inf_le_left_of_le, infs} <|> {apply inf_le_right_of_le, infs}]
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by apply le_antisymm; repeat {apply le_inf}; {infs}

I understand this is because calc has its own implicit use of le_trans and similar terms, and hence we can't just write

private meta def infs :=
`[refl <|> {apply inf_le_left, infs} <|> {apply inf_le_right, infs}]

However, it would be nice if we can somehow define infs instead to say something like "use inf_le_left and inf_le_right and make a calc proof from them using the appropriate transitivity terms", without either having to know the names of those transitivity terms or the name inf_le_left_of_le. Is this possible?

[Mario Carneiro]

It is possible to change the tactic to use le_trans and inf_le_left instead of inf_le_left_of_le, but general proof search using le_trans is messy because it has an undetermined middle variable

[Mario Carneiro]

private meta def infs :=
`[refl <|> {transitivity, apply inf_le_left, infs} <|> {transitivity, apply inf_le_right, infs}]
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by apply le_antisymm; repeat {apply le_inf}; {infs}