# Zulip Chat Archive

## Stream: maths

### Topic: Working with `fin n` (and `ite`?)

#### Johan Commelin (May 14 2018 at 12:03):

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 (May 14 2018 at 12:04):

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 (May 14 2018 at 12:04):

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 (May 14 2018 at 12:04):

You can access each element of the pair with `k.1`

and `k.2`

for example

#### Johan Commelin (May 14 2018 at 12:05):

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 (May 14 2018 at 12:05):

And I just get a goal `0 < ite ...`

and I have no way how to tackle that.

#### Kevin Buzzard (May 14 2018 at 12:06):

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 (May 14 2018 at 12:06):

@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 `mathlib`

s `data/fin.lean`

).

#### Johannes Hölzl (May 14 2018 at 12:08):

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 (May 14 2018 at 12:08):

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

#### Johannes Hölzl (May 14 2018 at 12:08):

@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 (May 14 2018 at 12:09):

like `fin.succ`

?

#### Johan Commelin (May 14 2018 at 12:13):

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 (May 14 2018 at 12:14):

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

#### Johan Commelin (May 14 2018 at 12:14):

Let me fix it

#### Johannes Hölzl (May 14 2018 at 12:15):

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 (May 14 2018 at 12:16):

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

#### Johan Commelin (May 14 2018 at 12:16):

Thanks!

#### Johan Commelin (May 14 2018 at 12:16):

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

#### Johan Commelin (May 14 2018 at 12:19):

I also fixed my type signature

#### Johannes Hölzl (May 14 2018 at 12:21):

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 (May 14 2018 at 12:22):

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 (May 14 2018 at 12:22):

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

#### Johan Commelin (May 14 2018 at 12:22):

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

#### Johan Commelin (May 14 2018 at 12:34):

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 (May 14 2018 at 12:41):

@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 (May 14 2018 at 12:41):

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 (May 14 2018 at 12:42):

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 (May 14 2018 at 12:42):

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

#### Kevin Buzzard (May 14 2018 at 12:42):

This morning I wanted to say something was compact

#### Kevin Buzzard (May 14 2018 at 12:42):

so I just wrote down some random definition of compact

#### Kevin Buzzard (May 14 2018 at 12:42):

and then wrote 100 lines of code

#### Kevin Buzzard (May 14 2018 at 12:43):

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

#### Kevin Buzzard (May 14 2018 at 12:43):

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

#### Kevin Buzzard (May 14 2018 at 12:44):

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 (May 14 2018 at 12:45):

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 (May 14 2018 at 18:18):

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 (May 14 2018 at 19:06):

Thanks!

Last updated: May 12 2021 at 07:17 UTC