Email Gateway (Aug 22 2022 at 20:15): Email Gateway (Aug 22 2022 at 20:15):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Today, I found myself struggling to resolve a, seemingly, very trivial
issue. I am trying to obtain a list of all type variables that are declared
in a proof context. It does not seem that the relevant data is exposed to
the public interface. However, most likely, I am missing something.
Here is a minimal example:
val ctxt = @{context};
val T = TVar (("'a", 0), ["Groups.plus"]);
val ctxt = Variable.declare_typ T ctxt;
(* val declTs = obtain_declared_types ctxt ? *)
Please note that I am aware of the function Variable.is_declared. However,
seemingly, this function merely performs a check based on the name context
and, therefore, does not include the schematic (type) variables.
The use case is the generation of fresh schematic type variables.
Therefore, if a solution to this problem can already be found somewhere in
the source code, it may be a suitable alternative to the answer to the
original question. Nevertheless, I would still highly prefer to understand
how to obtain all declared type variables.
Thank you
Email Gateway (Aug 22 2022 at 20:15):From: Alexander Krauss <krauss@in.tum.de>
Am 14.07.2019 um 18:03 schrieb mailing-list anonymous:
I am trying to obtain a list of all type variables that are declared
in a proof context. It does not seem that the relevant data is exposed to
the public interface.
Yes, I think this is not exposed. As I understand it, it is more of an
implementation detail, and the "invent fresh names" operations are what
you are supposed to use.
[...]
The use case is the generation of fresh schematic type variables.
In this case, I would probably generate fixed type variables first (cf.
Variable.invent_types) and then generalize the final results (terms,
theorems) (cf. Variable.export_*)
Hope this helps
Alex
Email Gateway (Aug 22 2022 at 20:16):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Alexander Krauss/All,
Thank you for your reply. It is very useful to know that the functionality
that I was looking for is not available.
Indeed, my problem is slightly superficial and, generally, can be resolved
by following one of the more traditional approaches, like the one that you
suggested at the end of your email. Nevertheless, it seems that using such
traditional approaches would result in redundant computations, given the
problem at hand. Perhaps, there is another way to proceed. I would like to
know if there is a way to reduce all indexnames in a theorem to zero in a
context-aware fashion (please note that I am aware of the function
Drule.zero_var_indexes, but it ignores the local context). Such a function
could provide an efficient alternative to the solution of the problem that
I am dealing with.
As a side note, it seems that making a functionality that shows all
entities declared in a context or, better yet, a context difference
function would be very useful for the purposes of
inspection/testing/verification/debugging. For example, I would like to
ensure that my modules do not leave any redundant entities in the context.
Given the information in your previous email, it seems that this is
something that one cannot do at the moment.
I would also like to make another remark that has some connection to the
problem that I was trying to solve. I encountered a behaviour which I find
difficult to understand. Somehow, given a locale context with declared
(type) variables, it is still possible to register theorems in the locale
context that, seemingly, ignore the sorts/types associated with the
previously declared variables (see the code listing after my signature).
Somehow, I was under the (seemingly, erroneous) impression that, unlike
constants, variables are only allowed to have one type/sort in the same
context... does there exist any documentation that explains this behaviour?
The only references that I could find on this matter were in the
implementation manual (p. 65 and p. 69):
"The core logic handles the type variables with the same name but
different sorts as different, although the type-inference layer (which is
outside the core) rejects anything like that."
"Type-inference rejects variables of the same name, but different types.
In contrast, mixed instances of polymorphic constants occur routinely."
However, these references do not explicitly state that it is, indeed, legal
and appropriate to use the same variable with different type/sort in the
same context. Why are the users allowed to forego a type inference before
registering a theorem in a context or creating a proveable goal? Are there
any practical use cases for this allowance? Most certainly, it enables the
construction of slightly peculiar theorems. For example, I was able to
produce the following theorem (see the code listing below):
"(B::'b::plus) = B ⟹ B::'b::type ≡ B"
Thank you
declare [[show_sorts]]
locale myloc =
fixes B :: "'b::plus"
assumes "B ≡ B"
begin
lemma tt: "True ≡ True" by auto
ML ‹
val T = TVar (("'a", 0), ["Groups.plus"]);
fun mk_eq_thm lthy =
let
val T = TVar (("'a", 1), ["HOL.type"]);
val ct = Var (("A", 0), T) |> Thm.cterm_of lthy;
val thm = ct |> Thm.reflexive;
val lthy = Local_Theory.note ((@{binding mythm}, []), single thm) lthy |>
snd
in lthy end
val q = Thm.implies_intr
fun mk_eq_thm' lthy =
let
val T = TFree ("'b", ["HOL.type"])
val ct = Free ("B", T) |> Thm.cterm_of lthy
val thm = ct |> Thm.reflexive
val thm = Thm.implies_intr
(@{term True} |> HOLogic.mk_Trueprop |> Thm.cterm_of lthy)
thm
val lthy = Local_Theory.note ((@{binding mythm'}, []), single thm) lthy
|> snd
in lthy end
›
local_setup ‹Local_Theory.target (Variable.declare_typ T)›
(*
Both produce an error similar to
"Sort constraint type inconsistent with default plus for type variable
"?'a"⌂":
schematic_goal "(?A::?'a::type) = ?A"
lemma "(Q::'b::type) = (Q::'b::type)"
*)
local_setup ‹mk_eq_thm›
local_setup ‹mk_eq_thm'›
thm mythm (* ?A::?'a::type ≡ ?A *)
thm mythm' (* B::'b::type ≡ B *)
(* peculiar theorem *)
lemma QQ: "True"
proof-
(* the occurrences of B have different types in the goal *)
define C where "C = (B = B)"
have True_C: "C = True" unfolding C_def by auto
have aaa: "True" by auto
note mythm'' = mythm'[folded True_C, unfolded C_def]
thm mythm'' (* (B::'b::plus) = B ⟹ B::'b::type ≡ B *)
show ?thesis by auto
qed
(*
It seems that it is possible to produce theorems in the locale
context that use the default sort 'type' both for the schematic type
variable
with the indexname ("'a", 0) and the fixed type variable with the name 'b,
as well as the type "'b::type" for the fixed variable B.
Nevertheless, the sorts of the declared types are still 'Groups.plus'. This
can be observed by trying to state the lemmas from the previous example:
schematic_goal "(?A::?'a::type) = ?A"
lemma "(Q::'b::type) = (Q::'b::type)"
which results in the same error as before.
*)
end
Last updated: Apr 19 2024 at 16:20 UTC