Working with `fin n` (and `ite`?)

Stream: maths

[Johan Commelin]

How should I do this:

definition helpme {n : ℕ} (i : fin (n+1)) (f: fin n → ℝ) : fin (n+1) → ℝ := sorry
-- λ k, if k < i then f ⟨k, sorry⟩ else if k = i then 0 else f (nat.pred k)

[Johan Commelin]

As you can see, I have a definition that almost works. (And I could get rid of the sorry in the middle by digging through some files in mathlib.)

[Kevin Buzzard]

if k : fin n then k is a pair consisting of a nat and a proof that the nat is less than n.

[Kevin Buzzard]

You can access each element of the pair with k.1 and k.2 for example

[Johan Commelin]

But I am not sure if this is the right way to define this... for example, I want to prove that helpme f takes positive values if f does...

[Johan Commelin]

And I just get a goal 0 < ite ... and I have no way how to tackle that.

[Kevin Buzzard]

yeah, these CS people don't like if, I think it must be the new goto (for people old enough to remember that command)

[Johannes Hölzl]

@Johan Commelin the first step is to simplify the problem: I guess you want a function like fin n -> fin (n+1). This can be done by doing it on the naturals (see raise_fin in mathlibs data/fin.lean).

[Johannes Hölzl]

I like if and if h : the problem is that we don't have a if-splitter tactic (a tactic which looks for a if in your goal and introduces a cases for it)

[Johan Commelin]

No, I'm going in the opposite direction of raise_fin

[Johannes Hölzl]

@Johan Commelin if you see a ite and don't know how to continuous: do the case distinction by by_cases p and then rewrite using if_pos and if_neg (or if it is a dependent if then dif_neg and dif_pos).

[Johannes Hölzl]

like fin.succ?

[Johan Commelin]

No, I just want to skip one i : fin (n+1), and in this way get a function on n elements... I then collapse the domain to fin n

[Johan Commelin]

Sorry, I see that I messed up my types...

[Johan Commelin]

Let me fix it

[Johannes Hölzl]

def fin.lift {n : ℕ} (i : fin (n + 2)) (j : fin n) : fin (n + 1) :=
⟨if i.1 < j.1 then j.1 + 1 else j.1,
  begin
    by_cases (i.1 < j.1),
    { rw [if_pos h], exact (nat.succ_lt_succ j.2) },
    { rw [if_neg h], exact (nat.lt_succ_of_lt j.2) }
  end⟩

[Johannes Hölzl]

Argh, sorry wrong way around... (CORRECTED)

[Johan Commelin]

Thanks!

[Johan Commelin]

That gives me the idea on how to work with this stuff

[Johan Commelin]

I also fixed my type signature

[Johannes Hölzl]

I was working a little bit on cubes and chains (see: https://gist.github.com/johoelzl/ace6a2304b58f77a561777f6ac411647 )
I didn't yet continue it, but it might be worthwhile to use vector n R instead of fin n -> R. I'm still unsure about this...

[Johan Commelin]

In the end, I think fin n is a particularly good choice for this. Because fin n are the objects of the simplex category

[Johan Commelin]

We just need to define all the maps fin n \to fin m

[Johan Commelin]

And I am currently struggling with the incarnation in the singular chain complex...

[Johan Commelin]

Anyway, I am voting for an ite tactic. Maybe I'll try to cargo-cult it myself after I've defined singular homology.

[Kevin Buzzard]

@Johan Commelin You are running into the same sort of issues, in a broad sense, that I am currently running into. You want to model certain things (e.g. R^n) and there are several equivalent ways of doing it (e.g. lists of length n, "vector n", or an inductive definition). My impression is that it's a bit of a dark art to see which definition is "best". As mathematicians we regard all these definitions as trivially equivalent, and indeed are capable of switching between various ways of thinking about one underlying idea without ever even fussing about the details, because we all know how to switch. In this game, every time you switch then all of a sudden the lemma or definition you had in one of the contexts becomes unavailable and you either end up writing infrastructure which will help you to switch between the notions, or (and my impression is that this is what the CS people advocate) deciding what the "best" way to do it is (you see that this is the question Johannes raises -- it is far far more important for CS people than for maths people) and writing everything for this decision and then writing the functions which translate to and from other situations.

[Kevin Buzzard]

I'm now just about sufficiently competent at Lean to be able to make a really lousy decision about how to model a situation and then struggle through all the proofs I need using this model.

[Kevin Buzzard]

If you want my advice then find some mathlib functions related to what you're doing and see how a CS person does it.

[Johan Commelin]

Yes, I think I agree. (Though your problems are way bigger then mine...)

[Kevin Buzzard]

This morning I wanted to say something was compact

[Kevin Buzzard]

so I just wrote down some random definition of compact

[Kevin Buzzard]

and then wrote 100 lines of code

[Kevin Buzzard]

and then I actually wanted to use some compactness result from the library

[Kevin Buzzard]

and then found that they had a trivially equivalent but in some sense completely different way of saying "finite subcover"

[Kevin Buzzard]

and of course it's at this point that you realise that their way of doing it is mathematically equivalent but, in terms of usability, much better.

[Kevin Buzzard]

So before you write too much more code you might want to explain what you want to do and suggest some basic definitions which will be at the foundation of everything, and then see what the CS people think of them.

[Mario Carneiro]

Re: fin, I did a lot of index work like this in dioph, using fin2 for convenience. It might help to look at stuff like insert_perm and remap_left

[Johan Commelin]

Thanks!