## Stream: new members

### Topic: mysterious message

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


#### Shing Tak Lam (Jun 30 2020 at 06:57):

try set_option pp.all true in your file.

#### Michael Beeson (Jun 30 2020 at 07:00):

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

#### Shing Tak Lam (Jun 30 2020 at 07:00):

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

#### Michael Beeson (Jun 30 2020 at 07:01):

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

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


#mwe ?

#### Kevin Buzzard (Jun 30 2020 at 07:06):

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

#### Michael Beeson (Jun 30 2020 at 07:09):

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

#### Sebastien Gouezel (Jun 30 2020 at 07:10):

What about set_option pp.all true?

#### Michael Beeson (Jun 30 2020 at 07:10):

See above, that was the first suggestion.

#### Sebastien Gouezel (Jun 30 2020 at 07:11):

ok, we really need a #mwe

#### Michael Beeson (Jun 30 2020 at 07:13):

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

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

#### Sebastien Gouezel (Jun 30 2020 at 07:20):

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

#### Michael Beeson (Jun 30 2020 at 07:21):

How do I upload an attachment?

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

#### Michael Beeson (Jun 30 2020 at 07:43):

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

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


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

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

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

#### Sebastien Gouezel (Jun 30 2020 at 07:51):

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

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

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

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

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

#### Reid Barton (Jul 01 2020 at 13:58):

I guess I meant other than this.

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

#### Scott Morrison (Sep 06 2020 at 04:35):

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

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

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

#### Scott Morrison (Sep 06 2020 at 04:37):

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

#### Scott Morrison (Sep 06 2020 at 04:38):

(or indeed just exact h.symm)

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

#### Mario Carneiro (Sep 06 2020 at 05:05):

Is docs#symmetry' a thing?

guess not

#### Kyle Miller (Sep 06 2020 at 05:17):

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

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

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

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