Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

(No equational lemmas)/(Mistaken as field notation) when using a namespace inside a section with universe polymorphism #613

Open
1 task done
winestone opened this issue Sep 6, 2021 · 0 comments

Comments

@winestone
Copy link

winestone commented Sep 6, 2021

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

Allowing a namespace inside a section can cause compile issues.

Steps to Reproduce

  1. Compile the following code:
    section
      universes u
    
      inductive my_unit : Type u
      | foo
    
      namespace my_unit
        def one : ℕ := 1
      end my_unit
    
      lemma test : my_unit.one = 1 := by refl
    end

Expected behavior: Code compiles, in particular, my_unit.one isn't treated as field notation.

Actual behavior: Obtain error message:

invalid field notation, type is not of the form (C ...) where C is a constant
  my_unit
has type
  Type u

Reproduces how often: 100%

Versions

  • Lean (version 3.32.1, commit 35b3a9c, Release) on cygwin.

Additional Information

If you rephrase the code, you can also get another issue which I think is related:

section
  universes u

  inductive my_unit : Type u
  | foo

  def my_unit.one (_ : my_unit) : ℕ := 1

  lemma test : my_unit.one my_unit.foo = 1 := by unfold my_unit.one
end

gives:

unfold tactic failed, my_unit.one does not have equational lemmas nor is a projection
state:
⊢ my_unit.foo.one = 1

There some small adjustments I've been able to make to get either example to compile. I think the second and third qualifies as a workaround.

  • Don't use universe polymorphism.
    section
      inductive my_unit : Type
      | foo
    
      namespace my_unit
        def one : ℕ := 1
      end my_unit
    
      lemma test : my_unit.one = 1 := by refl
    end
  • Move the namespace out of the section.
    section
      universes u
    
      inductive my_unit : Type u
      | foo
    end
    
    namespace my_unit
      universes u
      def one : ℕ := 1
      -- other code which uses `u`
    end my_unit
    
    section
      universes u
      lemma test : my_unit.one = 1 := by refl
    end
  • Use _root_.
    section
      universes u
    
      inductive my_unit : Type u
      | foo
    
      namespace my_unit
        def one : ℕ := 1
      end my_unit
    
      lemma test : _root_.my_unit.one = 1 := by refl
    end

Hopefully I haven't made any mistakes or missed an issue/PR, I couldn't find anything related when searching for both "namespace" and "section".

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant