{"action":"opened","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/692","labels_url":"https://api.github.com/repos/leanprover/lean/issues/692/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/692/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/692/events","html_url":"https://github.com/leanprover/lean/issues/692","id":90512679,"number":692,"title":"folding inductive definitions","user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/leanprover/lean/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-06-23T23:09:42Z","updated_at":"2015-06-23T23:09:42Z","closed_at":null,"body":"Suppose we define a function `f` by induction on the natural numbers. We often want to give such `f` the `[unfold-c _]` attribute, because then `f` is simplified when it is applied to either `0` or `succ`.\r\n\r\nHowever, the inductive calls of `f` should be folded back. For example, `f (succ n)` should reduce to `F n (f n)` and not to `F n (nat.rec_on n _ F)`. Example:\r\n\r\n```lean\r\n-- standard\r\nimport data.nat\r\nopen nat\r\ndefinition f [unfold-c 1] (n : ℕ) : ℕ := nat.rec_on n 1 (λn' p, succ (succ p))\r\n\r\nexample (n : ℕ) : f n = 2 * n + 1 :=\r\nbegin\r\n  induction n,\r\n  { reflexivity},\r\n  { esimp, state, fold (f a), state, rewrite [mul_succ, v_0]}\r\nend\r\n```\r\nHere the `fold` command should be done automatically.\r\n\r\nI think we briefly discussed this in the past (although I cannot find it now), but didn't find a good solution. However, I think it is an imortant issue, since I'm now doing a lot of folding by hand:\r\nhttps://github.com/fpvandoorn/lean/blob/9bb703eeec28e9f289a417f3599e22de409421a6/hott/algebra/e_closure.hlean#L99-106\r\n\r\nHere's my idea:\r\n* when we run `esimp`, we keep a list of items which should be folded afterwards\r\n* e.g. if `esimp` unfolds `f (succ n)`, we add `f n` to the list\r\n* after we are done with esimp, we run `try fold x` for every element `x` in the list\r\n* If we execute `esimp [f]` I think we should *not* add any terms with head `f` to the list.\r\n* The main challenge is to determine which terms to add to the list. Difficulties:\r\n  * If we unfold `f (succ (succ n))` we should add `f n` but don't need to add `f (succ n)`. So we need to strip constructors until we the head of the argument is not a `[constructor]` anymore. Here `n` needs not be a variable, as long as its head is not a `[constructor]`\r\n  * For inductive families we should also adapt indices: If we unfold `g` in `g (succ n) (vector.cons a v)`, we should store `g n v`. The relevant indices can be read of from the type of the constructor.\r\n  * Unfolding/Folding should be done in the right order: if we simplify `f (succ (f (succ n)))` we want to fold both `f`'s back\r\n  * One unfold can lead to multiple folds, e.g. if we define\r\n```lean\r\ninductive tree (A : Type) : Type :=\r\n| leaf : A → tree A\r\n| node : tree A → tree A → tree A\r\n```\r\nand we unfold `f (node a b)` we need to add both `f a` and `f b`. And of course, it can lead to zero unfolds, for example if we unfold `f leaf`\r\n"}}