Addressing mismatch issues

Stream: general

[Peter Nelson]

I am working with a bunch of calculations with expressions that depend on fintype, and mismatch issues are happening. From what I understand, avoiding the mismatches arising is not feasible, but I'm looking for a non-painful way to handle them.

Each individual mismatch can generally be handled with convert rfl, and indeed sometimes this will kill the problems if there is more than one. But it can be hard to handle these issues when they occur in a complicated context and the pretty-printer makes differences invisible. For instance, suppose that a and a' are complicated expressions in int, indistinguishable without diving into implicit parameters, and hiding different fintype instances. Let b and b' be another such pair. Now a = a' and b = b' can be proved with convert rfl (or maybe congr'), but how would I prove, say, that -b + x + a + b' + y + z - a' = x + y + z, where x, y and z are themselves long and complicated enough that copy-pasting them into a proof would double its length?

This is clearly possible, but quite awkard in the middle of a proof. Of course, a proof somehow isomorphic to rw [(by convert rfl : a = a'), (by convert rfl : b = b')], linarith is what I would like. But I can't do this without hundreds of characters and underscores, because a and a' are syntactically identical!

Unfortunately it is hard to come up with an mwe because the nature of my gripe is 'in a complicated context', but I hope I've communicated my question.

(Of course, what I would really like is a way to seamlessly replace fintype with a similar typeclass that is purely propositional, in a way that doesn't involve remaking half the API from scratch, but I don't know how to do that, either).

[Eric Wieser]

If you can't rewrite with a lemma due to a mismatching fintypes instance, that usually means that the lemma is written badly, and only applies to a specific instance

[Kevin Buzzard]

I teach my mathematician students to use set.finite and [finite X] where none of these problems occur. I have no interest in constructive finiteness

[Kevin Buzzard]

oh apparently mathlib doesn't have finite X -- hard luck.

[Johan Commelin]

@Peter Nelson These issues sound quite similar to the issues that we have been facing in homological algebra. Where you have a complex of (say) vector spaces, indexed by int or nat. And now you fact the issues that V i is not the same vector space as V (i - 1 + 1). Which is of course ridiculous. We are still experimenting to find the best solution.

[Johan Commelin]

But more on topic, I think that you provide another strong datapoint for the need of a propositional analogue of fintype.

[Kevin Buzzard]

@Peter Nelson let's first get one thing clear -- are we talking about finite types, or finite subsets of types? We already have set.finite in mathlib, which is an "I am finite" predicate on a set which does not suffer from all the constructivist problems you're seeing.

[Peter Nelson]

We're talking about finite types. I'm not using finset directly at all, except where I'm being forced to. Here is some code - one of the problems occurs in the last lemma.

(Related to the fact that I'm not using finset, what I'm trying to do here is to make the shorthand ∑ (a : X), f a easier to work with, since most of the finset.sum API is instead written in terms of ∑ a in X, f a.)

import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set

variables {α β: Type}[fintype α][add_comm_monoid β](f : α → β)

lemma set.to_finset_insert' (X : set α)(e : α) :
  (X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}

lemma fin_sum_eq (X : set α):
  ∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm

lemma fin_sum_insert {X : set α}{e : α}:
  e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
  rintro he,
  have hdj :disjoint X.to_finset {e},
  { rw [finset.disjoint_iff_inter_eq_empty], ext,
    simp only [finset.not_mem_empty, not_and, finset.mem_singleton, iff_false, finset.mem_inter, mem_to_finset],
    exact λ haX hae, false.elim (he (by {rwa ←hae})),},

  -- this next claim causes instance mismatch problems if fin_sum_eq is invoked directly,
  -- due to two competing instances of fintype for X ∪ {e}
  have hXe : ∑ (a : (X ∪{e}) ), f a = ∑ a in (X ∪ {e}).to_finset, f a,
    convert fin_sum_eq f (X ∪ {e} : set α),

  rw [hXe, fin_sum_eq f (X : set α), set.to_finset_insert' X e, finset.sum_union hdj],
  simp,
end

[Mario Carneiro]

Why don't you just use finsets here? it shouldn't be hard to have analogues of all the sets you could want with open_locale classical

[Peter Nelson]

The set API is just more complete.

[Mario Carneiro]

Only when it comes to equality of sets. The finset API is a lot more complete when it comes to summation; you can do the summation stuff on finsets and pull back to sets for the set algebra

[Mario Carneiro]

lemma fin_sum_insert {X : set α}{e : α}:
  e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
  rintro he,
  obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,
  rw [fin_sum_eq, add_comm, ← finset.sum_insert],
  convert (fin_sum_eq f _).trans _,
  { congr', ext, simp },
  simpa using he,
end

[Mario Carneiro]

set.to_finset doesn't seem to have many lemmas about it, although it does have mem_to_finset which is why the ext, simp works

[Peter Nelson]

so the trick is exists_finset_coe?

[Mario Carneiro]

That's how you make everything use finsets

[Peter Nelson]

Good to know - thanks!

[Peter Nelson]

Unfortunately it seems like the problem cascades. Here's an attempted consequence of the above where a mismatch issue carries forward, with either of our proofs of fin_sum_insert. The context is a little contrived - is is the problematic part of a proof by induction. The proof that works involves reducing to a case where a single convert resolves the goal, but rewriting earlier fails.

def subadditive (g : set α → ℤ) :=
  ∀ X Y, g (X ∪ Y) ≤ g X + g Y

lemma foo (S : set (set α)){g : set α → ℤ}{X₀ : set α}(hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
  g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
  -- rw fin_sum_insert g hX₀,
  -- Doesn't work

  simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,

  refine le_trans (hg _ _) _,
  refine le_trans (int.add_le_add_right hS (g X₀)) (le_of_eq _),
  convert (fin_sum_insert g hX₀).symm,
  -- works
end

[Johan Commelin]

So you can't use S : finset (set \a)?

[Peter Nelson]

I probably could, but I would be worried that this will just move the problem further upwards. In the case I want to invoke, S has type set (set \a) because it's a collection of equivalence classes, so I would have to use some type of equivalence between set and finset to get to finset (set \a).

[Mario Carneiro]

Yes, that's exists_finset_coe as you saw

[Mario Carneiro]

or set.to_finset

[Johan Commelin]

So I guess you can do

obtain \<S, rfl\> := exists_finset_coe S

or something like that, as first line of the proof

[Johan Commelin]

Right, as Mario suggested upstairs:

  obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,

[Johan Commelin]

After that, the proof should be "smooth"

[Mario Carneiro]

it wasn't completely smooth, there seem to be some missing simp lemmas

[Peter Nelson]

Yeah, that last proof is something where I want things from both APIs at the same time.

[Peter Nelson]

of course, what I actually want is that fintype be propositional.

[Eric Wieser]

If you use convert ... using 1, does it show what doesn't match?

[Peter Nelson]

The first instance of fintype ↥(S ∪ {X₀}) is this :

  (@subtype.fintype (set α) (λ (x : set α), x ∈ S)
     (@set.decidable_mem (set α) S (λ (a : set α), classical.prop_decidable (S a)))
     (@set.fintype α _inst_1))
  (@set.fintype_pure (set α) X₀)

and the second is this :

@set.fintype_union (set α)
  (λ (a b : set α),
     @fintype.decidable_pi_fintype α (λ (a : α), Prop) (λ (a : α) (a b : Prop), classical.prop_decidable (a = b))
       _inst_1
       a
       b)
  S
  {X₀}
  (@subtype.fintype (set α) (λ (x : set α), x ∈ S)
     (λ (a : set α), @set.decidable_mem (set α) S (λ (a : set α), classical.prop_decidable (S a)) a)
     (@set.fintype α _inst_1))
  (@set.fintype_pure (set α) X₀)

[Peter Nelson]

Ah, so it's actually decidable_eq that is the culprit! The difference between the above is :

fintype.decidable_pi_fintype α (λ (a : α), Prop) (λ (a : α) (a b : Prop), classical.prop_decidable (a = b))
_inst_1
a
b

vs

classical.prop_decidable (a = b)

I don't know if that makes any of these problems easier to address....

[Kevin Buzzard]

What should propositional finiteness be called? [is_finite alpha]?

[Eric Wieser]

My assumption is that docs#fin_sum_insert is stated poorly

[Eric Wieser]

But that link doesn't work - where is that lemma?

[Bryan Gin-ge Chen]

It was proved earlier in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Addressing.20mismatch.20issues/near/227098783

[Eric Wieser]

Is there a full mwe?

[Eric Wieser]

I think the lemma needs [fintype X] and [fintype (X \union {e})] to avoid this problem

[Peter Nelson]

This mwe is a union of things earlier, but here is all of it in one place:

import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set

variables {α β: Type}[fintype α][add_comm_monoid β](f : α → β)

lemma set.to_finset_insert' (X : set α)(e : α) :
  (X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}

lemma fin_sum_eq (X : set α):
  ∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm

lemma fin_sum_insert {X : set α}{e : α}:
  e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
  rintro he,
  obtain ⟨X, rfl⟩ := (finite.of_fintype X).exists_finset_coe,
  rw [fin_sum_eq, add_comm, ← finset.sum_insert],
  convert (fin_sum_eq f _).trans _,
  { congr', ext, simp },
  simpa using he,
end

def subadditive (g : set α → ℤ) :=
  ∀ X Y, g (X ∪ Y) ≤ g X + g Y


lemma foo (S : set (set α)){g : set α → ℤ}{X₀ : set α}(hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
  g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
  simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,

  --would like to rw here with fin_sum_insert but can't.

  refine le_trans (hg _ _) _,
  refine le_trans (int.add_le_add_right hS (g X₀)) (le_of_eq _),
  convert (fin_sum_insert g hX₀).symm,
end

[Eric Wieser]

Thanks, I'll try my idea out myself tomorrow

[Yakov Pechersky]

Is this just not going to work because subadditive is defined in a classical context?

[Eric Wieser]

Eric Wieser said:

I think the lemma needs [fintype X] and [fintype (X \union {e})] to avoid this problem

Yes, this fixes it, in conjuction with removing fintype α:

import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set

variables {α β: Type} [add_comm_monoid β](f : α → β)

lemma set.to_finset_insert' (X : set α) (e : α) [fintype ↥X] [fintype ↥(X ∪ {e})]:
  (X ∪ {e}).to_finset = X.to_finset ∪ {e} :=
by {ext, simp[or_comm]}

lemma fin_sum_eq (X : set α) [fintype ↥X] :
  ∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm

lemma fin_sum_insert {X : set α}{e : α} [fintype ↥X] [fintype ↥(X ∪ {e})]:
  e ∉ X → ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
  rintro he,
  unfreezingI { obtain ⟨X', rfl⟩ := finite.exists_finset_coe ⟨‹fintype ↥X›⟩ },
  rw [fin_sum_eq, fin_sum_eq, add_comm, ←finset.sum_insert],
  { congr', ext, simp },
  simpa using he,
end

def subadditive (g : set α → ℤ) :=
  ∀ X Y, g (X ∪ Y) ≤ g X + g Y


lemma foo (S : set (set α)) [fintype ↥S] {g : set α → ℤ} {X₀ : set α} [fintype ↥(S ∪ {X₀})] (hX₀ : X₀ ∉ S)
(hg : subadditive g) (hS : g (⋃₀ S) ≤ ∑ (X : ↥S), g X):
  g (⋃₀(S ∪ {X₀})) ≤ ∑ (X : ↥(S ∪ {X₀})), g X :=
begin
  simp_rw [sUnion_union, sUnion_singleton] at hS ⊢,
  rw fin_sum_insert _ hX₀,  -- rw works
  sorry,
end

[Eric Wieser]

You should never assume a more general fintype instance than the one the lemma actually requires and let the specific one be derived, because then the lemma won't match again terms which obtain the specific one via a different means

[Peter Nelson]

Thank you! What if I want to invoke fin_sum_insert in the middle of a larger proof where there is already a fintype α instance hanging around?

[Eric Wieser]

It should work fine

[Eric Wieser]

When you rewrite, the instances on the left-hand side of the eq / iff will already be present in the goal, while typeclass instances will try to deduce the ones on the right-hand-side

[Peter Nelson]

Ok. I've run into a curiosity that results from this solution when I'm applying it in an inductive proof. The below is the smallest example where I can reproduce the issue.

import tactic
----------------------------------------------------------------
open_locale classical big_operators
open set

variables {α β : Type}[add_comm_monoid β]

lemma fin_sum_empty (f : α → β) :
  ∑ (a : (∅ : set α)), f a = 0 :=
finset.sum_empty

lemma fin_sum_eq (f : α → β)(X : set α)[fintype X]:
  ∑ (a : X), f a = ∑ a in X.to_finset, f a :=
let φ : X ↪ α := ⟨coe, subtype.coe_injective⟩ in (finset.sum_map (finset.univ) φ f).symm

lemma fin_sum_insert (f : α → β){X : set α}{e : α}(he : e ∉ X)[fintype ↥X][fintype ↥(X ∪ {e})]:
   ∑ (a : X ∪ {e}), f a = (∑ (a : X), f a) + f e :=
begin
  unfreezingI {obtain ⟨X', rfl⟩ := finite.exists_finset_coe ⟨‹fintype ↥X›⟩ },
  rw [fin_sum_eq, fin_sum_eq, add_comm, ←finset.sum_insert],
  { congr', ext, simp },
  simpa using he,
end

lemma induction_foo [fintype α](P : set α → Prop):
  (P ∅) → (∀ (X : set α)(e : α), e ∉ X → P X → P (X ∪ {e})) → (∀ X, P X) :=
sorry

lemma fin_sum_one_eq_card [fintype α](X : set α):
  ∑ (a : X), (1 : α → ℤ) a = X.to_finset.card :=
begin
  revert X, apply induction_foo,
  {rw [to_finset_card, empty_card'], convert fin_sum_empty _, },

  intros X e he hX,
  -- rw fin_sum_insert _ he,
  -- doesn't work

  rw fin_sum_insert, swap, assumption,
  --works

  sorry,
end

In the proof of fin_sum_one_eq_card, I am able to rw with fin_sum_insert if I don't pass it the term he, but if I pass it he, the rewrite fails, even though he is exactly the term it needs, and resolving the goal later using he works fine . The swap, assumption handles this cleanly enough in practice, but I'd still like to understand what is happening, and can't figure it out.

[Kevin Buzzard]

I don't know the answer to your question, but convert works so it's some type class inference issue again. Independent of that, why have you got such a horrible ∑ (a : ↥X), 1 ↑a term? Why not just some over a \in X? Oh! Because it's not a finset :-( I think your fabulous questions are just indicating that we need some API. We solved this with finsum_in when we were doing finite groups: see here.

[Kevin Buzzard]

I totally agree with you, all this constructive stuff is hard to work with but as you can see there are now sufficiently many experts around going "no it's fine, just think about it this way and there's a trick" that we've all just got used to it and learnt the tricks. Why not just write your own API and sorry it all out? finsum_in will solve all your problems. The proofs are just hacks to reduce everything to finset.sum and are very ugly but you don't care about those, you just reap the benefits.

[Kevin Buzzard]

@Peter Nelson I hesitated to introduce these new definitions because some people pointed out to me that the tools we have are enough for the job as long as you continually jump over the traps you're running into, and hence because such a nonconstructive approach is not strictly necessary (it all _can_ be done with what we have) I was just in danger of adding to the noise a la xkcd#927. However your situation I think just makes it clear that we need them. If this sort of stuff is deterring beginners then it's clear that there's an argument for it. I've suggested these before but here we go again:

class is_finite (X : Type u) : Prop
noncomputable def finsum {ι M} [add_comm_monoid M] (f : ι → M) : M -- zero if support infinite
noncomputable def finsum_in {ι M} [add_comm_monoid M] (s : set ι) (f : ι → M) : M -- zero if support intersect s is infinite
def fincard (X : Type u) : ℕ -- zero if X is infinite

Why don't you switch to these, sorry all the lemmas you need and feed them back, and we can just make the API? I've done it once before and it was quite fun, I just didn't get round to PR'ing it because some people weren't convinced this stuff was needed. In some sense they might be right -- jump through some hoops, use convert and woo-hoo, it's all computable! I am losing my patience with this approach.

[Kevin Buzzard]

  intros X e he hX,
  convert fin_sum_insert _ he, -- this works
  have : ↑((X ∪ {e}).to_finset.card) = ∑ (a : ↥X), (1 : α → ℤ) ↑a + (1 : α → ℤ) e, -- the goal!
    sorry,
  exact this, -- stupid typeclass fail

[Kevin Buzzard]

With my approach there will be no up-arrows

[Jason KY.]

I wonder if it is worthwhile just pr finsum. All of the APIs are already done. I don't think too many standards is an issue if we can easily convert between the standards and I feel that this has come up often enough to warrant a separate definition.

[Peter Nelson]

I like this idea. I do see the perspective of the more constructively inclined, and am even (on some level) enjoying how much these subtle issues teach me about the language. I'm grateful for all the help, patience and expertise I've been getting here.

However, I am planning to give a talk in the near future to fellows combinatorialists about how great/fun formalization is, and these types of problems are among the downsides on my mind. 'Traps' is the right word - none of the problems are insurmountable, but they are barriers to entry. Being someone very interested in theorems about finite structures, I suspect that this stuff happens more frequently for me than many others, and it would be good to have a solution that can be explained in terms an average mathematician can immediately understand.

Regarding an API, I would love to have such a thing available in mathlib. Likely not much would be needed - I suspect the existing one is all I would need to work with.

[Eric Wieser]

A linter to catch the type of decidable / fintype instance problems I resolved above would likely help with avoiding some of these traps

[Kevin Buzzard]

Yes but I think the time has come now to do this -- and I'm about to sit down and do it -- because there are some people who simply never ever want to #eval anything and simply do not need the trouble which things like fintype and finset.sum can cause, especially if they open_locale classical on line 1 and then occasionally use types which have got decidable equality. It's just one extra hassle which doesn't need to be dealt with. Avigad told me that Isabelle has finsum and it works fine.

[Kevin Buzzard]

@Jason KY. I'll put you as co-author, I'll do it on the discord.

[Mario Carneiro]

It's not just #eval, when it comes to facts about small matrices or something dec_trivial can sometimes be the most powerful tool at our disposal

[Mario Carneiro]

That's not a great situation, since that approach has a host of limitations, but it is what it is

[Mario Carneiro]

That said I'm in agreement on the introduction of fincard and finsum FWIW. There are just a lot of lemmas that are needed to make this nice - I found at least two or three in my proof above, regarding the interaction between set.to_finset and all of the finset API; with a finsum API we also need lemmas relating it to finset sum, and also copies of everything in the finset sum API.

[Kevin Buzzard]

First attempt to make a finsum API is #6355. Many thanks to @Jason KY. who did most of the work.

[Kevin Buzzard]

@Peter Nelson we don't make propositional finite types because we can just use nonempty (fintype α). We don't do cardinality yet, that is some work we have prepared but haven't got into PR shape yet. This might take some time to get through the system.

[Peter Nelson]

That sounds great - I look forward to tinkering tomorrow.

Might there be a case for also adding finmax to the API? It is a special case of finsum (and could be defined as such), but API lemmas in which maxima are taken over subsets etc could be useful. Something I'm currently doing uses fintype.exists_max + choice to define a maximum, and I haven't run into any mismatch issues so far, but who knows what will happen in the future.

[Peter Nelson]

variables {α β : Type u}[linear_order β]

noncomputable def finmax (f : α → β) : β := sorry
-- some default value if no max exists, otherwise the max

lemma finmax_is_max [nonempty α][nonempty (fintype α)](f : α → β): ∀ x, f x ≤ finmax f := sorry

lemma exists_argmax  [nonempty α][nonempty (fintype α)](f : α → β): ∃ x,  f x = finmax f  := sorry

etc etc

[Mario Carneiro]

That seems very near to what supr already does

[Mario Carneiro]

we just need a version of supr that works on any preorder

[Peter Nelson]

The existence of an argmax following from (propositional) finiteness is what I'm after. I can't see anything about finiteness in the supr API, but maybe I'm missing something?

[Mario Carneiro]

finite lattices are complete

[Peter Nelson]

Is there a fintype hiding there somewhere?

[Mario Carneiro]

My point is that for the finmax function, you don't need any inputs except for preorder B and nonempty A, and it can be well defined whenever anything like it makes sense; you can then prove that it makes sense when A is finite to make use of it in your scenario

[Mario Carneiro]

there's no need to bake finiteness into the definition though

[Mario Carneiro]

actually nonempty B is probably better than nonempty A here, that way it can default to the zero of the codomain instead of a random value

[Mario Carneiro]

inhabited B is probably better

[Peter Nelson]

Ah, it looks like set.finite.exists_maximal_wrt already does what I want , without any fintype. Here it is:

theorem set.finite.exists_maximal_wrt {α : Type u} {β : Type v} [partial_order β]
(f : α → β)(s : set α) (h : s.finite) :
s.nonempty → (∃ (a : α) (H : a ∈ s), ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a')

Or not quite, but it's easy to get a linear_order version.

[Peter Nelson]

@Kevin Buzzard @Jason KY. I've started incorporating finsum into my project, as well as rolling my own fincard by finsumming ones (I'm assuming the intended implementation of fincard is more principled, but mine will do for now). It's great avoiding the mismatches, and what's more, not to have to regularly descend into finset coercion hell in the first place!

I have a question about intended usage. For most of my interaction with finsum, everything will be happening with variables {\a : Type} [nonempty (fintype \a)] at the top of files. But this will mean that for each of the finsum and finsum_in lemmas that require explicit finiteness assumptions (which already each come in a few different flavours) , there will be yet another version that takes a nonempty fintype instance. For example, here are statements of a lemma I proved and its version that takes an instance.

lemma finsum_le_finsum [ordered_add_comm_monoid M](hfg : ∀ x, f x ≤ g x)
(hf : (function.support f).finite)(hg : (function.support g).finite):
  ∑ᶠ (i : α), f i ≤ ∑ᶠ (i : α), g i :=
sorry

lemma finsum_le_finsum' [ordered_add_comm_monoid M][nonempty (fintype α)]
(hfg : ∀ x, f x ≤ g x):
  ∑ᶠ (i : α), f i ≤ ∑ᶠ (i : α), g i :=
sorry

Is doing this for every such lemma a reasonable solution? I can't even think of a good naming convention.

[Jason KY.]

I think the idea is you prove the different versions if you are writing APIs (e.g. your example) while if you are simply using finsum you can just stick to one version (or the most general version, i.e. the support is finite.). @Mario Carneiro suggest a naming scheme here