Isabelle: proof for a equality of transposed matrix with a constant factor

Question

I am facing problems with the following lemma, which I think should be correct. I can get the proof to work up to a certain point with small steps, however I haven't found a way to proof the entire lemma.

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"
proof -
  (* here is my draft *)
  have th1: "(χ i j. transpose A $ i $ j) = (χ i j. A $ j $ i)"
    by (simp add: det_transpose transpose_def)
  have "(χ i j. if i = l then (transpose A $ i $ j) else (transpose A $ i $ j)) =
    (χ i j. A $ j $ i)" by (metis column_def row_def row_transpose)
  show ?thesis sorry
qed

Answer 1

Before even starting to prove something in Isabelle, you should know how to prove it on paper (also experienced Isabelle users do not always heed their own advice ;)). If you know how to prove it on paper, it might still not be obvious how to translate the paper proof into Isabelle/Isar. However, it would make it easier to help (and show that you understand the mathematical problem at hand, which has nothing to do with Isabelle per se).

In the following I'll explain how I would approach this kind of proof:

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"

The first thing I noted is the abstractions χ i j. .... If I would prove something about plain lambda abstractions, I would definitely want to get rid of those as a first step, e.g., in order to prove that two functions f and g are equal, I would prove that f x = g x for all x. Which is expressed in Isabelle by the rule

ext: (⋀x. ?f x = ?g x) ⟹ ?f = ?g

Since I do not know much about Multivariate_Analysis I try to find a similar rule involving χ, by

find_theorems "(χ i. ?f i) = (χ i. ?g i)"

where the first hit is what I was searching for, i.e.,

Determinants.Cart_lambda_cong: (⋀x. ?f x = ?g x) ⟹ vec_lambda ?f = vec_lambda ?g

So I start the proof by applying this rule twice (with intro rule-name, the introduction rule rule-name is applied as often as possible):

proof (intro Cart_lambda_cong)

Now I have to show that for arbitrary i and j the statement holds when substituted for the χ parameters, i.e.,

  fix i j
  show "(if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
        (if i = l then c * (A $ j $ i) else (A $ j $ i))"

Then the prove is finished by applying the definition of transpose:

    by (simp add: transpose_def)
qed

Or instead of the above step-wise proof we could do

by (auto intro!: Cart_lambda_cong simp: transpose_def)

where the ! after intro tells the system that this rule should be applied aggressively (it does not work without the !, but don't ask me why ;), we would have to check the trace of applied rules to find out).

Answer 2

Looking at the lemma reveals that transpose A $ i $ j = A $ j $ i holds for all A,i,j, which can be easily proven by the simplifier:

lemma transpose_eq: "⋀i j. transpose A $ i $ j = A $ j $ i" by (simp add: transpose_def)

If we apply this equation manually with the subst method, your lemma can be solved easily be just rewriting the branches of the if expression:

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"
  apply (subst transpose_eq)
  apply (subst transpose_eq)
  apply (rule refl)
  done

So, instead of subst we should be able to use the simplifier with apply (simp add: transpose_eq), right? The reason it does not work is due to congruence rules. Basically, the simplifier knows a rule (if_weak_cong), which explicitly forbids it to simplify the branches of an if expression (this is often a good idea to keep goals on a managable size). So we need to remove this rule:

  apply (simp add: transpose_def cong del: if_weak_cong)

solves your original lemma.

For a more in-depth answer see "Why won't Isabelle simplify the body of my "if _ then _ else" construct?".