mathport:wf-refl

Stream: lean4

[Daniel Selsam]

@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]

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]

Hah! I can't answer your question but I do know that fib 5 is supposed to be 5 :-)

[Mario Carneiro]

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

[Mario Carneiro]

probably just delete the test

[Daniel Selsam]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

we may also want to introduce acc in type at some point

[Gabriel Ebner]

In Lean 4, this works anyhow no matter how Nat.mod is defined because Nat.mod is magic in the kernel.