Stream: General

Topic: When to cast and when not to cast

view this post on Zulip Craig Alan Feinstein (Sep 22 2024 at 02:45):

I'm trying to figure out the proof of lemma rpbd_incidence_matrix_cond in Fishers_Inequality.Incidence_Matrices. Notice that on some lines, int is placed before the matrices whereas on others including the statement of the theorem, int is not there. I'm wondering why. The reason I'm asking is I have a similar issue in my proof attempt of the Bruck Ryser Chowla Theorem. This theorem works with rational numbers, so casting is an issue there as well that I need to deal with. Here is the proof in the archive of formal proofs: 

lemma rpbd_incidence_matrix_cond: "N * (N⇧T) = Λ ⋅⇩m (J⇩m 𝗏) + (𝗋 - Λ) ⋅⇩m (1⇩m 𝗏)"
proof (intro eq_matI)
  fix i j
  assume ilt: "i < dim_row (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
    and jlt: "j < dim_col (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
  then have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) =
    (int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) + (int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j)"
    by simp
  then have split: "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) =
    (int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) + (𝗋 - Λ) * ((1⇩m 𝗏) $$ (i, j))"
    using ilt jlt by simp
  have lhs: "(int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) = Λ" using ilt jlt by simp
  show "(N * N⇧T) $$ (i, j) = (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j)"
  proof (cases "i = j")
    case True
    then have rhs: "(int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = (𝗋 - Λ)" using ilt by fastforce
    have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = Λ + (𝗋 - Λ)"
      using True jlt by auto
    then have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = 𝗋"
      using reg_index_lt_rep by (simp add: nat_diff_split)
    then show ?thesis using lhs split rhs True transpose_N_mult_diag ilt jlt by simp
  next
    case False
    then have "(1⇩m 𝗏) $$ (i, j) = 0" using ilt jlt by simp
    then have "(𝗋 - Λ) * ((1⇩m 𝗏) $$ (i, j)) = 0" using ilt jlt
      by (simp add: ‹1⇩m 𝗏 $$ (i, j) = 0›)
    then show ?thesis using lhs transpose_N_mult_off_diag ilt jlt False by simp
  qed
next
  show "dim_row (N * N⇧T) = dim_row (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
    using transpose_N_mult_dim(1) by auto
next
  show "dim_col (N * N⇧T) = dim_col (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
    using transpose_N_mult_dim(1) by auto
qed

view this post on Zulip Craig Alan Feinstein (Sep 22 2024 at 04:08):

Also will the "of_int" prefix tell Isabelle that it should be treated as a rational?

view this post on Zulip Mathias Fleury (Sep 22 2024 at 06:41):

Have tried to control-click on the symbol to see how the symbols of_int and int are defined and what there type is?

view this post on Zulip Craig Alan Feinstein (Sep 22 2024 at 22:17):

Yes, I tried of_nat too. of_int and of_nat seem to mean treat the variable as a rational, even though it is an integer or a natural, based on looking at examples. The actual definitions are in a lower level language that I do not comprehend at this time. And int = of_nat according to:

abbreviation int :: "nat ⇒ int"
  where "int ≡ of_nat"

view this post on Zulip Craig Alan Feinstein (Sep 22 2024 at 22:19):

I got the idea to use of_nat and of_int from the blog https://lawrencecpaulson.github.io/2022/05/04/baby-examples.html

view this post on Zulip Craig Alan Feinstein (Sep 23 2024 at 03:12):

The peculiar thing is the lemma rpbd_incidence_matrix_cond is the only lemma that uses int, yet other lemmas in the same section prove similar things without int. I don’t know why. But I bet knowing why is important.

Last updated: Dec 21 2024 at 12:33 UTC