Yiming Xu (Feb 09 2025 at 16:31): Yiming Xu (Feb 09 2025 at 16:31):I want to consider embedding a relation to another type, and I defined:
definition inc_rel where
"inc_rel i R ≡ {p. (∃ r1 r2. (r1,r2) ∈ R ∧ p = (i r1, i r2))}"
inc_rel is supposed to embed R via an injection i.
Yiming Xu (Feb 09 2025 at 16:31):I want as an effect:
theorem rtrancl_inj:
assumes "inj_on i (Domain R ∪ Range R)"
shows " inc_rel i (R⇧*) = (inc_rel i R)⇧*" using assms
However, nitpick tells me that is wrong.
Nitpicking goal:
inj_on i (Domain R ∪ Range R) ⟹
inc_rel i (R⇧*) = (inc_rel i R)⇧*
Nitpick found a quasi genuine counterexample
for card 'b = 3 and card 'a = 2:
Free variables:
R = {}
i = (λx. _)(a⇩1 := b⇩1, a⇩2 := b⇩2)
Try again with "user_axioms" set to "true" to
confirm that the counterexample is genuine
But it then seems that it does not conceive my definition of inc_rel correctly. I expect the both (inc_rel I R)^* and inc_rel i R^* are empty, given that R is empty.
Yiming Xu (Feb 09 2025 at 16:33):What is wrong here?
Mathias Fleury (Feb 09 2025 at 16:36):Nitpick is telling you that it is not sure if the counter example is correct: found a quasi genuine counterexample
Mathias Fleury (Feb 09 2025 at 16:37):Quickchecks claims to have found a counterexample:
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
i = (λx. undefined)(a⇩1 := a⇩1, a⇩2 := a⇩1)
R = {}
Evaluated terms:
inc_rel i (R⇧*) = {(a⇩1, a⇩1), (a⇩1, a⇩1)}
(inc_rel i R)⇧* = {(a⇩1, a⇩1), (a⇩2, a⇩2)}
but it looks wrong too
Yiming Xu (Feb 09 2025 at 16:38):Again I think both relations should be empty.
Yiming Xu (Feb 09 2025 at 16:38):I see, that is helpful to know that counter-example finders can be wrong...
Yiming Xu (Feb 09 2025 at 16:39):BTW are you aware of anything that considers the image of relations under functions?
Mathias Fleury (Feb 09 2025 at 16:39):Ahhhhh
Mathias Fleury (Feb 09 2025 at 16:40):you do not want the reflexive transitive closure
Mathias Fleury (Feb 09 2025 at 16:40):only the transitive closure, right?
Yiming Xu (Feb 09 2025 at 16:40):I just find it annoying to prove the image of a tree relation is a tree...
Yiming Xu (Feb 09 2025 at 16:40):I want both, actually.
Mathias Fleury (Feb 09 2025 at 16:41):So actually, the counter example is not wrong, your theorem does not mean what you think it means
lemma ‹rtrancl {} = (λx. (x,x)) ` UNIV›
by auto
I wonder why it is defined like this... Let me check the definition.
Mathias Fleury (Feb 09 2025 at 16:44):Yiming Xu said:
BTW are you aware of anything that considers the image of relations under functions?
you mean about f `` R?
Mathias Fleury (Feb 09 2025 at 16:44):Yiming Xu said:
I wonder why it is defined like this... Let me check the definition.
reflexive transitive closure
Mathias Fleury (Feb 09 2025 at 16:44):it must be _reflexive_
Yiming Xu (Feb 09 2025 at 16:45):Not only making the ones that is already in the relation reflexive, I see.
Mathias Fleury (Feb 09 2025 at 16:45):that why there is also the transitive closure (^+ in Isabelle)
Yiming Xu (Feb 09 2025 at 16:46):So is there anything consider the image of transitive closure?
Yiming Xu (Feb 09 2025 at 16:47):Fair enough if nothing exists yet...
Yiming Xu (Feb 09 2025 at 16:48):Thankfully I just convinced that my usage of it in my theorems is not wrong. I was panic for a moment.
Mathias Fleury (Feb 09 2025 at 16:49):Yiming Xu said:
So is there anything consider the image of transitive closure?
term ‹Image ((rtrancl A) :: ('a × 'a) set)›?
Mathias Fleury (Feb 09 2025 at 16:49):or are you talking about something else?
Yiming Xu (Feb 09 2025 at 16:49):I mean the image under a function.
Yiming Xu (Feb 09 2025 at 16:50):Here I actually only care about injective functions.
Mathias Fleury (Feb 09 2025 at 16:51):Can you write it down formally? I do not know what that is.
Yiming Xu (Feb 09 2025 at 16:52):definition im_rel where
"im_rel i R ≡ {p. (∃ r1 r2. (r1,r2) ∈ R ∧ p = (i r1, i r2))}"
term ‹(range (λx. (f x,f x))) O R›
I know the (λx. (f x,f x)) has a name, but it is escaping me right now
Yiming Xu (Feb 09 2025 at 16:58):Thanks! That is helpful to know. I will bug people around.
Last updated: Mar 09 2025 at 12:28 UTC