multiple assumptions of definitionally equal type

Stream: new members

[Reuben Rowe]

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]

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]

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]

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]

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]

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

[Rob Lewis]

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]

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

[Reuben Rowe]

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

[Rob Lewis]

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]

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

[Reuben Rowe]

@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]

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

[Rob Lewis]

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

[Reid Barton]

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

[Reuben Rowe]

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

[Reuben Rowe]

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]

That error looks weird

[Reid Barton]

How did you define the notation exactly?

[Reuben Rowe]

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

[Reuben Rowe]

How did you define the notation exactly?

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

[Reid Barton]

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]

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]

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]

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

[Reuben Rowe]

The latter.

[Reuben Rowe]

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

[Reid Barton]

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]

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

[Rob Lewis]

This is hard to follow without a working example.

[Reuben Rowe]

OK, I'll give the code.

[Reid Barton]

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

[Reuben Rowe]

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]

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]

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]

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]

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]

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

[Rob Lewis]

But that's probably unrelated.

[Reuben Rowe]

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]

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

[Reid Barton]

And tactic mode

[Reuben Rowe]

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.