[Merged by Bors] - feat(data/pnat/find): port over nat.find API

[pechersky]

Didn't port pnat.find_add because I got lost in the proof.

---

[eric-wieser]

To be clear, what I'm suggesting is:

/-- The `pnat` version of `nat.find_x` -/
protected def find_x : {n // p n ∧ ∀ m : ℕ+, m < n → ¬p m} :=
begin
  have : ∃ (n' : ℕ) (n : ℕ+) (hn' : n' = n), p n, from exists.elim h (λ n hn, ⟨n, n, rfl, hn⟩),
  have n := nat.find_x this,
  refine ⟨⟨n, _⟩, _, λ m hm pm, _⟩,
  { obtain ⟨n', hn', -⟩ := n.prop.1,
    rw hn',
    exact n'.prop },
  { obtain ⟨n', hn', pn'⟩ := n.prop.1,
    simp_rw [hn', subtype.coe_eta],
    exact pn' },
  { exact n.prop.2 m hm ⟨m, rfl, pm⟩, }
end

I don't really understand what you're doing with the opt_params in your version, but this avoids needing them.

[pechersky]

I don't really understand what you're doing with the opt_params in your version, but this avoids needing them.

I've found that when a definition or usage of a definition requires a proof, and we need two such proofs, where one implies the other, having both still as arguments is better, where the implication is stored in an opt_param. This opt_param laundering often works better when the statements interact with rw.

I will work on using your implementation.

[eric-wieser]

In the case of my definition you should probably never need the rewrite, as all the API for find_x is in its type alone.

[eric-wieser]

Can you add lt_add_left too for completeness? We have both for nat.

[eric-wieser]

I would guess

Suggested change

	⟨begin
	rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩,
	simp [←pnat.coe_le_coe]
	end⟩
	⟨λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, by simp [←pnat.coe_le_coe]⟩

[pechersky]

@[priority 10]
instance : covariant_class ℕ+ ℕ+ ((+)) (≤) :=
⟨λ ⟨a, ha⟩, by { extract_goal, }⟩

example (_x : ℕ+)
  (_fun_match : ∀ (_a : ℕ+) {n₁ n₂ : ℕ+},
                  n₁ ≤ n₂ → _a + n₁ ≤ _a + n₂) (a : ℕ)
  (_mlocal._fresh.304.3605 _mlocal._fresh.304.3606 : ℕ+)
  (ha : 0 < a) :
  __mlocal__fresh_304_3605 ≤ __mlocal__fresh_304_3606 →
  ⟨a, ha⟩ + __mlocal__fresh_304_3605 ≤
    ⟨a, ha⟩ + __mlocal__fresh_304_3606 :=
begin
  admit,
end

I think the destruction notation doesn't work properly with implicit arguments.

[eric-wieser]

bors d+

[bors]

✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[pechersky]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests