{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/921","labels_url":"https://api.github.com/repos/leanprover/lean/issues/921/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/921/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/921/events","html_url":"https://github.com/leanprover/lean/issues/921","id":121591326,"number":921,"title":"Extending (semi-)concrete structures","user":{"login":"dselsam","id":4520285,"avatar_url":"https://avatars.githubusercontent.com/u/4520285?v=3","gravatar_id":"","url":"https://api.github.com/users/dselsam","html_url":"https://github.com/dselsam","followers_url":"https://api.github.com/users/dselsam/followers","following_url":"https://api.github.com/users/dselsam/following{/other_user}","gists_url":"https://api.github.com/users/dselsam/gists{/gist_id}","starred_url":"https://api.github.com/users/dselsam/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dselsam/subscriptions","organizations_url":"https://api.github.com/users/dselsam/orgs","repos_url":"https://api.github.com/users/dselsam/repos","events_url":"https://api.github.com/users/dselsam/events{/privacy}","received_events_url":"https://api.github.com/users/dselsam/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-12-10T22:27:35Z","updated_at":"2015-12-11T21:25:15Z","closed_at":"2015-12-10T23:01:09Z","body":"This issue comes courtesy of Nathaniel Thomas:\r\n\r\n```Lean\r\nimport algebra.field data.real\r\nopen algebra real\r\n\r\nstructure has_scalar [class] (F V : Type) :=\r\n(smul : F → V → V)\r\n\r\nstructure vector_space [class] (F V : Type) extends has_scalar F V, field F :=\r\n(idcomp   : ∀ x, smul one x = x)\r\n\r\nstructure binary_to_real [class] (V : Type) :=\r\n(ip : V → V → ℝ)\r\n\r\nstructure real_inner_product [class] (V : Type) extends binary_to_real V, vector_space ℝ V :=\r\n(positivity : ∀ (v : V), ((ip v v) ≥ 0))\r\n\r\nset_option pp.all true\r\nset_option pp.numerals false\r\n\r\ndefinition positivity {V : Type} [inner : real_inner_product V] (v : V) \r\n  : real_inner_product.ip v v ≥ 0 :=\r\n@real_inner_product.positivity V inner v\r\n```\r\nyields\r\n```\r\nerror: type mismatch at definition 'positivity', has type\r\n  ∀ (V : Type.{?M_1}) (inner : real_inner_product.{?M_1} V) (v : V),\r\n    @ge.{1} real 11.source.to.has_le_3 (@real_inner_product.ip.{?M_1} V inner v v)\r\n      (@zero.{1} real 11.source.to.has_zero_3)\r\nbut is expected to have type\r\n  ∀ {V : Type.{?M_1}} [inner : real_inner_product.{?M_1} V] (v : V),\r\n    @ge.{1} real 11.source.to.has_le_3 (@real_inner_product.ip.{?M_1} V inner v v)\r\n      (@zero.{1} real (@real_inner_product.to.has_zero.{?M_1} V inner))\r\n```\r\nThe issue is that by extending the semi-concrete structure `vector_space ℝ V`, we have introduced a new instance of `@zero ℝ` that has no actual definition, and in particular is not definitionally equal to the standard instance.\r\n\r\nWhat is the recommended solution for this kind of problem?\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/164051225","html_url":"https://github.com/leanprover/lean/issues/921#issuecomment-164051225","issue_url":"https://api.github.com/repos/leanprover/lean/issues/921","id":164051225,"user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"created_at":"2015-12-11T21:25:14Z","updated_at":"2015-12-11T21:25:14Z","body":"Here are some thoughts. When we do abstract algebra, it will be convenient to use bundled structures:\r\n\r\n   https://github.com/leanprover/lean/blob/master/library/algebra/bundled.lean\r\n\r\nThat way, we can write\r\n```lean\r\nvariable F : Field\r\nvariable V : VectorSpace F\r\n```\r\ninstead of\r\n```lean\r\nvariable F : Type\r\nvariable [fieldF : field F]\r\ninclude fieldF\r\nvariable V : Type\r\nvariable [vector_space_FV] : vector_space F V\r\ninclude V\r\n```\r\nSimilarly we can write\r\n```lean\r\nvariables F₁ F₂ : Field \r\nvariables (V₁ : VectorSpace F₁) (V₂ : VectorSpace F₂)\r\n```\r\nrather than the much more verbose alternative. It is clunky to manage the \"includes,\" i.e. turn them off or on manually depending on whether a theorem or definition needs them. Also, there is no need to make class inference search for the relevant instance when it can be bundled into the types. Similarly, I think we want a linear operator to be a bundled structure (function + properties) between (bundled) vector spaces,\r\n```lean\r\nvariable T : LinearOperator V₁ V₂\r\n```\r\nand so on,\r\n\r\nBundled structures are used extensively in Floris' category theory library, and we are similarly starting a group theory library based on them, so we can write\r\n```lean\r\nvariable G : Group\r\nvariables H K : Subgroup G\r\n```\r\nThe thing is, when we do calculations with concrete vector spaces, I think we want the partially bundled versions. E.g. we may have\r\n```lean\r\nx y : vector real n\r\nc : real\r\n```\r\nand we want to write x + y or  smul c x  and have the system find the structure.\r\n\r\nThen the solution should be to do what we currently do with groups: use the partially bundled versions for calculations in the structure, and then bundle them up when we want to define operations on groups, etc. \r\n\r\nThe thing is, there are two things we can bundle or unbundle, namely, vector space and the field. At first, I thought we would want to keep the bundled structure for the underlying field, and only unbundle the vector space:\r\n```lean\r\nvariable F : Field\r\nvariable V : Type\r\nvariable [vector_space_F_V] : vector_space F V\r\n```\r\nBut that doesn't seem to work: in the case above, given x : vector real n, there is no way for class inference to find the F (in this case, the bundled real field structure).\r\n\r\nIn short, it seems to me that for concrete structures, we want to use the approach you have described here (with the field structure and vector space structure discovered by class inference). When we move to algebra, if we want to bundle things up, we bundle up both at once.\r\n\r\nI am just thinking out loud here, but if you think I am missing something, let me know.\r\n"}}