Artem Khovanov (Aug 30 2023 at 19:16): Artem Khovanov (Aug 30 2023 at 19:16):Is it possible to instantiate a (type)class within a proof? The "instantiation" and "instance" keywords do not work. If not, how can I work around this?
Here is an MWE showing the kind of thing I am trying to do:
theory Scratch imports Main
begin
typedef (overloaded) 'a ps = "{f::nat ⇒ 'a ::{zero}. True}"
morphisms nth Abs
by blast
setup_lifting type_definition_ps
instantiation ps :: ("{plus,zero}") plus
begin
lift_definition plus_ps :: "'a ps ⇒ 'a ps ⇒ 'a ps" is "λf g x. f x + g x" ..
instance ..
end
instantiation ps :: ("{semigroup_add,zero}") semigroup_add
begin
instance sorry (* imagine a proof here *)
end
lemma
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
sorry (* want to prove this *)
end
In this example, I want to instantiate the type 'a with class semigroup_add in order to prove the lemma. Alternatively, I tried the following proof:
lemma
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
proof-
have "OFCLASS('a, semigroup_add_class)" unfolding semigroup_add_class_def
proof-
show "OFCLASS('a, plus_class)" ..
next
show "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)" using assms .
qed
hence "OFCLASS('a ps, semigroup_add_class)" sorry
hence "OFCLASS('a ps, plus_class) &&& class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)" unfolding semigroup_add_class_def sorry
thus "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)" sorry
qed
However, I'm not sure how to fill the gaps.
Of course, the last instantiation in my MWE is morally equivalent to the lemma I want to prove, but I'm trying to do this in a more complicated context (I'm using types to sets).
Mathias Fleury (Aug 30 2023 at 19:25):I use interpret:
typedef (overloaded) 'a ps = "{f::nat ⇒ 'a ::{zero}. True}"
morphisms nth Abs
by blast
setup_lifting type_definition_ps
instantiation ps :: ("{plus,zero}") plus
begin
lift_definition plus_ps :: "'a ps ⇒ 'a ps ⇒ 'a ps" is "λf g x. f x + g x" ..
instance ..
end
lemma False
proof -
interpret ps: semigroup_add ‹plus :: 'a :: {semigroup_add,zero} ps ⇒ 'a ps ⇒ 'a ps›
sorry
thm ps.add_assoc
I'm not sure how I can use this to apply my instantiation. As I understand, I would have to basically repeat the instantiation proof within the interpret? What I would like to do is to somehow use the existing instantiation to prove the lemma.
For instance if I have this instantiation:
instantiation ps :: ("{semigroup_add,zero}") semigroup_add
begin
instance apply standard by transfer (simp add: add.assoc)
end
I don't want to have to repeat its proof in the proof of my lemma:
lemma
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
In my actual application the instantiation proof is long and split over many classes.
Mathias Fleury (Aug 31 2023 at 04:58):If you can prove the instantiation, the proof is trivial:
interpret ps: semigroup_add ‹plus :: 'a :: {semigroup_add,zero} ps ⇒ 'a ps ⇒ 'a ps›
by unfold_locales
BTW for the lemma you did not know how to prove class.semigroup_add is a constant, so class.semigroup_add_def exists to unfold it.
Artem Khovanov (Aug 31 2023 at 15:03):Sorry, I'm still unsure how to proceed. In my example, I don't have the'a::semigroup_add class annotation, I just have the fact class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a). What I'm unsure how to do is precisely this: how to go from this class.semigroup_add assertion to the ::semigroup_add annotation.
Artem Khovanov (Aug 31 2023 at 15:10):Basically, what I want to prove is this lemma:
lemma
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
Given this instantiation:
instantiation ps :: ("{semigroup_add,zero}") semigroup_add
lemma
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
apply unfold_locales
apply transfer
using assms unfolding class.semigroup_add_def
apply (auto)
done
Doesn't this proof just repeat the proof of the instantiation? In my application, the proof of the instantiation is quite long and split over many classes, and what I'm asking essentially is whether it's possible to just reference it rather than writing it all out again.
Mathias Fleury (Aug 31 2023 at 16:39):lemma hand_written_instance:
assumes "class.semigroup_add ((+)::'a::{plus,zero}⇒'a⇒'a)"
shows "class.semigroup_add ((+)::'a ps⇒'a ps⇒'a ps)"
apply (unfold class.semigroup_add_def)
sorry
instance ps :: ("{semigroup_add,zero}") semigroup_add
proof -
have "class.semigroup_add ((+)::'a⇒'a⇒'a)"
by unfold_locales
from hand_written_instance[OF this] show ‹OFCLASS('a ps, semigroup_add_class)›
apply (intro_classes)
apply (unfold class.semigroup_add_def)
by blast
qed
Ah OK, thanks! I guess what I was wondering was if it was possible to go in the other direction. In my application, the instance proof already exists, and I need the hand-written proof (so that I can apply the transfer package). I think what I will have to do is to manually create the hand-written proof by pasting in each instance proof, then stitching them together.
What I am actually trying to obtain is a "hand-written" version of
instantiation fpxs :: (field) field
in Formal_Puiseux_Series.Formal_Puiseux_Series (from the AFP).
Artem Khovanov (Sep 04 2023 at 22:13):(In case anyone comes across this)
The way you do what I wanted to do (ie turn the type sort into a locale hypothesis) is by using the attribute unoverload_type 'a from the Types-To-Sets library. An example is here:
https://isabelle.in.tum.de/dist/library/HOL/HOL-Types_To_Sets/T2_Spaces.html
Last updated: Apr 27 2024 at 20:14 UTC