# Zulip Chat Archive

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

#### Alex J. Best (Jul 06 2020 at 04:37):

(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

#### Alex J. Best (Jul 06 2020 at 04:37):

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?

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

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

#### Chris M (Jul 06 2020 at 05:13):

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