# Tag Info

Accepted

### Termination and confluence -- which goes first?

As you have noticed there is no "natural" way to prove confluence and termination: to prove confluence from local confluence you need termination, but proving termination often depends on ...
• 506

### Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
• 9,593

### Universe inconsistency as an effect

I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature. Some background information Computational effects and dependent ...
• 9,593

### Strictly-monotone "max" operation for constructive Brouwer-trees?

You can define a max that will be better behaved by induction on x and y. Something like: <...
• 982
Accepted

### How to prove termination of mutually recursive functions if only some decrease their arguments?

The trick is to "order" the functions themselves by using a product as the measure. Here's a working example: ...

### Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete? Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
• 1,256
Accepted

### How to provide proof for termination in Agda?

There are three possible approaches: Use a different algorithm, like division in stdlib, see div-helper. Use the well-founded induction library. There are many ...
• 6,276

### How to prove the termination of Ackermann in Lean?

Usually x-1 is harder to work with (but not impossible). Pattern matching is much easier from a type theoretic perspective. So (this is actually one of the test ...
• 4,015
Accepted

### proof of termination for zip in Lean

It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are ...
• 5,186
Accepted

### How to convince Agda that definition is terminating in the presence of unapplied recursion?

I can think of two ways of solving the problem. First, make All and Value mutually recursive so that you don't have to pass <...
• 9,593

### Defining a terminating ripple, with arguments swapping places

Idris is also happy with this definition: ...
• 1,256

### Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?

It's consistent to interpret the type of strict propositions as the type of double negation stable propositions (or more generally as $j$-stable propositions for any given Lawvere-Tierney topology $j$)...
• 301

### Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?

Sadly, a big issue of strict propositions is that in their current form they validate very little choice principles. For instance, I don't think that your example is provable. Indeed, Pujet and ...
• 5,186

### How to prove the termination of Ackermann in Lean?

With dependent types and the awesome prelude of Lean 4, one can define the Ackermann function in any equivalent way as long as the definition is constructive. However, the more closely the definition ...

### Defining a terminating ripple, with arguments swapping places

In Lean 4, this is done using well-founded recursion by specifying a termination measure: ...

### proof of termination for zip in Lean

The answer by Meven Lennon-Bertrand is exactly right, but the best way to ensure you are doing structural recursion is to avoid writing the match statement in the first place: ...
• 8,960
Accepted

### How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

For reference, in Coq, termination checking “just works” on this function: ...
• 1,053

### How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

The part of Lean that tries to determine whether recursion is well-founded does not look inside definitions (it's dangerous to do so when one is dealing with recursive definitions). You can solve the ...
• 9,593

### How to prove the termination of Ackermann in Lean?

Here's a variant that doesn't require termination_by: ...
Accepted

### Using decreasing_by to prove termination in Lean 4

You can follow the examples in TPIL4 Chapter 8. (Edit: This answer is for the new syntax, which changed in Lean 4.6. See the 4.6 release notes for a comparison with the former syntax.) In particular:...
• 8,960

### Defining a terminating ripple, with arguments swapping places

HOL4's automatic search for a well-founded termination relation succeeds in this case, so you need only write: ...
• 1,112