fix(data/fin): rename raise_fin -> fin.raise; simp lemmas for fin #138
Conversation
data/fin.lean
Outdated
|
|
||
| def raise (k : fin n) : fin (n + 1) := ⟨val k, lt_succ_of_lt (is_lt k)⟩ | ||
|
|
||
| def lower (k : fin (n + 1)) (h : k.val < n) : fin n := ⟨k.val, h⟩ |
There was a problem hiding this comment.
I don't think we want this function. As it is it's basically mk; I guess it would be better if it did something else with the extra element like send n to n-1 and i < n to i. But then we will probably want more control on which element to double, and then it is a different function altogether. I think the easiest thing is just to say there is no lower function.
johoelzl
changed the title
There was a problem hiding this comment.
@jcommelin do you want to incorporate the changes? They are only syntactic so I can do them too. (there is a short style guide: https://github.com/leanprover/mathlib/blob/master/docs/style.md , but it misses some things, e.g. having short attribute annotations inline...)
I usually change the title of the commits (or if it contains only one commit, the title of the PR) to follow Lean's commit convention. See:
https://github.com/leanprover/lean/blob/master/doc/commit_convention.md
data/fin.lean
Outdated
|
|
||
| variable {n : ℕ} | ||
|
|
||
| def raise (k : fin n) : fin (n + 1) := ⟨val k, lt_succ_of_lt (is_lt k)⟩ |
There was a problem hiding this comment.
please add the comment /-- Embedding of fin ninfin (n+1) -/ back.
This is a user comment, i.e. you see it a tooltip.
data/fin.lean
Outdated
| def raise (k : fin n) : fin (n + 1) := ⟨val k, lt_succ_of_lt (is_lt k)⟩ | ||
|
|
||
| @[simp] | ||
| lemma succ_val (j : fin n) : j.succ.val = j.val.succ := by cases j; simp [fin.succ] |
There was a problem hiding this comment.
The attribute annotation is inline with lemma succ_val etc.
There was a problem hiding this comment.
but the proof in a new line, i.e.
@[simp] lemma succ_val (j : fin n) : j.succ.val = j.val.succ :=
by cases j; simp [fin.succ]
data/fin.lean
Outdated
| lemma succ_val (j : fin n) : j.succ.val = j.val.succ := by cases j; simp [fin.succ] | ||
|
|
||
| @[simp] | ||
| lemma pred_val (j : fin (n+1)) (h : j ≠ 0) : (j.pred h).val = j.val.pred := by cases j; simp [fin.pred] |
There was a problem hiding this comment.
The attribute annotation is inline with lemma succ_val etc.
There was a problem hiding this comment.
but the proof in a new line, i.e.
@[simp] lemma pred_val (j : fin (n+1)) (h : j ≠ 0) : (j.pred h).val = j.val.pred :=
by cases j; simp [fin.pred]
|
@johoelzl Thanks for the feedback. I will incorporate it; it's good practice for me. Thanks for the links to the style guides. |
|
Thanks! |
No description provided.