Zulip Chat Archive

Stream: new members

Topic: mysterious message


view this post on Zulip Michael Beeson (Jun 30 2020 at 06:56):

Can you help me make sense of this error message?

type mismatch at application
  and.intro h10.right.left
term
  h10.right.left
has type
    x,y    R
but is expected to have type
    x,y    R

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 06:57):

try set_option pp.all true in your file.

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:00):

That causes
invalid Boolean option value, 'true' or 'false' expected

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 07:00):

Sorry, I forgot the true there. I've edited my original comment

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:01):

Whew, now I have a lot more to look at!

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:04):

but the mystery is still there:

has type
  @Model.mem M _inst_1 (@Model.ordered_pair M _inst_1 x y) R
but is expected to have type
  @Model.mem M _inst_1 (@Model.ordered_pair M _inst_1 x y) R

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:06):

#mwe ?

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:06):

Could be a universe issue, you could set_option pp.universes true

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:09):

I don't think that changed the output messages at all.

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:10):

What about set_option pp.all true?

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:10):

See above, that was the first suggestion.

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:11):

ok, we really need a #mwe

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:13):

Well, I only have a maximal working example. My file is 385 lines.

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:14):

I was hoping it was easy for you people.. but if not I guess I'll just delete that proof and try it again some other way.

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:20):

If your file is self-contained, you can just upload it as an attachment on zulip.

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:21):

How do I upload an attachment?

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:21):

You can post it on gist.github.com as well. You upload an attachment by clicking on the paper clip under the box where you type messages

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:43):

inf.lean

OK there is my file that produces the error message about which I posted.

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 07:47):

@Michael Beeson

I've modified your example slightly, and I get the actual error message.

lemma paste_members:
   (R:M) (S:M), Rel R  Rel S   x y z:M, ( (single (single x)),  y, z   paste M R S 
                                    x,y  R  x,z   S
                                  ) :=
  assume (R:M) (S:M),
  have h1: Rel (inv (proj1:M)), from inverse_axiom1 proj1 (rel_proj1 M),
  have h2: Rel (inv (proj2:M)), from inverse_axiom1 proj2 (rel_proj2 M),
  begin
    intros hr hs,
    assume x y z,
    rw paste,
    rw (intersection_axiom (join R (inv proj1)) (join S (inv proj2))  single (single x),  y,z   ),
    rw (join_axiom R (inv proj1) hr h1  single (single x),  y,z   ),
    rw (join_axiom S (inv proj2) hs h2  single (single x),  y,z   ),
    apply iff.intro,
      { intro h3,
        cases h3 with h4 h5,
        cases h4 with x h6,
        cases h6 with y h8,
        cases h5 with x h7,
        cases h7 with z h9,
        cases h8 with z h10,
        cases h9 with z h11,
        refine and.intro _ _,
        { have := h10.2.1,
          exact this }
      },
      {

      }

  end

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 07:49):

Essentially, you have multiple variables called x and y, and h10.right.left has a different x and/or y compared to the goal

view this post on Zulip Michael Beeson (Jun 30 2020 at 07:50):

Thank you. I have made other errors having multiple variables with the same name. I am a slow learner...

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:50):

Exactly. After the cases h9, you have in your proof state

x y z x y x z z : M,

So three different things are named x

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:51):

(and three are named z and two are named y!)

view this post on Zulip Reid Barton (Jun 30 2020 at 12:52):

Lean's error message could be better here. I know there are already some situations where it warns about having two variables with the same name.

view this post on Zulip Patrick Massot (Jun 30 2020 at 21:47):

This multiple variables with the same name issue is really awful. I was never convinced by arguments in favor of not warning the user here, except when the name is this.

view this post on Zulip Reid Barton (Jun 30 2020 at 22:32):

Can autogenerated variables names collide with existing ones? If so a warning could be annoying to work around sometimes. (Or it could only warn about variables the user explicitly named.) But if Lean is going to produce an error anyways, then there's absolutely no reason not to emit a warning as well.

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 06:43):

My experience with auto-generated variables is that it depends on the tactic. For example have will make as many thiss as you will ever need

view this post on Zulip Reid Barton (Jul 01 2020 at 13:58):

I guess I meant other than this.

view this post on Zulip Michael Beeson (Sep 06 2020 at 03:31):

set_option default_priority 100
reserve infix `  ` : 49
class  Model (M:Type)  :=
(mem : M  M  Prop)
(pair: M  M  M)
(single: M  M)
(infix    :=  mem )
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:   a b, ( x, (mem x a  mem x b))  a=b)
(pairing_axiom:   x a b, (x  {a,b}  (x = a   x = b)))
( single_definition :  x, single x = {x,x})
(notation `{` a `,` b `}` := pair a b)

open Model
infix   :=  mem
notation `{` a `,` b `}` := pair a b
variables (M:Type) [Model M] (a b x y z u v w X R W: M)

lemma symmetry_test2:  a b:M, (a=b  b = a):=
 begin
  intros a b h,
  symmetry at h,
  exact h,
 end

The line "symmetry at h" third from the bottom generates
"invalid 'begin-end' expression, ',' expected"
and the next line generates "sync", although the
lemma does type-check. I got here when an attempted
use of "symmetry" generated a similar error, but in that
case the proof wouldn't check. The example above
can be copied and checked. Probably you could remove
many of the class members. If you remove "at h" the
error goes away, indicating that the syntax elsewhere is OK.
But it should be OK with "at h" as shown; indeed it is OK enough
to type-check...

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:35):

It's just that symmetry doesn't accept an at keyword.

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:35):

If you hover over symmetry to get the tooltip, or look at tactic#symmetry, you'll see it only operates on the goal.

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:36):

I agree it would be nice if it accepted this, and indeed this would be an excellent tactic project for someone wanting to learn about writing tactics.

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:37):

If you import tactic.basic, then you can use replace h := h.symm in the meantime.

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:38):

(or indeed just exact h.symm)

view this post on Zulip Mario Carneiro (Sep 06 2020 at 05:02):

You can't define notations starting with {. Bad Things will happen. All notations starting with { are defined inside the C++ code

view this post on Zulip Mario Carneiro (Sep 06 2020 at 05:05):

Is docs#symmetry' a thing?

view this post on Zulip Mario Carneiro (Sep 06 2020 at 05:06):

guess not

view this post on Zulip Kyle Miller (Sep 06 2020 at 05:17):

I started implementing it, but then I found symmetry' is in tactic/apply.lean

view this post on Zulip Johan Commelin (Sep 06 2020 at 05:19):

We should really beg and plead those tactic' versions until they give up and move to core to merge themselves with the unprimed versions.

view this post on Zulip Kyle Miller (Sep 06 2020 at 05:28):

It looks like one difference with symmetry' versus symmetry is that when it applies to the goal, it uses tactic.symmetry', which uses retry_apply rather than apply_core to apply the symmetry lemma. This retry_apply tries apply_core first, but then it does some sort of try-to-apply-harder routine if that fails.

view this post on Zulip Bryan Gin-ge Chen (Sep 06 2020 at 05:34):

Here's a tracking issue for the primed tactics, though it hasn't been updated in a while: lean#124.


Last updated: May 16 2021 at 05:21 UTC