## Stream: new members

### Topic: tactic for "apply in some order"

#### 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"?

#### 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


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


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

(deleted)

#### Kenny Lau (Jul 06 2020 at 04:37):

this is like Coq Ltac

#### Kenny Lau (Jul 06 2020 at 04:37):

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

oh lol!

#### Kenny Lau (Jul 06 2020 at 04:37):

the point is to prove inf_assoc

#### Kenny Lau (Jul 06 2020 at 04:37):

using inf_le_left etc

#### Kenny Lau (Jul 06 2020 at 04:40):

@Mario Carneiro do you know Coq Ltac?

#### Kenny Lau (Jul 06 2020 at 04:40):

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

#### Kenny Lau (Jul 06 2020 at 04:41):

I've been wanting to ask about this

#### Mario Carneiro (Jul 06 2020 at 04:41):

you can do that in non-interactive tactics

#### 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

#### Kenny Lau (Jul 06 2020 at 04:42):

but do we have that functionality currently?

#### Chris M (Jul 06 2020 at 04:44):

what are non-interactive tactics?

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


#### Kenny Lau (Jul 06 2020 at 04:45):

^ an example of Ltac match goal with

#### Kenny Lau (Jul 06 2020 at 04:45):

so we can build tactics that apply inf_le_left and le_inf

#### Kenny Lau (Jul 06 2020 at 04:46):

like a custom solver for lattice equations

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


#### Chris M (Jul 06 2020 at 04:53):

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

yes

#### Chris M (Jul 06 2020 at 04:55):

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

#### Kenny Lau (Jul 06 2020 at 04:55):

the left hand side first

#### 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

#### Mario Carneiro (Jul 06 2020 at 04:57):

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

#### 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


#### 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


#### Mario Carneiro (Jul 06 2020 at 05:12):

I think you just wrote a prover for intuitionistic logic

#### Kenny Lau (Jul 06 2020 at 05:12):

oh right they're the same as lattices

#### Kenny Lau (Jul 06 2020 at 05:12):

where's my complement

#### Mario Carneiro (Jul 06 2020 at 05:12):

heyting lattices to be precise

#### 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?

#### Kenny Lau (Jul 06 2020 at 05:13):

for the first time

nice

#### Mario Carneiro (Jul 06 2020 at 05:13):

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

#### Mario Carneiro (Jul 06 2020 at 05:15):

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

#### 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!)

#### 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


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

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

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

#### 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

#### Chris M (Jul 09 2020 at 05:37):

Ah I see it now, thanks :)

#### 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?

#### 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

#### 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