Timeline for Binding variables to terms involving later variables
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 1 at 7:49 | answer | added | James McKinna | timeline score: 7 | |
| Mar 1 at 6:59 | history | edited | Mike Shulman | CC BY-SA 4.0 |
with indices, it seems that more extensive permutation of the context may be needed
|
| Feb 29 at 22:07 | comment | added | Andrej Bauer | Yes, I realized that was the case after reading Meven's answer. | |
| Feb 29 at 22:01 | comment | added | Mike Shulman | @AndrejBauer Agda only has pattern-matching on variables. Is it not general enough? To match against an arbitrary term, you just define a general function by of a variable by pattern-matching and then apply the function to the term. | |
| Feb 29 at 21:31 | comment | added | Andrej Bauer |
@MikeShulman: Do you expect the special case of n a variable to be generally useful, or do you have a special case in mind that you care about? A general proof assistant just wouldn't bother worrying about your example, because it's not general enough.
|
|
| Feb 29 at 21:30 | comment | added | Andrej Bauer |
@MevenLennon-Bertrand: Your example shows that there is too little deductive power (can't deduce x = y from suc x = suc y), not that equalities themselves are too weak (you managed just fine using them to explain what you want).
|
|
| Feb 29 at 18:09 | comment | added | Mike Shulman | @MevenLennon-Bertrand Of course, but in that case my pseudo-syntax is not expressive enough, since you need to specify the motive by hand. As you pointed out in the last paragraph of your answer, you can't in general expect the proof assistant to guess it, because higher-order unification is undecidable. | |
| Feb 29 at 18:06 | comment | added | Meven Lennon-Bertrand♦ | What do you mean? Surely you can do induction with a dependent motive, even when the argument is not a variable? | |
| Feb 29 at 16:35 | comment | added | Mike Shulman |
@AndrejBauer Restricting to n being a variable is what allows the motive to be refined in the branches. Otherwise you have only a recursion principle, not an induction principle.
|
|
| Feb 29 at 15:53 | history | became hot network question | |||
| Feb 29 at 11:01 | comment | added | Meven Lennon-Bertrand♦ |
The problem with judgmental equalities is that they are slightly too weak in this context, because they are a priori not injective: in many of these cases, you get equations like suc x = suc y, and you really want to be able to conclude x = y instead. This kind of injectivities is an important step of the work Equations or Program do in Coq.
|
|
| Feb 29 at 10:59 | answer | added | Meven Lennon-Bertrand♦ | timeline score: 5 | |
| Feb 29 at 8:32 | comment | added | Andrej Bauer |
The general case here is that n is an expression, not a variable. Is there some reason you are specializing to a variable only? I do not know how existing proof assistants do it, but precisely for this sort of reason Andromeda (and finitary type theories that it's based on) allows judgemental equations in contexts.
|
|
| Feb 29 at 7:49 | history | asked | Mike Shulman | CC BY-SA 4.0 |