Questions tagged [list-manipulation]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
4 answers
760 views

Defining a terminating `ripple`, with arguments swapping places

In Agda, I can make the following definition, and Agda believes that the recursion terminates. Notice that the arguments “swap places” in the recursive call, so neither of the arguments individually ...
James Wood's user avatar
1 vote
0 answers
60 views

Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other

Require Import Coq.Lists.List. I have the following properties defined on a list of natural numbers: ...
Agnishom Chattopadhyay's user avatar
1 vote
2 answers
110 views

Partitioning a list with 2 elements in the middle in coq

I am trying to prove some theorems using sequent calculus, for some parts (e.g. cases with Exchange rule) I need a theorem like below ...
asha soroushpoor's user avatar
1 vote
1 answer
95 views

How to prove this correctness principle of transposition of lists of lists in Coq?

I have defined the function transpose as follows: ...
Agnishom Chattopadhyay's user avatar