Hongjian Jiang (Jan 31 2024 at 23:38): Hongjian Jiang (Jan 31 2024 at 23:38):What I want to achieve is the distributive: \sum{j=1,n}. (aj * bj + aj * cj) = \sum{j=1, n}. aj * (bj + cj) . Here I abstract a b c as list.
I already defined the distributive lemma left_commute : theorem ?x ⋅ (?a + ?b) = ?x ⋅ ?a + ?x ⋅ ?b, but stuck at above proof.
type_synonym 'a vec = "'a list"
lemma "x * (a + b) = x * a + x * b"
by (simp add: local.distrib_left)
lemma c1: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n = 1 ⟹
List.fold (+) (map2 (*) r x) a + List.fold (+) (map2 (*) r y) a = List.fold (+) (map2 (*) r (map2 (+) x y)) a"
apply(simp add:vec_def) apply(induct r) apply simp apply simp apply(induct x) apply simp apply simp apply(induct y) apply auto
by (simp add: local.add.left_commute local.add_comm local.distrib_left)
lemma c2: "
List.fold (+) x a + List.fold (+) y a = List.fold (+) (x@y) a"
apply auto
by (simp add: local.add.left_commute local.fold_plus_sum_list_rev)
lemma c3: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
List.fold (+) (map2 (*) r x) a + List.fold (+) (map2 (*) r y) a = List.fold (+) ((map2 (*) r x) @ (map2 (*) r y)) a"
using c2 by presburger
lemma c4: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
length (map2 (*) r x) = length (map2 (*) r (map2 (+) x y))"
apply auto
by (simp add: vec_def)
lemma c5: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
List.fold (+) ((map2 (*) r x) @ (map2 (*) r y)) a = List.fold (+) (map2 (*) r (map2 (+) x y)) a"
apply(simp add:vec_def)
apply(induct r) apply auto apply (induct x) apply auto apply(induct y) apply auto oops
Intuitively, the proof is straightforward, but i find the problem might lie on isabelle can not expend it throughly.
Any help would be appreciated.
Yong Kiam (Feb 01 2024 at 01:22):can you post your entire theory file, including the statement you want to prove? in general, you probably shouldn't be defining your own sum unless you're doing it for learning purposes
Hongjian Jiang (Feb 01 2024 at 06:31):theory Sym_Regular_Algebra
imports "Regular_Algebras.Regular_Algebras" Matrix.Utility Matrix.Matrix_Legacy
begin
type_synonym 'a Matrix = "'a list list"
context Sr_algebra begin
definition equations :: "'a vec ⇒ 'a vec ⇒ 'a" where
"equations a b = (List.fold (+) (List.map2 (*) a b) 0)"
definition ewp_vec :: "'a vec ⇒ bool" where
"ewp_vec v = (∀i∈set v. ¬ ewp i)"
lemma "x * (a + b) = x * a + x * b"
by (simp add: local.distrib_left)
lemma c1: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n = 1 ⟹
List.fold (+) (map2 (*) r x) a + List.fold (+) (map2 (*) r y) a = List.fold (+) (map2 (*) r (map2 (+) x y)) a"
apply(simp add:vec_def) apply(induct r) apply simp apply simp apply(induct x) apply simp apply simp apply(induct y) apply auto
by (simp add: local.add.left_commute local.add_comm local.distrib_left)
lemma c2: "
List.fold (+) x a + List.fold (+) y a = List.fold (+) (x@y) a"
apply auto
by (simp add: local.add.left_commute local.fold_plus_sum_list_rev)
lemma c3: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
List.fold (+) (map2 (*) r x) a + List.fold (+) (map2 (*) r y) a = List.fold (+) ((map2 (*) r x) @ (map2 (*) r y)) a"
using c2 by presburger
lemma c4: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
length (map2 (*) r x) = length (map2 (*) r (map2 (+) x y))"
apply auto
by (simp add: vec_def)
lemma c5: "vec n r ⟹ vec n x ⟹ vec n y ⟹ n > 1 ⟹
List.fold (+) ((map2 (*) r x) @ (map2 (*) r y)) a = List.fold (+) (map2 (*) r (map2 (+) x y)) a"
apply(simp add:vec_def)
apply(induct r) apply auto apply (induct x) apply auto apply(induct y) apply auto oops
end
What I am trying to prove is lemma "vec n a ⟹ vec n l ⟹ mat n n m1 ⟹ n > 0 ⟹ ∀i∈set [0..<n]. equations a (m1!i) + l!i = a!i ⟹ ∀i∈set [0..<n]. ewp_vec (col m2 i) ⟹
vec n b ⟹ vec n l ⟹ mat n n m2 ⟹ n > 0 ⟹ ∀i∈set [0..<n]. equations b (m2!i) + l!i = b!i ⟹ ∀i∈set [0..<n]. ewp_vec (col m1 i) ⟹ ∀i∈set [0..<n]. a!i = b!i". So I have to split it into small cases. Is there any usual way to use the sum operator?
Mathias Fleury (Feb 01 2024 at 06:54):Intuitively, the proof is straightforward, but i find the problem might lie on isabelle can not expend it throughly.
Then I must have a very different intuition how such a proof would look like, because it very much looks like what I expected:
lemma fold_0: ‹NO_MATCH 0 a ⟹ fold (+) (xs) a = fold (+) (xs) 0 + a›
apply (induction xs arbitrary: a)
apply simp
by (metis local.add_zeror local.fold_plus_sum_list_rev)
lemma c5:
shows "vec n r ⟹ vec n x ⟹ vec n y ⟹ List.fold (+) (map2 (*) r (map2 (+) x y)) a = List.fold (+) ((map2 (*) r x) @ (map2 (*) r y)) a"
apply (induction x arbitrary: n a y r)
subgoal by (auto simp: vec_def)
subgoal premises H for x xs m a ys rs
using H(1)[of ‹m-1› ‹tl ys› ‹tl rs›] H(2-)
apply (cases ys; cases rs)
apply (auto simp add: fold_0 c3 vec_def semigroup.assoc[OF local.add.semigroup_axioms])
by (smt (verit) H(1) c2 local.add_comm local.distrib_left semigroup.assoc[OF local.add.semigroup_axioms] vec_def)
done
(I was too lazy to find out what ac_simps rules apply in this algebra, so I used the very slow smt call)
Mathias Fleury (Feb 01 2024 at 06:55):And simp followed by induct is considered bad practice
Mathias Fleury (Feb 01 2024 at 08:44):And @Yong Kiam 's suggestion is to use the already existing:
definition equations :: "'a vec ⇒ 'a vec ⇒ 'a" where
"equations a b = sum_list (List.map2 (*) a b)"
which is the best choice
Hongjian Jiang (Feb 01 2024 at 09:22):Thanks a lot. It works for me enough. Another question is which would be good practice if not use induct tactic
Yong Kiam (Feb 01 2024 at 09:29):I think @Mathias Fleury meant not to use induct right after a simp -- just start your proof with induct. The reason for this is that it will be much easier to trace the induction (after simp, the proof state might be very different)
Hongjian Jiang (Feb 01 2024 at 09:33):ah, I see. Thanks
Yong Kiam (Feb 01 2024 at 09:35):BTW, the better option might be to use a newer matrix library in which the vector dot product is defined
text ‹This theory is marked as legacy, since there is a better
implementation of matrices available in @{file ‹../Jordan_Normal_Form/Matrix.thy›}.
That formalization is more abstract, more complete in terms of operations,
and it still provides an efficient implementation.›
I will try this way, using vector dot product is exactly what I need in the lemma. Thank
Hongjian Jiang (Feb 01 2024 at 13:34):Sorry to ask question again, I was stuck at lemma m9: shows "vec n r ⟹ vec n x ⟹ (sum_list (map2 (*) r x)) * z= sum_list ((map2 (*) r (map (λr. r * z) x)))" this lemma
Yong Kiam (Feb 01 2024 at 13:46):I believe this will again be solved if you use the newer matrix library which knows about the laws for scalar multiplication
Mathias Fleury (Feb 01 2024 at 13:48):I am unconvinced that the newer library will help. I am sure that it is better, but this proof is not hard at all:
lemma m9: shows "(sum_list (map2 (*) r x)) * z= sum_list ((map2 (*) r (map (λr. r * z) x)))"
apply (induction x arbitrary: r)
subgoal by auto
subgoal for a x r
by (cases r) (auto simp: ac_simps)
done
From this thread, I have the impression that you do not know what arbitrary is
Hongjian Jiang (Feb 01 2024 at 13:51):yes, I read the document which says that arbitrary is used to generalize. But don't know how to use it exactly
Yong Kiam (Feb 01 2024 at 13:56):have you worked through "Programming and Proving in Isabelle/HOL"? this is covered by that, for example
Hongjian Jiang (Feb 01 2024 at 13:58):I have impressions about one example there, which generalized a fix value to arbitraray variable. But is there any tricks to choose which variable needs to be generalized? Like above lemma, x and r are both list, why induct on x and arbitrary on r. Thanks.
Yong Kiam (Feb 01 2024 at 13:59):that comes from experience, maybe @Mathias Fleury has some heuristic in this case (although I think inducting on either should work fine here)
Hongjian Jiang (Feb 01 2024 at 14:07):Thanks, Yong. Maybe need to write more isabelle code to get such skill
Mathias Fleury (Feb 01 2024 at 14:08):r is a dummy list, while x is the list you are manipulating with the *z. So I picked x (although I believe both work)
Last updated: Apr 28 2024 at 01:11 UTC