MergeSort

Agda : 2.6.2.1

agda-stdlib-1.7.1

coq 8.15.1

4 way to prove correctness 1 way to prove permutation

Definition of merge and proof of correctness

Based on different definition of merge, we have multiply way to prove sorted property.

MergeSort.agda : single definition, single correctness

single-mutual.agda : single definition, mutual correctness

mutual-mutual.agda : mutual definition, mutual correctness

	Agda		Coq
	use `with` to define merge	define merge mutually	Fixpoint	function
nested recursion	?	?	ok	todo
mutual recursion	single-mutual	mutual-mutual	-	todo
length + length	length-decrease	mutual-length-decrease	ok	todo
other tactic	with	-	-	functional induction

Proof of permutation

Only one way avaiable.

Proof of time complexity

TODO