## Stream: new members

### Topic: multiple assumptions of definitionally equal type

#### Reuben Rowe (Nov 26 2019 at 15:53):

I have come across a situation where, in tactic mode, I have two assumptions in my context whose types are not equal but they are definitionally equal. Specifically, for a particular expression _e, the types are m ∈ _e and _e = some m. I would like to rewrite using the equality. However, when I use rw ‹_e = some m› the rw tactic fails because the assumption of type m ∈ _e appears before the other one in the context, and so the tactic ‹_e = some m› returns the wrong assumption.

Of course, I can use the names of the assumptions instead of the ‹⬝› tactic, but I would like to avoid using names if I can.

Is this a known problem? is it considered a "problem"?

#### Kevin Buzzard (Nov 26 2019 at 17:58):

I guess I've never had to worry about not using names. Do you need both hypotheses in the context? If not then you could clear one. Otherwise probably you can use some meta magic (which I know nothing about) to give the bad tactic a fresh name or something.

#### Reuben Rowe (Nov 26 2019 at 18:18):

It's not that I can't use names for the hypotheses, it's that I want to try doing without - it's a style objective.

#### Kevin Buzzard (Nov 26 2019 at 18:24):

Just to be sure -- if you rewrite with the name of the correct assumption, does the rewrite not fail?

I was looking at conditionally complete lattices in Lean's maths library over the last few days, and they use the french quotes in several places.

#### Reid Barton (Nov 26 2019 at 18:25):

I suppose the assumption tactic (which underlies the french quotes) could do a first pass to look for a hypothesis that matches the requested type syntactically. I seem to recall this coming up before.

#### Reuben Rowe (Nov 26 2019 at 18:31):

@Kevin Buzzard: yes, if I name the hypothesis rw succeeds

#### Rob Lewis (Nov 26 2019 at 18:31):

It might even be enough to change this line to show p, by assumption. https://github.com/leanprover-community/lean/blob/master/library/init/meta/tactic.lean#L871

#### Rob Lewis (Nov 26 2019 at 18:32):

There's a chance that could have side effects elsewhere.

#### Reuben Rowe (Nov 26 2019 at 18:32):

@Rob Lewis: no, it is the assumption tactic itself which picks the wrong hypothesis

#### Rob Lewis (Nov 26 2019 at 18:33):

It doesn't matter which hypothesis the tactic chooses if they're definitionally the same. What matters is what the assumption tactic is used to prove.

#### Rob Lewis (Nov 26 2019 at 18:33):

(p : t) isn't necessarily the same as show t, from p.

#### Reuben Rowe (Nov 26 2019 at 18:33):

@Reid Barton: I played around by implementing a new version of assumption which checks for syntactic equality. In my particular case it was failing because there are meta-variables that are different.

#### Rob Lewis (Nov 26 2019 at 18:33):

The latter guarantees a term with type t. The former guarantees a term with type defeq to t.

#### Rob Lewis (Nov 26 2019 at 18:34):

So assumption would still find the first proof, but it would use it to prove the syntactic thing you want.

#### Reid Barton (Nov 26 2019 at 18:34):

That would make the french quote syntax marginally more useful as well

#### Reuben Rowe (Nov 26 2019 at 18:35):

@Rob Lewis oh right, yes I see what you mean

#### Reuben Rowe (Nov 26 2019 at 18:50):

So, I tried defining a local notation for french brackets with this proposed new implementation, and I was getting some errors:

none of the overloads are applicable
error for λ (x_1 : _),
show x_1, from has_bind.seq (tactic.save_info (_ 49 34)) (tactic.step tactic.interactive.assumption)
assumption tactic failed

context: switched to basic overload resolution where arguments are elaborated without any information about the expected type, because failed to elaborate all candidates using the expected type
m = n
this can happen because, for example, coercions were not considered in the process
none of the overloads are applicable


#### Reid Barton (Nov 26 2019 at 18:53):

That error looks weird

#### Reid Barton (Nov 26 2019 at 18:54):

How did you define the notation exactly?

#### Reuben Rowe (Nov 26 2019 at 18:54):

It might be because in my code, there are some implicit goals that need to be solved.

#### Reuben Rowe (Nov 26 2019 at 18:54):

How did you define the notation exactly?

notation ‹ p › := (show p, by assumption)

#### Reid Barton (Nov 26 2019 at 18:55):

Making it local notation (or just different syntax) might help, then it will override the global notation rather than Lean trying to consider both

#### Reuben Rowe (Nov 26 2019 at 18:55):

When I inline show p, by assumption at the place I want to use it (i.e. to generate a name for the hypothesis I want to apply rw to), it goes through fine, but also gives me new goals related to the parameters in my code.

#### Reuben Rowe (Nov 26 2019 at 18:56):

Making it local notation (or just different syntax) might help, then it will override the global notation rather than Lean trying to consider both

Yeah, that seems to be working.

#### Reid Barton (Nov 26 2019 at 18:57):

Working working or the same behavior as when you wrote show p, by assumption manually?

The latter.

#### Reuben Rowe (Nov 26 2019 at 18:59):

So, it is generating new goals related to the implicit parameters of p.

#### Reid Barton (Nov 26 2019 at 19:04):

So let's see. The actual p in your case involves metavariables? And you're expecting them to be filled in by the actual type of the hypothesis that matches?

