Zulip Chat Archive

Stream: new members

Topic: multiple assumptions of definitionally equal type


view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:31):

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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Nov 26 2019 at 18:32):

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

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:32):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Nov 26 2019 at 18:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 26 2019 at 18:34):

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

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:35):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 26 2019 at 18:53):

That error looks weird

view this post on Zulip Reid Barton (Nov 26 2019 at 18:54):

How did you define the notation exactly?

view this post on Zulip 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.

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:54):

How did you define the notation exactly?

notation p := (show p, by assumption)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 26 2019 at 18:57):

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

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:58):

The latter.

view this post on Zulip Reuben Rowe (Nov 26 2019 at 18:59):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 26 2019 at 19:05):

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

view this post on Zulip Rob Lewis (Nov 26 2019 at 19:09):

This is hard to follow without a working example.

view this post on Zulip Reuben Rowe (Nov 26 2019 at 19:11):

OK, I'll give the code.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Nov 26 2019 at 19:28):

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

view this post on Zulip Rob Lewis (Nov 26 2019 at 19:28):

But that's probably unrelated.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 26 2019 at 20:05):

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

view this post on Zulip Reid Barton (Nov 26 2019 at 20:05):

And tactic mode

view this post on Zulip 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