Naso (Jun 30 2023 at 13:59): Naso (Jun 30 2023 at 13:59):I have started formalizing some work involving presheaves of posets and related structures. To ensure that the structure satisfies its defining properties, such as having a transitive, reflexive, antisymmetric relation for a poset, I encoded them as record types with 'valid' predicates.
Recently, I discovered typedef and the transfer/lifting architecture, and I realized that this approach might be a much better way to handle things because it enforces the validity predicate by default. Consequently, I decided to rewrite my formalization. So far, I have successfully formalized Functions and (topological) Spaces. However, I'm encountering difficulties when trying to formalize a presheaf, which is a contravariant functor from a topological space into sets, using transfer.
I defined a RawPresheaf as follows:
record ('A, 'x) RawPresheaf =
prim_space :: "'A Space"
prim_ob :: "('A Open, 'x set) Function"
prim_ar :: "('A Inclusion, ('x, 'x) Function) Function"
It includes a valid predicate:
definition valid :: "('A, 'x) RawPresheaf ⇒ bool"
Then I defined Presheaf as:
typedef ('A, 'x) Presheaf = "{ rF :: ('A, 'x) RawPresheaf . valid rF}"
Now, I am attempting to prove the following lemma:
fixes F :: "('A, 'x) Presheaf" and i :: "'A Inclusion"
assumes "i ∈ inclusions (space F)"
shows "Function.dom (ar F ⋅ i) = ob F ⋅ (Space.cod i)"
apply transfer
The current state of the proof is as follows:
proof (prove)
goal (2 subgoals):
1. ⋀F i. Presheaf.valid F ⟹ valid_inc i ⟹ Function.raw_dom (?ad17 (prim_ar F) i) = prim_ob F ⋅ RawInclusion.raw_cod i
2. Transfer.Rel (rel_fun (=) (rel_fun cr_Inclusion cr_Function)) ?ad17 (⋅)
It appears that the presence of the anonymous function ?ad17 indicates that transfer has failed on the \cdot operation (defined as app), even though app is defined as a lifted version of raw_app](https://github.com/nasosev/cva/blob/1c0a16aac93a21f0cb292977836d402a6573d096/new/Function.thy#L76), and I did not encounter any problems using transfer on app in the Space and Function theories, only in Presheaf, which is defined in terms of them. Hence, I suspect that the issue may be due to the nested typedef definition of Presheaf, but I'm not certain. I have consulted the manual and attempted to use transfer', transfer_prover, and transfer fixing:, but without success.
I would greatly appreciate any assistance here! The source code is available here.
Last updated: Apr 28 2024 at 08:19 UTC