examples

Stream: new members

[Alex Zhang]

How can I close the following goal?
example (h :card I = 0) (i : I) : false := sorry

[Adam Topaz]

We have docs#cardinal.ne_zero_iff_nonempty

[Adam Topaz]

And even docs#cardinal.eq_zero_iff_is_empty

[Adam Topaz]

Do you need more help using such lemmas?

[Alex Zhang]

Thanks and I will try!

[Alex Zhang]

This is simple to prove example (a : ℚ): - ((λ i, a) : α → ℚ) = (λ i, -a) := by {ext, simp}.
But are there any built-in lemmas pushing or pulling scalars around maps?

[Kyle Miller]

In this case, it turns out to be true definitionally:

example {α : Type*} (a : ℚ): - ((λ i, a) : α → ℚ) = (λ i, -a) := rfl

[Eric Wieser]

docs#pi.neg_def

[Eric Wieser]

Hmm. We have docs#pi.add_def

[Eric Wieser]

Want to PR that missing lemma?

[Alex Zhang]

Yes! (but perhaps not by me :) )

[Alex Zhang]

Let me know when things are PRed :)

[Eric Wieser]

I'm guessing docs#pi.sub_def is also missing

[Eric Wieser]

Weird

[Kyle Miller]

I haven't checked -- would @[simps] be able to add these definition lemmas? I'm partly not sure if it would work at all, and partly not sure how it interacts with to_additive.

[Eric Wieser]

Yes, but it would mark them simp which might not be helpful

[Alex Zhang]

How should I prove

import tactic
example (a : ℕ) : ↑(a.pred) = ↑(a) - (1 :ℚ) := by {sorry}

[Anne Baanen]

Some sort of docs#nat.pred_eq_sub_one followed by tactic#norm_cast?

[Anne Baanen]

(Note that this is only true for 0 < a)

[Eric Rodriguez]

0.pred = 0

[Anne Baanen]

In fact, there is just docs#nat.cast_pred

[Kevin Buzzard]

@Alex Zhang you really want to move away from nat.pred and nat.sub. They are very poorly behaved functions mathematically, and you can always rewrite in terms of addition.

[Kevin Buzzard]

Just like we don't use > and >= because we can rewrite in terms of < and <=.

[Alex Zhang]

I guess they are not provable actually as Eric pointed out.

example : (nat.pred 0) = 0 := rfl
example : 0 - (1 :ℚ) = -1 := by simp

[Kevin Buzzard]

Right, but the corresponding addition versions are true and provable.

[Alex Zhang]

I unfortunately encountered pred as I used finset.card_erase_of_mem

[Kevin Buzzard]

But in that situation you can prove that you're not taking pred of 0

[Mario Carneiro]

there are other card_erase lemmas that don't use pred I think

[Mario Carneiro]

looks like most users just use something along the lines of rw [finset.card_erase_of_mem, nat.pred_succ]

[Alex Zhang]

I am just rewriting

lemma finset.card_erase_of_mem' [decidable_eq α] {a : α} {s : finset α} :
  a ∈ s → finset.card (finset.erase s a) + 1 = finset.card s :=

[Kevin Buzzard]

This is a better lemma because it's a stronger statement.

[Mario Carneiro]

It's not a good rewrite lemma though

[Mario Carneiro]

what's the #xy here? How did you get here

[Alex Zhang]

Mario Carneiro said:

It's not a good rewrite lemma though

perhaps change the direction?

[Alex Zhang]

Mario Carneiro said:

what's the #xy here? How did you get here

I am proving

import algebra.big_operators
import data.fintype.card
import data.finset.basic

open_locale big_operators

