Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(data/rat/basic): Add nat num and denom inv lemmas #8581

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(data/rat/basic): Add nat num and denom inv lemmas #8581

Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b5a3e79
feat(rat.basic): Add nat num and denom inv lemmas
FrickHazard Aug 8, 2021
6a2c2c9
Update lemmas names to inv_coe_nat_num and inv_coe_nat_denom
FrickHazard Aug 9, 2021
97a7fe6
Add inv_coe_int_denom and inv_coe_int_num and golf nat proofs.
FrickHazard Aug 11, 2021
eefcac9
whitespace
eric-wieser Aug 11, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 20 additions & 0 deletions src/data/rat/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -744,6 +744,26 @@ begin
coe_nat_div_self]
end

lemma inv_coe_nat_num {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 :=
begin
rw [rat.inv_def', rat.coe_nat_num, rat.coe_nat_denom],
suffices : (((1 : ℤ) : ℚ) / (a : ℤ)).num = 1,
exact_mod_cast this,
apply num_div_eq_of_coprime,
{ assumption_mod_cast },
{ simp only [nat.coprime_one_left_iff, int.nat_abs_one] }
end
Copy link
Member

@eric-wieser eric-wieser Aug 10, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this proof is simpler if you prove it for int first:

Suggested change
lemma inv_coe_nat_num {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 :=
begin
rw [rat.inv_def', rat.coe_nat_num, rat.coe_nat_denom],
suffices : (((1 : ℤ) : ℚ) / (a : ℤ)).num = 1,
exact_mod_cast this,
apply num_div_eq_of_coprime,
{ assumption_mod_cast },
{ simp only [nat.coprime_one_left_iff, int.nat_abs_one] }
end
lemma inv_coe_int_num {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 :=
begin
rw [rat.inv_def', rat.coe_int_num, rat.coe_int_denom, nat.cast_one, ←int.cast_one],
apply num_div_eq_of_coprime ha0,
rw int.nat_abs_one,
exact nat.coprime_one_left _,
end
lemma inv_coe_nat_num {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 :=
inv_coe_int_num (by exact_mod_cast ha0 : 0 < (a : ℤ))

Can you do the same for the lemma below?

Copy link
Collaborator Author

@FrickHazard FrickHazard Aug 11, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, thanks for the feedback! I updated your golf and added inv_coe_int_denom. The nat version of the proof uses an additional exact_mod_cast, because of casting the denom, which is a nat.


lemma inv_coe_nat_denom {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.denom = a :=
begin
rw [rat.inv_def', rat.coe_nat_num, rat.coe_nat_denom],
suffices : ((((1 : ℤ) : ℚ) / (a : ℤ)).denom : ℤ) = a,
exact_mod_cast this,
apply denom_div_eq_of_coprime,
{ assumption_mod_cast },
{ simp only [nat.coprime_one_left_iff, int.nat_abs_one] },
end

protected lemma «forall» {p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b) :=
⟨λ h _ _, h _,
λ h q, (show q = q.num / q.denom, from by simp [rat.div_num_denom]).symm ▸ (h q.1 q.2)⟩
Expand Down