Email Gateway (Aug 19 2022 at 15:03): Email Gateway (Aug 19 2022 at 15:03):From: Holden Lee <hl422@cam.ac.uk>
In general I can't seem to get auto/simp to check conditions thoroughly.
Here is an example.
lemma (in module) mult1:
assumes h1: "finite S" and h2: "S⊆ carrier M"
shows "(⨁⇘M⇙x∈S. 𝟭⇘R⇙⊙⇘M⇙ x) = (⨁⇘M⇙x∈S. x) "
proof -
from assms show ?thesis
........................
done
qed
I tried apply (auto cong: finsum_cong') but this doesn't work. Here, the
following does work:* apply (intro finsum_cong', auto)*. (But in more
complicated things*, if I can't use auto/simp then I'm forced to break the
problem into pieces by subgoal_tac.)
I'm confused as to why intro would be stronger than cong here (especially
since the name finsum_cong' suggests that it be used as a congruence rule).
In general what does "intro" do that auto/simp cong does not? To my
understanding, when simp wants to prove P and P appears in the conclusion
of a simp rule, it should try to prove the premises of the rule; wouldn't
this be the same as intro?
What I would imagine the simplifier does above is
(1) look at finsum_cong'
"[| A = B; g ∈ B -> carrier G;
!!i. i ∈ B ==> f i = g i |] ==> finsum G f A = finsum G g B"
and from this, try to show
(1) S=S
(2) g∈ S -> carrier M
(3) !!x∈ B ==>𝟭⇘R⇙⊙⇘M⇙ x = x
(2) should be discharged by the simp rule Pi_I'[simp]: "(!!x. x : A --> f x
: B x) ==> f : Pi A B", the fact that S⊆ carrier M, and hence that %x. x is
in S->carrier M (in fact this is another simp rule in FuncSet)
(3) should be simplified by the module axioms (declared simp).
Thanks,
Holden
*Another example ... ==>
(⨁⇘V⇙v∈S. (λv∈S. m1 v ⊕⇘K⇙ m2 v) v ⊙⇘V⇙ v) = (⨁⇘V⇙v∈S. m1 v ⊙⇘V⇙ v) ⊕⇘V⇙
(⨁⇘V⇙v∈S. m2 v ⊙⇘V⇙ v)
I pass to auto/simp a rule that combines sums over the same set provided
that the terms are in the carrier, so I would expect the RHS to be
rewritten (but it's not). There are of course also simp/intro rules for
showing that a sum of terms in carrier V is also in carrier V, and that
scalar multiplication of terms in carrier V is also in carrier V.
Here is part of the simp_trace, if it helps. (I don't know how to read it.)
[4]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
x ∈ S ⟹ ?g x ∈ carrier M ≡ ?Q'1
[4]Adding rewrite rule "??.unknown":
x ∈ S ≡ True
[3]SUCCEEDED
x ∈ S ⟶ ?g x ∈ carrier M ≡ x ∈ S ⟶ ?g x ∈ carrier M
[2]FAILED
(⋀x. x ∈ S ⟶ ?g x ∈ carrier M) ⟹ ?g ∈ S → carrier M ≡ True
[1]Congruence proof failed. Could not prove
S ≡ ?B ⟹
?g ∈ ?B → carrier M ⟹
(⋀i. i ∈ ?B ⟹ 𝟭 ⊙⇘M⇙ i ≡ ?g i) ⟹ finsum M (op ⊙⇘M⇙ 𝟭) S ≡ finsum M ?g ?B
Last updated: Apr 27 2024 at 01:05 UTC