refactor: define List.IsChain, deprecate Chain and Chain'
#1052
Conversation
|
Mathlib CI status (docs):
|
fgdorais
added
awaiting-review
|
I'm not a fan, this turns things that would be recursive on lists into well founded recursions. |
|
What about renaming |
|
|
|
BTW, what things start using well founded recursions with my def? |
|
I'm partial to |
|
My main motivation is that we get |
|
What's wrong with using |
|
|
||
| /-- Recursion principle for `List.IsChain. -/ | ||
| @[elab_as_elim] | ||
| protected def IsChain.rec {p : ∀ l : List α, IsChain R l → Sort u} |
There was a problem hiding this comment.
Please use motive instead of p.
There was a problem hiding this comment.
Maybe add recOn for convenience? I'm not sure if casesOn would be useful but it doesn't hurt to have it.
|
|
||
| /-- Induction principle for `List.IsChain. -/ | ||
| @[elab_as_elim] | ||
| protected theorem IsChain.induction {p : ∀ l : List α, IsChain R l → Prop} |
|
|
||
| theorem IsChain.imp_of_mem (hRS : ∀ a ∈ l, ∀ b ∈ l, R a b → S a b) (h : IsChain R l) : | ||
| IsChain S l := by | ||
| induction l with |
There was a problem hiding this comment.
Wouldn't this be simpler using IsChain.rec?
|
I would like to merge this sooner than later. It looks like there's just a few small issues and a Mathlib adaptation. |
|
I'm sorry for the delay. I'll have some time to work on this tomorrow. |
No description provided.