## Stream: new members

### Topic: Alternative to have followed by repeat {assumption}

#### Marc Masdeu (Oct 01 2020 at 14:19):

Hello,

I find myself with lemmas that have many hypotheses and that directly solve the goal. I apply them (without passing the hypotheses) and end up with many new goals, each of which already in the context, so I do repeat {assumption} to close the goal. I would like to know if there is a nicer way to do that (in terms of less characters typed, for instance). A variation of the problem is when after the apply I can close the goal with repeat {tauto}.

Here is a MWE which is a bit too silly but illustrates what I am trying to say:

import tactic

lemma key_lemma {x : ℕ} : x > 3 → x < 5 → x = 4 :=
begin
intros h g,
linarith,
end

lemma my_lemma {x : ℕ} (h : 2*x > 3) (g : 2*x < 5) : 2*x = 4 :=
begin
apply key_lemma, -- is there a tactic that does these two lines together automatically?
repeat {assumption}, --
end


#### Kevin Buzzard (Oct 01 2020 at 14:21):

lemma my_lemma {x : ℕ} (h : 2*x > 3) (g : 2*x < 5) : 2*x = 4 :=
begin
apply key_lemma h g,
end


#### Kevin Buzzard (Oct 01 2020 at 14:21):

lemma my_lemma {x : ℕ} (h : 2*x > 3) (g : 2*x < 5) : 2*x = 4 :=
key_lemma h g


#### Ruben Van de Velde (Oct 01 2020 at 14:45):

If you don't want to use the names, you could do key_lemma ‹_› ‹_›

#### Rob Lewis (Oct 01 2020 at 14:48):

Or apply key_lemma; assumption

#### Marc Masdeu (Oct 01 2020 at 16:29):

@Kevin Buzzard , what you propose is exactly what I'm trying to avoid here: if key_lemma has 10 hypotheses, then I don't want to be typing the names that I have come up with before, since it makes maintenance harder and it's quite boring.

@Rob Lewis this is similar to my solution and probably makes me content.

I guess that it wouldn't hurt that apply automatically checked if it can close the goal with the assumptions already in the context...

#### Johan Commelin (Oct 01 2020 at 16:30):

It might make apply slow, and since it is used a lot, we want apply to be as fast as possible.
Hence apply foo; assumption seems like the best idiom

#### Marc Masdeu (Oct 01 2020 at 16:33):

Yes, I was afraid that I was missing a tactic name, but fine.

#### Kevin Buzzard (Oct 01 2020 at 17:17):

Can you give some concrete example where you really want to feed 10 hypotheses into a theorem? Normally things like type class inference and unification do a lot of the work for you.

#### Kevin Buzzard (Oct 01 2020 at 17:18):

lemma my_lemma {x : ℕ} (h : 2*x > 3) (g : 2*x < 5) : 2*x = 4 :=
begin
apply key_lemma (by assumption) (by assumption)
end


#### Marc Masdeu (Oct 01 2020 at 17:32):

Here is a lemma I have proven, regarding HilbertPlane. It says given a line (implicit) and three point not on it (implicit, also), then if both B and C belong "to the other side" than A, then B and C are at the same side of the line.

lemma same_side.at_most_two_classes (hA : ¬ A ∈ ℓ) (hB : ¬ B ∈ ℓ) (hC : ¬ C ∈ ℓ)
(hBneqC : B ≠ C) (hAB: ¬ same_side ℓ A B) (hAC: ¬ same_side ℓ A C): same_side ℓ B C :=
begin
sorry
end


This gets used to the following theorem, which says that given a line then one can split its complement into two classes of points, S1 and S2.

theorem plane_separation (ℓ : Ω.Line):  ∃ S1 S2 : set (Ω.Point),
S1 ∩ S2 = ∅ ∧ S1 ∪ S2 ∪ ℓ = {P : Ω.Point | tt} ∧
(∀ A B : Ω.Point, (A ∉ ℓ) → (B ∉ ℓ) →
(( A ∈ S1 ∧ B ∈ S1) ∨ (A ∈ S2 ∧ B ∈ S2) ↔ (A#B) ∩ ℓ = ∅)) :=
begin
sorry
end


At some point of the proof I am at this state

Ω: HilbertPlane
ℓ: HilbertPlane.Line
CD: HilbertPlane.Point
hC: C ∉ ℓ
hD: D ∉ ℓ
H: ¬same_side ℓ C D
S1: set HilbertPlane.Point := {P : HilbertPlane.Point | same_side ℓ P C}
S2: set HilbertPlane.Point := {P : HilbertPlane.Point | same_side ℓ P D}
x: HilbertPlane.Point
h: x ∉ ℓ
hs: ¬same_side ℓ C x
⊢ same_side ℓ x D


and I prove it by

by_cases hxD : x = D,
rw hxD, exact same_side.refl,
apply same_side.at_most_two_classes,
repeat {assumption},


In this result this same patter occurs once more.

This could use of class inference, but then I never know what kind of assumptions need to be put in this system...

#### Johan Commelin (Oct 01 2020 at 17:33):

No, I don't think this should use type classes. It's just a lot of assumptions.

#### Johan Commelin (Oct 01 2020 at 17:34):

Note that assumption' will try assumption on all goals.

#### Marc Masdeu (Oct 01 2020 at 17:36):

@Johan Commelin this seems very similar to the ";" trick. I guess it's okay to have so much variety.

#### Scott Morrison (Oct 02 2020 at 00:01):

No one has mentioned tactic#solve_by_elim, which is very useful for sequences of apply and assumption.

Last updated: Dec 20 2023 at 11:08 UTC