variables {I : Type*} [fintype I] [decidable_eq I]
def fn : I → I → ℚ := λ i j, ite (i = j) 0 1
lemma eg (j : I) : ∑ (i : I), (fn i j) = fintype.card I - 1 :=
by {simp [fn, finset.sum_ite], simp [finset.filter_ne'],
  simp [finset.card_erase_of_mem],sorry}

[Mario Carneiro]

you have a - in the theorem statement

[Mario Carneiro]

how about writing it as (∑ (i : I), fn i j) + 1 = fintype.card I instead

[Alex Zhang]

It will not be super helpful

lemma eg (j : I) : ∑ (i : I), (fn i j) + 1 = fintype.card I :=
by {simp [fn, finset.sum_ite], simp [finset.filter_ne'],
  simp [finset.card_erase_of_mem],sorry}

I have got around this by writing an "add" version for finset.card_erase_of_mem, which is easy.

[Alex Zhang]

(deleted)

[Kevin Buzzard]

import tactic

example (a : ℕ) (h : a ∣ 4) (h₁ : a ≠ 1) (h₂ : a ≠ 2) : a = 4 :=
begin
  have h2 : a ≤ 4 := nat.le_of_dvd dec_trivial h,
  interval_cases a,
  { revert h, norm_num },
  { revert h₁, norm_num },
  { revert h₂, norm_num },
  { revert h, norm_num }
end

[Kevin Buzzard]

Even better:

import tactic

example (a : ℕ) (h : a ∣ 4) : a ≠ 1 → a ≠ 2 → a = 4 :=
begin
  have h2 : a ≤ 4 := nat.le_of_dvd dec_trivial h,
  revert h,
  interval_cases a;
  norm_num,
end

[Alex Zhang]

Many thanks, Kevin!

[Alex Zhang]

I didn't know interval_cases before

[Alex Zhang]

How can I prove that the card of a field is >= 1?

import tactic.gptf
import data.fintype.card
import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] (p : ℕ) [char_p F p]

open fintype

example : 1 ≤ card F := by sorry

[Alex Zhang]

I got it! example : 1 ≤ card F := fintype.card_pos_iff.mpr ⟨1⟩

[Alex Zhang]

Is there a way to improve tauto! a little bit such that it can close goals like

import tactic
example {α} (a b c : α): a = b ∧ b = c ∨ ¬a = b ∧ a = c ↔ a = c := by tauto!

or is there any other tactic(s) that are able to close this goal?
I noticed tauto {closer := tac} in https://leanprover-community.github.io/mathlib_docs/tactics.html#tautology. But not sure how to use this feature.

[Kevin Buzzard]

import tactic
example {α} (a b c : α): a = b ∧ b = c ∨ ¬a = b ∧ a = c ↔ a = c :=
begin
  by_cases h : a = b;
  simp [h],
end

I am a bit surprised that tauto! doesn't close this.

[Kevin Buzzard]

Oh, I guess tauto just does plain logic, and this proof needs transitivity of =.

[Alex Zhang]

Kevin Buzzard said:

Oh, I guess tauto just does plain logic, and this proof needs transitivity of =.

Exactly!

[Alex Zhang]

It seems that tauto {closer := tac} is able to improve it, but not quite sure about this.

[Kevin Buzzard]

import tactic

meta def tidytauto := `[tidy, tauto!]

example {α} (a b c : α): a = b ∧ b = c ∨ ¬a = b ∧ a = c ↔ a = c :=
begin
  tidytauto,
end

[Alex Zhang]

I didn't know this trick for combining tactics.

[Kevin Buzzard]

it makes for unreadable code so it's not really used much in practice.

[Alex Zhang]

How can I make this a local or private definition?

[Alex Zhang]

and why isn't meta def tidytauto := [ tauto!, tidy]` able to close the goal?

[Kevin Buzzard]

because tauto! fails (rather than succeeding and leaving two goals) and tidy would only work on one goal.

[Kevin Buzzard]

The answer to your question is simply that tauto!, tidy does not close the goal. You can see the errors yourself.

[Alex Zhang]

Because tauto! is a finishing tactic, so doesn't tidy actually do anything in tauto!, tidy?

[Horatiu Cheval]

I always thought such things like tidytauto should be in the tactic.interactive namespace. Why isn't it the case? It seems all my rudimentary knowledge about tactics is wrong :)

[Alex Zhang]

How can I prove that

import field_theory.finite.basic
example {F : Type*} [fintype F] [has_zero F] [decidable_eq F] :
fintype.card {a : F // a = 0} = 1 := sorry

[Eric Rodriguez]

docs#fintype.card_eq_one_iff

[Eric Rodriguez]

actually, simp does it - did you even try that?

[Alex Zhang]

I don't think simp itself will do. I tried simp.

[Alex Zhang]

simp [fintype.card_eq_one_iff] closes the goal!

[Eric Rodriguez]

Simp works on my local machine. Are uou on the latest mathlib?

[Alex Zhang]

No. Thanks for letting me know this! :)

[Alex Zhang]

Is "b⁻¹ *_ is an equivalence for nonzero b in a field " established in mathib?

[Anne Baanen]

I don't think so, but here's a quick bit of code:

@[simps]
def units.mul_equiv {M : Type*} [monoid M] (u : units M) : M ≃ M :=
{ to_fun := (*) u,
  inv_fun := (*) ↑u⁻¹,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

@[simps]
def group_with_zero.nonzero_mul_equiv {G : Type*} [group_with_zero G] (b : G) (hb : b ≠ 0) : G ≃ G :=
(units.mk0 b hb).mul_equiv

[Anne Baanen]

In particular, these are linear equivs if you have an algebra structure:

...
@[simps]
def units.mul_lequiv {R A : Type*} [comm_semiring R] [semiring A] [algebra R A] (u : units A) : A ≃ₗ[R] A :=
{ .. u.mul_equiv,
  .. algebra.lmul R A u }

@[simps]
def group_with_zero.nonzero_mul_lequiv {R F : Type*} [comm_semiring R] [field F] [algebra R F]
  (b : F) (hb : b ≠ 0) : F ≃ₗ[R] F :=
(units.mk0 b hb).mul_lequiv

[Eric Wieser]

docs#equiv.mul_left, docs#equiv.mul_left'?

[Anne Baanen]

That's weird, I tried various permutations of library_search and grep equiv.l?mul but couldn't find these.

[Eric Wieser]

And even docs#order_iso.mul_left

[Eric Wieser]

I don't know if we have the add_equiv version for division rings