#### Reid Barton (Nov 26 2019 at 19:05):

(wouldn't it be easier to just give the name of the hypothesis...?)

#### Rob Lewis (Nov 26 2019 at 19:09):

This is hard to follow without a working example.

#### Reuben Rowe (Nov 26 2019 at 19:11):

OK, I'll give the code.

#### Reid Barton (Nov 26 2019 at 19:13):

There are also probably easy ways to avoid having the old hypothesis around, besides clear, like rw at or replace

#### Reuben Rowe (Nov 26 2019 at 19:18):

universe u

parameters { α : Type u } [denumerable α] { αs : finset α }

def incl : α ↪ ℕ :=
function.embedding.mk encodable.encode encodable.encode_injective

def codes := finset.map incl αs

def code :=
match codes.max with
| none :=  0
| some n := (n+1)
end

example : ∀ c ∈ codes, c < code :=
begin
intros,
cases (finset.max_of_mem ‹c ∈ codes›) with m,
have : codes.max = some m, from ‹m ∈ codes.max›,
have : code = m + 1, by {
rw code,
rw ‹codes.max = some m›,
refl,
},
show : c < code,
by calc
c ≤ m : by {apply finset.le_max_of_mem, repeat {assumption}}
... < m + 1 : by apply nat.lt_succ_self
... = code : by {symmetry, from ‹code = m + 1›},
done,
end


#### Reuben Rowe (Nov 26 2019 at 19:20):

There are also probably easy ways to avoid having the old hypothesis around, besides clear, like rw at or replace

Yes, but these all involve naming the hypotheses, and I can just give the name of the hypothesis to rw, but as I say I am trying to see how far I can get by writing proofs in a "nameless" style. Perhaps this is not an interesting thing to try and do.

#### Rob Lewis (Nov 26 2019 at 19:23):

This works fine for me?

import data.equiv.denumerable
universe u
section
parameters { α : Type u } [denumerable α] { αs : finset α }

def incl : α ↪ ℕ :=
function.embedding.mk encodable.encode encodable.encode_injective

def codes := finset.map incl αs

def code :=
match codes.max with
| none :=  0
| some n := (n+1)
end
local notation ‹ p › := (show p, by assumption)

example : ∀ c ∈ codes, c < code :=
begin
intros,
cases (finset.max_of_mem ‹c ∈ codes›) with m,
have : codes.max = some m,  from ‹m ∈ codes.max›,
have : code = m + 1, by {
rw code,
rw ‹codes.max = some m›,
refl,
},
show c < code, from
calc
c ≤ m : by {apply finset.le_max_of_mem, repeat {assumption}}
... < m + 1 : by apply nat.lt_succ_self
... = code : by {symmetry, from ‹code = m + 1›},
done,
end

end


#### Rob Lewis (Nov 26 2019 at 19:25):

Perhaps this is not an interesting thing to try and do

I'm not sure it's uninteresting, but it's definitely nonstandard. You'll run into issues sooner or later.

#### Reuben Rowe (Nov 26 2019 at 19:27):

This works fine for me?

Yes, you are right, it is. So something else about the rest of my code is causing the problem.

#### Rob Lewis (Nov 26 2019 at 19:28):

Note that I changed show : c < code to show c < code.

#### Rob Lewis (Nov 26 2019 at 19:28):

But that's probably unrelated.

#### Reuben Rowe (Nov 26 2019 at 19:57):

OK, here is the code that displays what I was seeing.

import data.equiv.denumerable

universe u

local notation ‹ p › := (show p, by assumption)

section

parameters { α : Type u } [denumerable α] { αs : finset α }

private
def incl : α ↪ ℕ :=
function.embedding.mk encodable.encode encodable.encode_injective

private
def codes := finset.map incl αs

private
def code :=
match codes.max with
| none :=  0
| some n := (n+1)
end

parameter ( αs )

def fresh_var : α :=
denumerable.of_nat α code

example : fresh_var ∉ αs :=
begin
have : ∀ c ∈ codes, c < code, by {
intros,
cases (finset.max_of_mem ‹c ∈ codes›) with m,
have : codes.max = some m,
by assumption,
-- from ‹m ∈ codes.max›,
have : code = m + 1, by {
rw code,
rw ‹codes.max = some m›,
-- rw this,
refl,
},
show c < code, from
calc
c ≤ m : by {apply finset.le_max_of_mem, repeat {assumption}}
... < m + 1 : by apply nat.lt_succ_self
... = code : by {symmetry, from ‹code = m + 1›},
done,
},
sorry
end

end


Now the problem is the use of the private keyword --- removing it, the code is fine.

I guess I have misunderstood the purpose of this keyword: my intention was that the definitions should not be visible outside of the section (or some other unit) in which they are declared.

#### Reid Barton (Nov 26 2019 at 20:05):

I vaguely recall seeing something like this... maybe an interaction between private and parameters?

And tactic mode

#### Reuben Rowe (Nov 26 2019 at 20:07):

If you remove the local notation for the french brackets, you see the problem I was originally describing (i.e. the assumption tactic finding the wrong assumption). This is whether the private keyword is used or not.

If you include the local notation, but put private on the definitions for both codes and code, you see a problem due to extra goals being generated.

Last updated: May 09 2021 at 19:11 UTC