You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
It is nontrivial (currently for me impossible) to use wlog in the following example.
lemmaforty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
(1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
wlog : a ≤ b ∧ b ≤ c, -- or some similar incantation involving "using ..."end
I am perfectly happy with having to prove some side goals.
The text was updated successfully, but these errors were encountered:
import tactic.wlog data.rat.order
lemmaforty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
(1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
wlog : a ≤ b ∧ b ≤ c using [a b c, a c b, b a c, b c a, c a b, c b a] tactic.skip,
end
@jcommelin I like your suggested syntax. My only worry is that, because the number of cases is n! for n variables, it's easy to make it unreasonably slow or otherwise expensive. What do you think of setting an upper limit of 4 or 5 variables with an error message if you go over but with the option to override it?
Yup, that seems totally reasonable. I think that the typical use case will be n = 3, sometimes n = 4. (And with n = 2 the new syntax doesn't save bytes.)
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
It is nontrivial (currently for me impossible) to use
wlog
in the following example.I am perfectly happy with having to prove some side goals.
The text was updated successfully, but these errors were encountered: