Stream: General

Topic: Questions about "fix"


view this post on Zulip Craig Alan Feinstein (Mar 23 2025 at 22:14):

I haven't really used Isabelle heavily since last year and I'm just getting back into it now. The good news is I've learned so much since the summer of last year. Last year, someone in Zulip recommended the "fix" operator. I tried using it here but I got a "linarith_split_limited exceeded" error after the last line "by auto":

lemma brc_v_1_mod_4:
      assumes "𝗏 mod 4 = 1"
        shows "βˆƒx :: rat mat.(βˆ‘j ∈ {4..<5}.
               ((βˆ‘h ∈ {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
               (βˆ‘h ∈ {5..<𝗏}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
                of_nat Ξ› * (βˆ‘j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
                of_nat (𝗄 - Ξ›) * (βˆ‘j ∈ {4..<5}. (x $$ (4-j, 0))^2)"
proof -
  obtain a b c d where lag_eq:
    "a^2 + b^2 + c^2 + d^2 = 𝗄 - Ξ›"
    using blocksize_gt_index sum_of_four_squares by metis

  fix m :: "nat"
  fix n :: "nat"
  fix h :: "nat"
  fix i :: "nat"
  fix j :: "nat"
  fix x :: "rat mat"
  fix x0 :: "rat"
  fix x1 :: "rat"
  fix x2 :: "rat"
  fix x3 :: "rat"
  fix y0 :: "rat"
  fix y1 :: "rat"
  fix y2 :: "rat"
  fix y3 :: "rat"

  assume assm1: "𝗏 β‰₯ m" "m > 3" "x0 = x $$ (m-4,0)"
          "x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
          "x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
  assume assm2: "m + 4*n = 𝗏"

    have "βˆƒe0 e1 e2 e3 :: rat.(βˆ‘h ∈ {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
          e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
          (βˆ‘h ∈ {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"
      using linear_comb_of_y_part_2_i3 assm1 lag_eq by auto

Any ideas what could be causing this?

The lemma being used in brc_v_1_mod_4 is the following, which was successfully proven:

lemma linear_comb_of_y_part_2_i3:
  assumes "a ∈ β„•" "b ∈ β„•" "c ∈ β„•" "d ∈ β„•"
          "x0 ∈ β„š" "x1 ∈ β„š" "x2 ∈ β„š" "x3 ∈ β„š"
          "a^2 + b^2 + c^2 + d^2 = (𝗄 - Ξ›)"
          "x ∈ rat mat" "𝗏 β‰₯ m" "m > 3" "i ∈ {0..<4}" "x0 = x $$ (m-4,0)"
          "x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
          "x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "y0 ∈ β„š" "y1 ∈ β„š" "y2 ∈ β„š" "y3 ∈ β„š"
  shows "βˆƒe0 e1 e2 e3 :: rat.(βˆ‘h ∈ {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
    e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
    (βˆ‘h ∈ {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"

Another question is what are the advantages of using fix instead of assume? As I recall, one of the experts in Zulip said I should be using fix instead of assume. Could the problem be I should have used fix in linear_comb_of_y_part_2_i3 instead of assume?

view this post on Zulip Mathias Fleury (Mar 24 2025 at 05:46):

fix is just a way to fix a variable. So this:

 fix m :: "nat"
assume assm1: "𝗏 β‰₯ m"

just means "let

m∈Nm \in \mathbb{N}

such that

𝗏β‰₯m.𝗏 β‰₯ m.

So the question is not "should I use fix". The question is "how does my proof look like on paper?"

view this post on Zulip Mathias Fleury (Mar 24 2025 at 05:48):

In a proof by hand you would never write an assume in a middle of a proof. So you should not do it in Isabelle either.

view this post on Zulip Mathias Fleury (Mar 24 2025 at 05:48):

Remark that

"x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"

look like definitions and not assumptions

view this post on Zulip Craig Alan Feinstein (Mar 24 2025 at 16:09):

Mathias, so all this is just cosmetic? I was hoping this would lead me to figure out why my proof isn’t working. In any case how would you rewrite the assume part in the middle of my proof so it looks cosmetically better?

view this post on Zulip irvin (Mar 24 2025 at 17:24):

I believe that unless you provide a method for others to run your proofs. It would be extremely hard for others to figure out modify/fix your proofs.

view this post on Zulip Mathias Fleury (Mar 24 2025 at 18:59):

it is not a question about cosmetic. It is a question about how the proofs.

view this post on Zulip Mathias Fleury (Mar 24 2025 at 19:00):

On paper, you would never write in the middle a proof "oh and here let's assume that v >= 4".

view this post on Zulip Mathias Fleury (Mar 24 2025 at 19:00):

You need to justify why you can do that

view this post on Zulip Mathias Fleury (Mar 24 2025 at 19:01):

and one why to do that is to say: oh let's just give a name to this thing

view this post on Zulip Mathias Fleury (Mar 24 2025 at 19:01):

this is not an assumption

view this post on Zulip Mathias Fleury (Mar 24 2025 at 19:02):

But, Isabelle is not here to tell you how to do a proof, it is here to check the proof. You have to do the creative part of deciding how to do the proof.

view this post on Zulip Craig Alan Feinstein (Mar 24 2025 at 22:37):

Irvin, even though it looks complicated, the proof of brcv1mod4 follows from the other lemma by modes ponens. But I am having trouble getting Isabelle to recognize this.

view this post on Zulip Craig Alan Feinstein (Mar 24 2025 at 23:14):

Mathias I am putting inside the proof assumptions about variables that are not defined in the actual statement of the lemma. But they are necessary for proving existence in the lemma statement. How would you do this? By the way, this is all part of the last part of the standard proof of the Bruck Ryser Chowla theorem. This isn’t my proof. I’m just trying to translate it into Isabelle.

view this post on Zulip Mathias Fleury (Mar 25 2025 at 02:50):

A lot of the literature looks like a proof but needs improvement to have a proper proof

view this post on Zulip Mathias Fleury (Mar 25 2025 at 02:53):

So in your case:

But they are necessary for proving existence in the lemma statement.

Why can you assume them? Obviously you cannot assume False in the middle of a proof. So there must be some argument why you can do that

view this post on Zulip Mathias Fleury (Mar 25 2025 at 02:58):

My guess is that:

1. x0 to x4 are actually definitions "x0 = x $$ (m-4,0)" "x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)" (keyword in Isabelle: defines… and you do not need a proof to define things!)
2. m and n are actually value you can obtain from 𝗏 mod 4 = 1 but you pick values such that m>3 intead of the smallest values (keyword in Isabelle: obtain… and you need a proof!)
3. From 1 you can prove that the alternative definition with one_of ... four_of hold (keyword in Isabelle: have… and you need a proof und will use x0_def ... x4_def)

view this post on Zulip Mathias Fleury (Mar 25 2025 at 03:00):

And if I am correct, something just happened: none of the things are assume in the middle of a proof. They have a proper justification. And none of the things are new fresh variables in the middle of a proof that need a fix.

view this post on Zulip Craig Alan Feinstein (Mar 25 2025 at 16:02):

The lemma claims there exist rational numbers which satisfy the equation- v and k and Lambda are properties of the symmetric design. The variables that are assumed and fixed are used to construct the solution.

view this post on Zulip Craig Alan Feinstein (Mar 25 2025 at 16:21):

Are there any other similar existence theorems in Isabelle?

view this post on Zulip irvin (Mar 25 2025 at 17:12):

Here are some examples of using define and obtain.

lemma DEFINE:
  assumes n_def:"(n :: nat) = 2"
  shows "βˆƒy. y * 2 = n"
proof -
  define y where y_def: "(y ::nat) = 1"
  then have "y * 2 = n"
    using y_def n_def by simp
  then show "βˆƒy. y * 2 = n"
    by auto

qed

lemma OBTAIN:
  assumes "βˆƒy. P y"
  shows "βˆƒx. P x"
proof -
  obtain y where  " P y "
    using assms by auto
  then show "βˆƒx. P x"
    by auto
qed

Define requires no proof, obtain requires a proof

view this post on Zulip irvin (Mar 25 2025 at 17:14):

Craig Alan Feinstein said:

The lemma claims there exist rational numbers which satisfy the equation- v and k and Lambda are properties of the symmetric design. The variables that are assumed and fixed are used to construct the solution.

in isabelle it would roughly be.

obtain rat1 rat2 rat3 where "property1" "property2"
by proof_method

view this post on Zulip Mathias Fleury (Mar 25 2025 at 19:01):

I would suggest starting with an Isabelle tutorial like the prog-prove (the beginning of the concrete semantics)

view this post on Zulip Craig Alan Feinstein (Mar 25 2025 at 23:06):

Irvin and Mathias, thank you that gives me something to work with.

view this post on Zulip Craig Alan Feinstein (Mar 26 2025 at 00:18):

I just tried the following:

lemma brc_v_1_mod_4:
      assumes "𝗏 mod 4 = 1"
        shows "βˆƒx :: rat mat.(βˆ‘j ∈ {4..<5}.
               ((βˆ‘h ∈ {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
               (βˆ‘h ∈ {5..<𝗏}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
                of_nat Ξ› * (βˆ‘j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
                of_nat (𝗄 - Ξ›) * (βˆ‘j ∈ {4..<5}. (x $$ (4-j, 0))^2)"
proof -
  obtain a b c d where lag_eq:
    "a^2 + b^2 + c^2 + d^2 = 𝗄 - Ξ›"
    using blocksize_gt_index sum_of_four_squares by metis

  fix m :: "nat"
  fix n :: "nat"
  fix i :: "nat"
  fix x :: "rat mat"
  define x0 where "(x0 :: rat) = x $$ (m-4,0)"
  define x1 where "(x1 :: rat) = x $$ (m-3,0)"
  define x2 where "(x2 :: rat) = x $$ (m-2,0)"
  define x3 where "(x3 :: rat) = x $$ (m-1,0)"
  define n where "(n :: nat) = (𝗏 - m) div 4"

  fix y0 :: "rat"
  fix y1 :: "rat"
  fix y2 :: "rat"
  fix y3 :: "rat"

  assume assm1: "𝗏 β‰₯ m" "m > 3" "i ∈ {0..<4}"
          "x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"

    have "βˆƒe0 e1 e2 e3 :: rat.(βˆ‘h ∈ {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
          e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
          (βˆ‘h ∈ {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"
      using linear_comb_of_y_part_2_i3 assm1 lag_eq by auto

Unfortunately, I got a "linarith_split_limit exceeded (current value is 9)" error repeated. The last have statement should follow from "linear_comb_of_y_part_2_i3" in the first post of this thread. It is just modes ponens.

view this post on Zulip irvin (Mar 26 2025 at 02:42):

You're still assuming stuff that I assume you should be proving.
This bit should be have

          "x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
          "x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"

view this post on Zulip irvin (Mar 26 2025 at 04:57):

In fact brc_v_1_mod_4 should not be using any assume keyword in the whole proof block

view this post on Zulip Mathias Fleury (Mar 26 2025 at 05:40):

BTW isn't linarith_split_limit exceeded just a warning?

view this post on Zulip Craig Alan Feinstein (Mar 26 2025 at 15:58):

Mathias, linarith split limit exceeded was something that kept repeating itself to the point where I couldn’t tell what was happening. When I had my Isabelle in front of me last night I got a purple highlight over auto meaning it was still running without stopping.

view this post on Zulip Craig Alan Feinstein (Mar 26 2025 at 16:09):

Irvin the four equations that you posted are definitely assumptions. Or perhaps better to say definitions, but I don’t know how to make them definitions.

view this post on Zulip Mathias Fleury (Mar 26 2025 at 19:30):

Craig Alan Feinstein said:

Mathias, linarith split limit exceeded was something that kept repeating itself to the point where I couldn’t tell what was happening. When I had my Isabelle in front of me last night I got a purple highlight over auto meaning it was still running without stopping.

could be that the arith simplifier is spamming the interface with messages

view this post on Zulip Mathias Fleury (Mar 26 2025 at 19:36):

Craig Alan Feinstein said:

Irvin the four equations that you posted are definitely assumptions. Or perhaps better to say definitions, but I don’t know how to make them definitions.

One last try: in the world of math I know where proofs are sequences of applications of theorems and axioms, there are no assumptions in the middle of a proof. Never. It just does not make sense.

Apparently we cannot agree on that. Therefore, we cannot help you.

view this post on Zulip Craig Alan Feinstein (Mar 26 2025 at 22:45):

Mathias I am not here to argue with you, but learn from you. But I am coming from the perspective that you can say β€œassume” in a math proof. I learned this as a college freshman from a course in logic - if you want to prove that A implies B, then you can do this by assuming A and then proving B. In the case of the proof of the Bruck Ryser Chowla theorem, the idea is to prove a certain equation 1 has an rational solution. This is done by assuming that the variables in equation 2 satisfy certain conditions and then showing by induction that these conditions lead to a solution in equation 1. This is why I was using assume in the proof. But I really don’t care if you call what I am doing assume or something else. I just want my Isabelle proof to work.

view this post on Zulip Mathias Fleury (Mar 27 2025 at 05:38):

if you want to prove that A implies B, then you can do this by assuming A and then proving B

When you prove that theorem yes. When you use that theorem no. When you use it, you show that A holds. And from this you derive B.

And here you are clearly trying to use it. You even using the keyword using linear_comb_of_y_part_2_i3.

view this post on Zulip irvin (Mar 27 2025 at 15:01):

Also note that its safe to assume .../ without loss of generality assume ... needs to be justified in isabelle.

view this post on Zulip Craig Alan Feinstein (Mar 27 2025 at 16:17):

Ok, now I understand where you are coming from. I have to think about this.

view this post on Zulip Craig Alan Feinstein (Mar 28 2025 at 00:03):

Before today, I thought your arguments were irrelevant semantic arguments. Now I see that yes they are semantic arguments but not irrelevant because in Isabelle, everything is semantics. I reread what you wrote and they make sense now. Thank you.

view this post on Zulip Craig Alan Feinstein (Apr 03 2025 at 02:45):

I've gotten to this point:

lemma brc_v_1_mod_4:
      assumes "𝗏 mod 4 = 1"
        shows "βˆƒx :: rat mat.(βˆ‘j ∈ {4..<5}.
               ((βˆ‘h ∈ {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
               (βˆ‘h ∈ {5..<𝗏}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
                of_nat Ξ› * (βˆ‘j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
                of_nat (𝗄 - Ξ›) * (βˆ‘j ∈ {4..<5}. (x $$ (4-j, 0))^2)"
proof -
  obtain a b c d where lag_eq:
    "a^2 + b^2 + c^2 + d^2 = 𝗄 - Ξ›"
    using blocksize_gt_index sum_of_four_squares by metis

  fix h :: "nat"
  fix i :: "nat"
  fix j :: "nat"
  obtain m where "𝗏 β‰₯ m" "m > 3"
    using assms t_design_min_v by force
  define n where "n = (𝗏-m) div 4"
  fix y0 :: "rat"
  fix y1 :: "rat"
  fix y2 :: "rat"
  fix y3 :: "rat"
  fix x0 :: "rat"
  fix x1 :: "rat"
  fix x2 :: "rat"
  fix x3 :: "rat"
  obtain x where "x $$ (m-4,0) = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-3,0) = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-2,0) = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-1,0) = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
    by simp
  define x0 where "x0 = x $$ (m-4,0)"
  define x1 where "x1 = x $$ (m-3,0)"
  define x2 where "x2 = x $$ (m-2,0)"
  define x3 where "x3 = x $$ (m-1,0)"

The problem with it is I want x to be a rat mat but I'm not sure how to use the obtain statement to do this.

view this post on Zulip Mathias Fleury (Apr 03 2025 at 04:37):

obtain x :: "rat mat" where …

view this post on Zulip Craig Alan Feinstein (Apr 03 2025 at 12:37):

Thanks!

view this post on Zulip Craig Alan Feinstein (Apr 04 2025 at 00:41):

Irvin was right before when he said I would have to justify it in some way. I'm not sure what kind of justification it needs though. The function is a rational function, so the definition works. Perhaps that is the answer?

view this post on Zulip irvin (Apr 04 2025 at 01:52):

Yup that is "proved" by type inference.

view this post on Zulip Craig Alan Feinstein (Apr 04 2025 at 22:44):

Do you just say β€œusing functionname” or β€œusing functionnames”?

view this post on Zulip Craig Alan Feinstein (Apr 04 2025 at 22:46):

Or something like that?

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 00:37):

I looked up "type inference" but couldn't find anything that would solve the problem. Then I tried:

  have one: "one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3))) ∈ β„š"
    by simp
  have two: "two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3))) ∈ β„š"
    by simp
  have three: "three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3))) ∈ β„š"
    by simp
  have four: "four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3))) ∈ β„š"
    by simp
  obtain x :: "rat mat" where "x $$ (m-4,0) = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-3,0) = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-2,0) = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
                 "x $$ (m-1,0) = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
    using one two three four by simp

but Isabelle didn't accept any of the sentences. Any ideas?

view this post on Zulip Mathias Fleury (Apr 09 2025 at 06:26):

For one to four I would expect that these numbers are automatically rational numbers because of the type, but it is hard to know without any definition.
For x define x as the matrix (or the vector) with the 4 elements instead of talking about the elements directly

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 12:32):

What do you mean β€œwith the four elements”? The matrix is supposed to be an m by 1 matrix. (I found that Isabelle liked it better when it was a matrix instead of a vector.)

one, two, three, four are just looking at the first, second, third, fourth elements of a vector while y_inv_of is just a linear transformation of a four element vector. There are only rational numbers in the definitions of the functions.

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 22:05):

I just tried:

  fix h :: "nat"
  fix i :: "nat"
  fix j :: "nat"
  obtain m where assm1: "𝗏 β‰₯ m" "m > 3"
    using assms t_design_min_v by force
  define n where "n = (𝗏-m) div 4"
  fix y0 :: "rat"
  fix y1 :: "rat"
  fix y2 :: "rat"
  fix y3 :: "rat"
  fix x0 :: "rat"
  fix x1 :: "rat"
  fix x2 :: "rat"
  fix x3 :: "rat"
  define x0 where "x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
  define x1 where "x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
  define x2 where "x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
  define x3 where "x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
  obtain x :: "rat mat" where
                 "x $$ (m-4,0) = x0"
                 "x $$ (m-3,0) = x1"
                 "x $$ (m-2,0) = x2"
                 "x $$ (m-1,0) = x3"
    by simp

with no luck. simp didn't work as well as sledgehammer.

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 22:07):

The function definitions are:

fun y_inv_reversible ::"((nat Γ— nat Γ— nat Γ— nat) Γ— (rat Γ— rat Γ— rat Γ— rat)) β‡’
             ((nat Γ— nat Γ— nat Γ— nat) Γ— (rat Γ— rat Γ— rat Γ— rat))" where
  "y_inv_reversible((a, b, c, d),(y0, y1, y2, y3)) = ((a, b, c, d),
  ((of_nat a)*y0 - (of_nat b)*y1 - (of_nat c)*y2 - (of_nat d)*y3)/of_nat(a^2 + b^2 + c^2 + d^2),
  ((of_nat b)*y0 + (of_nat a)*y1 + (of_nat d)*y2 - (of_nat c)*y3)/of_nat(a^2 + b^2 + c^2 + d^2),
  ((of_nat c)*y0 + (of_nat a)*y2 + (of_nat b)*y3 - (of_nat d)*y1)/of_nat(a^2 + b^2 + c^2 + d^2),
  ((of_nat d)*y0 + (of_nat c)*y1 + (of_nat a)*y3 - (of_nat b)*y2)/of_nat(a^2 + b^2 + c^2 + d^2))"

fun y_inv_of :: "((nat Γ— nat Γ— nat Γ— nat) Γ— (rat Γ— rat Γ— rat Γ— rat)) β‡’
                  (rat Γ— rat Γ— rat Γ— rat)" where
  "y_inv_of((a, b, c, d),(y0, y1, y2, y3)) =
   rightside(y_inv_reversible((a, b, c, d),(y0, y1, y2, y3)))"

fun one_of :: "(rat Γ— rat Γ— rat Γ— rat) β‡’ rat" where
  "one_of(y0, y1, y2, y3) = y0"

fun two_of :: "(rat Γ— rat Γ— rat Γ— rat) β‡’ rat" where
  "two_of(y0, y1, y2, y3) = y1"

fun three_of :: "(rat Γ— rat Γ— rat Γ— rat) β‡’ rat" where
  "three_of(y0, y1, y2, y3) = y2"

fun four_of :: "(rat Γ— rat Γ— rat Γ— rat) β‡’ rat" where
  "four_of(y0, y1, y2, y3) = y3"

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 22:44):

Also this should probably be used so that a^2 + b^2 + c^2 + d^2 != 0:

  obtain a b c d where lag_eq:
    "a^2 + b^2 + c^2 + d^2 = 𝗄 - Ξ›"
    using blocksize_gt_index sum_of_four_squares by metis

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 22:46):

Would anybody be interested in looking at my whole proof? I'm on the last hard-to-prove lemma and I've been stuck on it for a long time. When it gets done, it will be a nice addition to the AFP library.

view this post on Zulip Craig Alan Feinstein (Apr 09 2025 at 23:03):

Or are there any examples out there like this that I can look at and learn from?

view this post on Zulip Mathias Fleury (Apr 10 2025 at 04:24):

Craig Alan Feinstein said:

What do you mean β€œwith the four elements”? The matrix is supposed to be an m by 1 matrix. (I found that Isabelle liked it better when it was a matrix instead of a vector.)

one, two, three, four are just looking at the first, second, third, fourth elements of a vector while y_inv_of is just a linear transformation of a four element vector. There are only rational numbers in the definitions of the functions.

It is very strange to me to have a matrix m x 1 where you care only about 4 values

view this post on Zulip Mathias Fleury (Apr 10 2025 at 04:25):

But anyway, if you do not care about the value, you could pick one

view this post on Zulip Mathias Fleury (Apr 10 2025 at 04:28):

So you could define x as:

mat m 1 (%i j.
   if j=0 then
      if i = m-4  then x0 else if i = m-3 then x1 else if i = m-2 then x2 else if i =m-1 then x3
      else 0
   else 0)

view this post on Zulip Mathias Fleury (Apr 10 2025 at 04:28):

Here I picked 0, but any real number would do

view this post on Zulip Craig Alan Feinstein (Apr 10 2025 at 12:16):

Thank you, I’ll give that a shot.

view this post on Zulip Craig Alan Feinstein (Apr 11 2025 at 01:22):

I tried

define x :: mat m 1 where  "x = (Ξ»i j.
     if j = 0 then
       if i = m - 4 then x0
       else if i = m - 3 then x1
       else if i = m - 2 then x2
       else if i = m - 1 then x3
       else 0
     else 0)"

but it didn't like it.

view this post on Zulip Mathias Fleury (Apr 11 2025 at 06:57):

I have never used any matrices, but this:

define x :: "rat mat" where  "x = mat m 1 (Ξ»i j.
     if j = 0 then
       if i = m - 4 then x0
       else if i = m - 3 then x1
       else if i = m - 2 then x2
       else if i = m - 1 then x3
       else 0
     else 0)"

is what I meant…

view this post on Zulip Craig Alan Feinstein (Apr 11 2025 at 09:21):

Thank you, I’ll try that

view this post on Zulip Craig Alan Feinstein (Apr 11 2025 at 18:56):

I just tried it but it didn't accept it. It said,

"Type unification failed: Clash of types "nat" and "_ Γ— _"

Type error in application: incompatible operand type

Operator: mat m 1 :: (nat Γ— nat β‡’ ??'a) β‡’ ??'a mat
Operand:
Ξ»i j. if j = 0
then if i = m - 4 then x0 else if i = m - 3 then x1 else if i = m - 2 then x2 else if i = m - 1 then x3 else 0
else 0 ::
nat β‡’ ??'b β‡’ rat

Coercion Inference:

Local coercion insertion on the operand failed:
No coercion known for type constructors: "prod" and "nat""

view this post on Zulip Jan van BrΓΌgge (Apr 11 2025 at 22:40):

Change Ξ»i j to Ξ»(i, j).. The error tells you that map m 1 expects a function that takes a tuple.

view this post on Zulip Craig Alan Feinstein (Apr 15 2025 at 02:06):

Jan, thank you, I just tried that and it worked.


Last updated: Apr 26 2025 at 12:36 UTC