Zulip Chat Archive

Stream: new members

Topic: tactic for "apply in some order"


view this post on Zulip Chris M (Jul 06 2020 at 04:15):

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

view this post on Zulip Alex J. Best (Jul 06 2020 at 04:20):

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

view this post on Zulip Chris M (Jul 06 2020 at 04:21):

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]}

view this post on Zulip Chris M (Jul 06 2020 at 04:30):

@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.

view this post on Zulip Alex J. Best (Jul 06 2020 at 04:37):

(deleted)

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:37):

this is like Coq Ltac

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:37):

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

view this post on Zulip Alex J. Best (Jul 06 2020 at 04:37):

oh lol!

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:37):

the point is to prove inf_assoc

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:37):

using inf_le_left etc

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:40):

@Mario Carneiro do you know Coq Ltac?

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:40):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:41):

I've been wanting to ask about this

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:41):

you can do that in non-interactive tactics

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:41):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:42):

but do we have that functionality currently?

view this post on Zulip Chris M (Jul 06 2020 at 04:44):

what are non-interactive tactics?

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:45):

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.

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:45):

^ an example of Ltac match goal with

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:45):

so we can build tactics that apply inf_le_left and le_inf

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:46):

like a custom solver for lattice equations

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:47):

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}

view this post on Zulip Chris M (Jul 06 2020 at 04:53):

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

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:54):

yes

view this post on Zulip Chris M (Jul 06 2020 at 04:55):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 04:55):

the left hand side first

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:55):

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

view this post on Zulip Mario Carneiro (Jul 06 2020 at 04:57):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 05:03):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 05:11):

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

view this post on Zulip Mario Carneiro (Jul 06 2020 at 05:12):

I think you just wrote a prover for intuitionistic logic

view this post on Zulip Kenny Lau (Jul 06 2020 at 05:12):

oh right they're the same as lattices

view this post on Zulip Kenny Lau (Jul 06 2020 at 05:12):

where's my complement

view this post on Zulip Mario Carneiro (Jul 06 2020 at 05:12):

heyting lattices to be precise

view this post on Zulip Chris M (Jul 06 2020 at 05:13):

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

view this post on Zulip Kenny Lau (Jul 06 2020 at 05:13):

for the first time

view this post on Zulip Chris M (Jul 06 2020 at 05:13):

nice

view this post on Zulip Mario Carneiro (Jul 06 2020 at 05:13):

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

view this post on Zulip Mario Carneiro (Jul 06 2020 at 05:15):

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

view this post on Zulip Scott Morrison (Jul 06 2020 at 06:04):

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

view this post on Zulip Scott Morrison (Jul 06 2020 at 06:04):

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

view this post on Zulip Scott Morrison (Jul 06 2020 at 06:06):

(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.)

view this post on Zulip Scott Morrison (Jul 06 2020 at 06:06):

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.

view this post on Zulip Chris M (Jul 08 2020 at 04:43):

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.

view this post on Zulip Kenny Lau (Jul 08 2020 at 05:32):

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

view this post on Zulip Chris M (Jul 09 2020 at 05:37):

Ah I see it now, thanks :)

view this post on Zulip Chris M (Jul 09 2020 at 06:08):

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?

view this post on Zulip Mario Carneiro (Jul 09 2020 at 06:10):

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

view this post on Zulip Mario Carneiro (Jul 09 2020 at 06:11):

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}

Last updated: May 08 2021 at 17:33 UTC