{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/804","labels_url":"https://api.github.com/repos/leanprover/lean/issues/804/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/804/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/804/events","html_url":"https://github.com/leanprover/lean/issues/804","id":101535285,"number":804,"title":"Any thoughts on matrix inverses?","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":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-08-18T00:04:03Z","updated_at":"2015-08-18T16:22:14Z","closed_at":null,"body":"Similar to #650, there are many options for representing matrix inverses. I'll list a few that come to mind.\r\n```Lean\r\ndefinition inverse_of (M : matrix A n n) (N : matrix A n n) :=\r\nM * N = I ∧ N * M = I\r\n```\r\n\r\n(1) We can use type-class inference to propagate `∃ N, inverse_of M N` along e.g. multiplication and transpose, and then use classical choice:\r\n```Lean\r\ndefinition invertible [class] (M : matrix A n n) :=  ∃ N, inverse_of M N\r\nnoncomputable definition inverse (M : matrix A n n) := classical.epsilon (inverse_of M)\r\nnotation A⁻¹ := inverse A \r\nlemma inverse_spec (M : matrix A n n) [M_invertible : invertible M] \r\n: inverse_of M M⁻¹ := classical.epsilon_spec M_invertible\r\n```\r\nPros: simple\r\nCons: does not compute, returns meaningless matrix if not invertible.\r\n\r\n(2) We can use type-class inference to propagate a proposition that a specific inverse algorithm takes as an argument, and then use that algorithm itself:\r\n```Lean\r\ndefinition invertible [class] (M : matrix A n n) := det M ≠ 0\r\ndefinition compute_inverse (M : matrix A n n) [M_invertible : invertible M]\r\n:= (det M)⁻¹ * adjugate M\r\nnotation A⁻¹ := compute_inverse A \r\nlemma inverse_spec (M : matrix A n n) [M_invertible : invertible M] \r\n: inverse_of M M⁻¹ := ... -- an actual proof\r\n```\r\nPros: constructive\r\nCons: no algorithm choice\r\n\r\n(3) We can use type-class inference to propagate the actual inverse as data, and can toggle between inverse algorithms by setting priorities for the base case:\r\n```Lean\r\ndefinition invertible [class] (M : matrix A n n) := Σ N, inverse_of M N\r\ndefinition project_inverse (M : matrix A n n) [M_invertible : invertible M]\r\n:= M_invertible\r\nnotation M⁻¹ := (project_inverse M).1\r\nlemma inverse_spec (M : matrix A n n) [M_invertible : invertible M] \r\n: inverse_of M M⁻¹ := (project_inverse M).2\r\n```\r\nPros: constructive, algorithmically flexible\r\nCons:  `M⁻¹` may not be definitionally equal `M⁻¹`\r\n\r\n(I haven't given up hope that subsingleton-equality can be handled nicely in the elaborator, though maybe I am alone on this.)\r\n\r\nThere are of course several other options as well. One of the main design issues seem to be how much to support computing using the same symbols and data-structures we use for math. One hypothesis is that they are such separate endeavors that one should switch to an entirely different mode when one needs to compute efficiently. \r\n\r\nAny thoughts?"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/132265376","html_url":"https://github.com/leanprover/lean/issues/804#issuecomment-132265376","issue_url":"https://api.github.com/repos/leanprover/lean/issues/804","id":132265376,"user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"created_at":"2015-08-18T16:22:14Z","updated_at":"2015-08-18T16:22:14Z","body":"> (I haven't given up hope that subsingleton-equality can be handled nicely in the elaborator, though maybe I am alone on this.)\r\n\r\nYou are not alone :-)\r\nI didn't give up either.\r\n\r\nThat being said, the `matrix` type should be viewed as a \"reference type\" for matrices.\r\nWe are defining it as `fin n -> fin m -> A`. \r\nSimilarly, `nat` is the reference type for natural numbers.\r\nBoth of them are simple, but do not have good computational behavior.  \r\nSo, I think it is not very useful to support multiple implementations.\r\nIn the long term, we will define \"efficient representations\" for theses types (e.g., a sparse representation for matrices), prove equivalences between them, and transport results/theorems.\r\n"}}