# Zulip Chat Archive

## Stream: lean4

### Topic: mathport:wf-refl

#### Daniel Selsam (Apr 01 2021 at 15:26):

@Mario Carneiro To backport Lean4's behavior for https://github.com/dselsam/mathport/issues/20 I think you only need to change these lines in Lean3: https://github.com/leanprover-community/lean/blob/master/src/library/type_context.cpp#L715-L718 Some proofs will break though, of course.

#### Daniel Selsam (Apr 09 2021 at 17:57):

I am trying to patch https://github.com/leanprover-community/lean/blob/master/tests/lean/run/fib_wrec.lean#L26 after this change. What is best practice in lean3 for non-rfl-ing well-founded proofs?

#### Kevin Buzzard (Apr 09 2021 at 18:01):

Hah! I can't answer your question but I do know that `fib 5`

is supposed to be 5 :-)

#### Mario Carneiro (Apr 09 2021 at 18:02):

I think you should be able to prove that one by something like `repeat {rw fib, simp}`

#### Mario Carneiro (Apr 09 2021 at 18:03):

probably just delete the test

#### Daniel Selsam (Apr 09 2021 at 18:08):

Mario Carneiro said:

I think you should be able to prove that one by something like

`repeat {rw fib, simp}`

Doesn't work.

#### Daniel Selsam (Apr 09 2021 at 18:09):

Mario Carneiro said:

probably just delete the test

Since we will need to propagate this change to mathlib as well, we ought to find a robust solution.

#### Daniel Selsam (Apr 09 2021 at 18:14):

Probably best to allow `reflexivity (md := transparency.all)`

#### Mario Carneiro (Apr 10 2021 at 03:40):

Daniel Selsam said:

Mario Carneiro said:

probably just delete the test

Since we will need to propagate this change to mathlib as well, we ought to find a robust solution.

This presumes that this kind of code is typical for mathlib, and I don't think it is. We do need to propagate the change to mathlib, but we will find out what the fallout is then and it's probably not anything like this fib test

#### Mario Carneiro (Apr 10 2021 at 03:41):

Generally theorems about well founded definitions are proved by `rw`

or `simp`

with the equation coming out of the wf definition, rather than deep rfl. Or at least that's my hypothesis that needs to be tested on mathlib

#### Gabriel Ebner (Apr 30 2021 at 12:35):

I've tried porting mathlib to this change (#7264) and it's just really painful.

`dec_trivial`

breaks if the expressions contains`fin`

- Different ways of writing numerals in
`fin`

are no longer definitionally equal:`(1 : fin 2)`

,`fin.succ (0 : fin 1)`

,`((1 : ℕ) : fin 2)`

,`⟨1, one_lt_two⟩`

all mean something different.

The`fin`

problem is particularly problematic because they appear in a lot of places, and in types.

The reason this breaks is because `nat.mod`

no longer reduces in the kernel. So my proposal would be to define `nat.mod`

without well-founded recursion (and also `nat.div`

because it's in the same file). lean#570 Opinions?

#### Mario Carneiro (Apr 30 2021 at 12:39):

Seems like a good idea to me. There is an obvious bound on recursion depth, so a definition by recursion on fuel will work fine and will compute better in the kernel. `#eval`

of course replaces the definition so it doesn't matter

#### Mario Carneiro (Apr 30 2021 at 12:40):

we may also want to introduce `acc`

in type at some point

#### Gabriel Ebner (Apr 30 2021 at 12:50):

In Lean 4, this works anyhow no matter how `Nat.mod`

is defined because `Nat.mod`

is magic in the kernel.

Last updated: May 07 2021 at 13:21 UTC