Newbie question: How to apply `rfl` for every possible input

Stream: new members

[Michael Fishman]

Below is a minimal example of what I'm trying to do. How can I rewrite colors_map_to_one_enumerated_proof to avoid enumerating over colors explicitly? colors_map_to_one_abstracted_proof is my failed attempt. I expect I'm missing a very simple change that would make this work.

inductive Color
  | Blue
  | Red
deriving Repr

def f (c : Color) : Nat :=
  match c with
    | .Red => 1
    | .Blue => 1

/--Prove that f is 1 for all colors by going over each color explicitly-/
theorem colors_map_to_one_enumerated_proof : (∀ c : Color, f c = 1) :=
  fun (c : Color) =>
  match c with
  | Color.Red => by rfl
  | Color.Blue => by rfl

/--Prove that f is 1 for all colors without going over each color explicitly. Does not work.-/
theorem colors_map_to_one_abstracted_proof : (∀ c : Color, f c = 1) :=
  fun (c : Color) =>
    match c with
      | _ => by rfl -- Fails

Failure message:

The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
c x✝ : Color
⊢ f x✝ = 1

[Kevin Buzzard]

It doesn't work because the equality is true, but it's not true by definition. If you do cases on c then you're using Color.rec which is an axiom.

[Eric Wieser]

by cases c <;> rfl might be the answer you want here

[Michael Fishman]

Thank you! That worked.

theorem colors_map_to_one_abstracted_proof : (∀ c : Color, f c = 1) :=
  fun (c : Color) =>
  by cases c <;> rfl

(In case anyone reads this in the future, here are the docs for the <;> tactic.)

[Michael Fishman]

Followup question: I want this to work when I use \a instead of Color, where \a is any finite product of inductive types. How can I express this? I know I can do something like [TypeClassName \a] to express that \a satisfied the type class TypeClassName, but I don't know wha the analagous syntax is for saying a type is inductive.

I checked that, if I replace Color with a product of inductive types Color \times Size, that by cases c <;> rfl still works.

[Michael Fishman]

The error I get is

tactic 'induction' failed, major premise type is not an inductive type

[Ted Hwa]

I'm no expert but I don't think you can get this to work because the tactic would have to split the goal into an unknown number of cases.

[Michael Fishman]

Fair! In retrospect, I realize this followup example doesn't really map to the actual problem I'm working on.

[Michael Fishman]

Related question: Given an inductive type, can I get a list of all its values? For now, I made a custom FinType type class with an .all method, but I expect there's a more built-in technique.

[Ted Hwa]

Be careful with that idea. Inductive types encompass much more than just finite enumerations. It allows for recursion as well. For example, Nat is an inductive type.

[Michael Fishman]

Thanks for the warning. Is there a standard way to talk about types with a finite number of values?

[Ted Hwa]

Can you explain more what you are trying to do? Usually I haven't found a need for something like .all. As for Fintype, it already has a field called elems but I don't think I've ever used it directly.

[Michael Fishman]

I didn't realize Fintype existed - I made a new typeclass for that :sweat_smile:
Thanks for the link!

I'm trying to create a type for Probability Distributions over finite event spaces, where the event variables of the distribution are part of the type.
Eg if I have a probability distribution over Color, and a probability distribution over Species, I want the product distribution over Color x Species to have its type inferred automatically.

I'm representing a Distribution as a function mapping the event space to non negative rationals, along with a proof that the function sums to one. I'm using .all / .elems to define the how to sum up all the values of the function.

/-- Type with a finite number of members-/
class FinType (α : Type) where
  all : List α

/--Product of FinTypes is a FinType-/
instance [FinType α] [FinType β] : FinType (α × β) where
  all := (FinType.all : List α).product (FinType.all : List β)


inductive Color
  | Blue
  | Red
deriving Repr

inductive Species
  | Pansy
  | Rose
deriving Repr


inductive Size
  | Small
  | Large
deriving Repr

instance : FinType Color where
  all :=  [.Blue, .Red]

instance : FinType Species where
  all := [.Pansy, .Rose]

instance : FinType Size where
  all :=  [.Small, .Large]

/--Sum all elements of a FinType when mapped via f. Can we do this without the parens?-/
def finmapsum (α : Type) [FinType α] (f : α → NNRat) : NNRat :=
  ((FinType.all).map f).sum

/--True iff α sums to 1 via f-/
def SumsToOne {α : Type} [FinType α] (f : α → NNRat) : Prop :=
  finmapsum α f = 1

structure Distribution (α : Type) [FinType α]  where
  f : α → NNRat
  sums_to_one : SumsToOne f


/--Make product of functions-/
def product_function (fa : α → NNRat) (fb : β → NNRat) : (α × β) → NNRat :=
  fun (a, b) => (fa a) * (fb b)


/--The product of two probability distributions is still a distribution, ie the probabilities sum to 1.-/
theorem product_is_distribution [FinType α] [FinType β] (pa : Distribution α ) (pb : Distribution β) : SumsToOne (product_function pa pb) :=
  sorry

[Ted Hwa]

You want to use the BigOperators which can be used to form a sum over a finite set. For that to work, you need to use the built-in classes, not your own.

[Michael Fishman]

Thanks! I'll give those a try.

[Kevin Buzzard]

The topic of this thread doesn't convey at all the fact that you want to make finite probability spaces, something which we probably have already. I would ask another question in #new members or #mathlib4 (threads are cheap!) about implementation of finite probability spaces containing your actual question, you might find all the work is already done.

[Daniel Weber]

I have some stuff on finite probability spaces here, you can take a look at how I implemented it

[Michael Fishman]

Fair! I got a bit XY'ed :sweat_smile:

I posted another question for this now.

I'll take a look through your implementation, Daniel. Thanks for making and sharing it!