Stream: Beginner Questions

Topic: goal in context cannot be proved

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:13):

I have this Isar state

using this:
  constrained_to (renaming_subst fr too) χ = renaming_subst (map fst (filter (λx. fst x ∈ χ) (zip fr too))) (map snd (filter (λx. fst x ∈ χ) (zip fr too)))

goal (1 subgoal):
 1. constrained_to (renaming_subst fr too) χ = renaming_subst (map fst (filter (λx. fst x ∈ χ) (zip fr too))) (map snd (filter (λx. fst x ∈ χ) (zip fr too)))

I don't think that the definitions are relevant, but these two are exactly the same, shouldn't it be easily proved? try cannot find anything and netiher can I. I didn't think it allowed shadowing in the first place, but I don't think theres any shadowing in my proof. What could cause this?

EDIT:
Lesson Learned:

  1. check colors of variables are the same
  2. check that types of things match (using declare [[show_types, show_sorts]])
  3. when showing types, pay special attention to unused type varibles listed, these could occur in types not shown
    The problem is that some of my functions have freely chosen type variables, which was not shown, and instantiated differently at each call.

view this post on Zulip Lukas Stevens (Apr 25 2024 at 11:15):

Do all variables have matching colors? Can you post a screenshot of Isabelle/Jedit?

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:16):

Good point, but yes, same colors
image.png

view this post on Zulip Lukas Stevens (Apr 25 2024 at 11:18):

You could also do declare [[show_types,show_sorts]]. Maybe something is wrong there.

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:21):

Oh I didn't know about that, good idea
image.png

They are different in a confusing way

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:25):

Oh I see how it works, but then they agree right?

view this post on Zulip Lukas Stevens (Apr 25 2024 at 11:28):

The 'a matches. But where does the 'd come from?

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:30):

It doesn't show anywhere so I'm not sure. Do you know how I would find out?

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:32):

looking at everything in Print Context with context, cases, terms, and theorems, there is no 'd

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:42):

oh, renaming_subst has type 'a list ⇒ 'a list ⇒ 'a ⇒ ('b, 'a) Type.type so the 'b is unconstrained by the input, so I guess this 'b is instantiated differently, not shown in the annotations. And I'm trying to prove equivalence independent on type instantiation.

view this post on Zulip Jonathan Lindegaard Starup (Apr 25 2024 at 11:51):

Annotations that force the type parameter worked. I'm not sure how to make it pretty but its a solution. Thank you :)

Last updated: May 06 2024 at 12:29 UTC