Email Gateway (Jan 07 2023 at 15:15): Email Gateway (Jan 07 2023 at 15:15):From: Asta Halkjær From <andro.from@gmail.com>
Hi,
In my current project, I'm interested in knowing that a lot of datatypes
inherit the cardinality of their parameters, in a similar way to how a lot
of datatypes are countable as long as their parameters are.
For instance, the cardinal library already knows about lists, so you can
prove the following:
lemma
assumes ‹infinite (UNIV :: 'a set)›
shows ‹|UNIV :: 'a list set| =o |UNIV :: 'a set|›
using assms card_of_lists_infinite by fastforce
But I would like an automatic way to generate lemmas like this for other
datatypes (of the correct shape) as well.
Is there any existing work on this?
Best,
Asta
Email Gateway (Jan 09 2023 at 16:27):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Asta,
The closest to this is perhaps the proof that we do internally in the datatype construction, where we establish for any BNF ‘a T:
"|{x. set_T x ⊆ A}| ≤o ( |A| +c ctwo) ^c (bd_T +c |UNIV :: bd_type_T T set| )"
If you take A to be UNIV this is the same as:
"|UNIV :: 'a T set| ≤o |UNIV :: 'a set| ^c (bd_T +c |UNIV :: bd_type_T T set| )”
If you further know that T is countable you can get to:
"|UNIV :: 'a T set| ≤o |UNIV :: 'a set| ^c natLeq”
This gives a rather crude upper bound (and no lower bound) if you compare with what you found in the library for lists. On the upside it works for any BNF.
But probably you want something more precise for the datatypes “of the correct shape”. Do you have an intuition what the correct shape is (just sums of products, i.e., no nesting?).
Best wishes,
Dmitriy
Email Gateway (Jan 09 2023 at 16:48):From: Asta Halkjær From <andro.from@gmail.com>
Hi Dmitriy,
Cool! What I am interested in is logical syntax.
I have just submitted an AFP entry with a framework for proving
completeness, so I wanted a generic solution for users of that framework.
The non-generic solution I came up with is the following.
The example here is first-order logic. I have done the same for hybrid
logic.
Syntax can be written down linearly, so I can write an injective function
from terms and formulas to lists of type ('f + 'p) + marker <*> nat.
Here 'f is the type of functions symbols, 'p is the type of propositional
symbols and marker is just an enumeration type.
My encoding is basically Polish notation but with the natural numbers added
in to ease the injectivity proof.
For example: "Imp p q" becomes "Inr (ImpM, length (encode p)) # encode p @
encode q".
I wrote a similar function for labelled hybrid logic formulas.
Then I wrote a helper lemma that does the cardinal arithmetic for both
cases.
Since the marker type is finite and I assume that 'f is infinite, 'f + 'p
swallows marker <*> nat .
In the end I get that |UNIV :: ('f, 'p) fm set| <=o |UNIV :: 'f set| +c
|UNIV :: 'p set|.
This feels like a nice bound to me.
While this is not automatic, the injective function should not be too hard
to copy and modify to other syntax.
Best,
Asta
Den man. 9. jan. 2023 kl. 17.25 skrev Dmitriy Traytel <traytel@di.ku.dk>:
Last updated: Apr 19 2024 at 16:20 UTC