feat: Add proof to proof_wanted theorems of Array get?_size and get?_push #412
Conversation
Std/Data/Array/Lemmas.lean
Outdated
| · next hne => simp only [getElem?, size_push] | ||
| split <;> split <;> try simp only [*, get_push_lt] | ||
| · next p q => have tmp := Nat.le_of_lt_succ p | ||
| apply Or.elim (Nat.eq_or_lt_of_le tmp) <;> assumption | ||
| · next p q => exact p (Nat.lt.step q) |
There was a problem hiding this comment.
Please just two extra space when adding indenting: no need to line up with anything on the previous line.
There was a problem hiding this comment.
(Newlines immediately after => are also good.)
There was a problem hiding this comment.
Is that really a good simp lemma, with the if-then-else on the other side? It kinda blows up the term.
My (incomplete, tainted by Isabelle's simp) intuition is that you'd want the conditional two lemmas above as simp lemmas, if any at all?
There was a problem hiding this comment.
Here, trichotomy of Nat is needed, but it's tricky to derive that from very limited theorems from lean4 itself.
Thus, I just called split all the way and then looked for contradictions.
Only split / simp only / exact / rw are used. So, it won't blow up the term, right?
There was a problem hiding this comment.
Sorry, I wasn't clear, I'm wondering if the @[simp] annotation is a good default
There was a problem hiding this comment.
I see. I have no idea about that.
There was a problem hiding this comment.
In that case maybe just leave it out in this PR
There was a problem hiding this comment.
Sorry, I misread the diff, the @[simp] is on the, well, simpler theorem. All good then :-)
fgdorais
added
the
awaiting-review
joehendrix
added
will-merge-soon
No description provided.