mysterious message

Stream: new members

[Michael Beeson]

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

[Shing Tak Lam]

try set_option pp.all true in your file.

[Michael Beeson]

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

[Shing Tak Lam]

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

[Michael Beeson]

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

[Michael Beeson]

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

[Kevin Buzzard]

#mwe ?

[Kevin Buzzard]

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

[Michael Beeson]

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

[Sebastien Gouezel]

What about set_option pp.all true?

[Michael Beeson]

See above, that was the first suggestion.

[Sebastien Gouezel]

ok, we really need a #mwe

[Michael Beeson]

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

[Michael Beeson]

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.

[Sebastien Gouezel]

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

[Michael Beeson]

How do I upload an attachment?

[Kevin Buzzard]

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

[Michael Beeson]

inf.lean

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

[Shing Tak Lam]

@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

[Shing Tak Lam]

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

[Michael Beeson]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Reid Barton]

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.

[Patrick Massot]

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.

[Reid Barton]

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.

[Kevin Buzzard]

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

[Reid Barton]

I guess I meant other than this.

[Michael Beeson]

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...

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

(or indeed just exact h.symm)

[Mario Carneiro]

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

[Mario Carneiro]

Is docs#symmetry' a thing?

[Mario Carneiro]

guess not

[Kyle Miller]

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

[Johan Commelin]

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

[Kyle Miller]

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.

[Bryan Gin-ge Chen]

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