Alternative to have followed by repeat {assumption}

Stream: new members

[Marc Masdeu]

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]

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

[Kevin Buzzard]

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

[Ruben Van de Velde]

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

[Rob Lewis]

Or apply key_lemma; assumption

[Marc Masdeu]

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

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

Note that assumption' will try assumption on all goals.

[Marc Masdeu]

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

[Scott Morrison]

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