Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

9
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Feb 29 at 8:32
  • $\begingroup$ 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. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Feb 29 at 11:01
  • $\begingroup$ @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. $\endgroup$
    – Mike Shulman
    Commented Feb 29 at 16:35
  • 1
    $\begingroup$ @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. $\endgroup$
    – Mike Shulman
    Commented Feb 29 at 18:09
  • 1
    $\begingroup$ @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). $\endgroup$
    – Andrej Bauer
    Commented Feb 29 at 21:30