Zulip Chat Archive

Stream: new members

Topic: Alternative to have followed by repeat {assumption}


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ruben Van de Velde (Oct 01 2020 at 14:45):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 14:48):

Or apply key_lemma; assumption

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Marc Masdeu (Oct 01 2020 at 16:33):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:34):

Note that assumption' will try assumption on all goals.

view this post on Zulip 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.

view this post on Zulip 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: May 10 2021 at 00:31 UTC