Stream: Beginner Questions

Topic: can't instantiate quantifiers

ee (Feb 02 2024 at 13:29):

"(∀x y. symm x y ⟶
(∃z f g.
target f = target g ∧
source f = x ∧ source g = y ∧ target f = z)) ⟶
source f = source g ⟹
symm (target f) (target g)"
This is the statement I'm trying to prove. Ideally what I'd like to do is

1. " (∃z f g. target f = target g ∧ source f = x ∧ source g = y ∧ target f = z)) " instantiate the f and g here

2. Merge the ( source f = source g) with "target f = target g ∧ source f = x ∧ source g = y ∧ target f = z)) " to get " source f = source g /\ target f = target g", and the using the definition of symm prove the result

Problems:

1. Auto gives me things I can't prove.
2. Simp does nothing
3. I can't use (rule allI / exE) or get rid of the quantifiers.
4. I can't figure out how to add "source f = source g" to my assumptions instead of having it as the result of an implication.
   Thanks a bunch

Yong Kiam (Feb 02 2024 at 13:32):

is there a problem with your parentheses here? your 1) is behind the symm x y implication

Mathias Fleury (Feb 02 2024 at 13:40):

I think that the )⟶ should be )⟹

Yong Kiam (Feb 02 2024 at 13:42):

hm, that still doesn't fix that there's no x and y (at least not that I can see) to choose to get the existential in 1)

Mathias Fleury (Feb 02 2024 at 13:56):

I meant

(∀x y. symm x y ⟶
(∃z f g.
target f = target g ∧
source f = x ∧ source g = y ∧ target f = z)) ⟶
source f = source g ⟹

should be

(∀x y. symm x y ⟶
(∃z f g.
target f = target g ∧
source f = x ∧ source g = y ∧ target f = z))  ⟹
source f = source g ⟹

Mathias Fleury (Feb 02 2024 at 13:56):

but it is very hard to know

Yong Kiam (Feb 02 2024 at 13:57):

hm but that doesn't change the problem substantially right? your version is one auto away
ah I was reading the binding wrong on the meta implies

ee (Feb 02 2024 at 14:00):

Mathias Fleury said:

I meant

(∀x y. symm x y ⟶
(∃z f g.
target f = target g ∧
source f = x ∧ source g = y ∧ target f = z)) ⟶
source f = source g ⟹

should be

(∀x y. symm x y ⟶
(∃z f g.
target f = target g ∧
source f = x ∧ source g = y ∧ target f = z))  ⟹
source f = source g ⟹

Ah yeah that was a typo. I'll see if that changes anything with the proof

ee (Feb 02 2024 at 14:14):

Is there a way to turn all the "-->" into "==>" .? The reason I have both is because I used "-->" in a definition(which is what you are supposed to do afaik?) and now I'm using it in a lemma so I used "==>"

Last updated: Apr 28 2024 at 12:28 UTC