mutual-merge.agda

open import Data.String as String using (String; fromList)
open import Data.Nat              using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
open import Data.Nat.Properties  
open import Data.Bool             using (Bool; true; false; if_then_else_)
open import Data.List   hiding (merge; partition)
open import Data.List.Properties  using (map-id; map-compose)
open import Data.Product          using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
open import Data.Sum   as Sum     using (_⊎_; inj₁; inj₂; map)
open import Data.Unit             using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; cong-app; sym; trans; subst; module ≡-Reasoning)
open ≡-Reasoning
open import Relation.Nullary      using (¬_; Dec; yes; no)
open import Induction.WellFounded
open import Relation.Binary
open import Data.Nat.Induction


mutual
  merge : List ℕ -> List ℕ -> List ℕ
  merge [] x₁ = x₁
  merge (x ∷ x₂) [] = x ∷ x₂  
  merge (x ∷ xs) (y ∷ ys) with x ≤? y
  merge (x ∷ xs) (y ∷ ys) | yes _ = x ∷ merge xs (y ∷ ys)
  merge (x ∷ xs) (y ∷ ys) | no _ = y ∷ merge' x xs ys
  
  merge' : ℕ -> List ℕ -> List ℕ -> List ℕ
  merge' x x₁ [] = x ∷ x₁
  merge' x xs (y ∷ ys) with  x ≤? y
  merge' x xs (y ∷ ys)  | yes _ = x ∷ merge xs (y ∷ ys)
  merge' x xs (y ∷ ys)  | no _ = y ∷ merge' x xs ys

Require Import Le Lt Gt Decidable PeanoNat Recdef.

Fixpoint merge (l1 l2 : list nat) : list nat  :=
  match l1, l2 with
  | nil , _ => l2
  | _, nil => l1
  | cons a1 l1' , cons a2 l2' =>
      if ( a1 <=? a2 ) then ( a1 :: merge l1' l2 ) else ( a2 :: merge_aux a1 l1' l2')
  end
with merge_aux (a1 : nat) (l1 l2 : list nat) :=
  match l2 with
  | nil => a1 :: l1
  | cons a2 l2' => if (a1 <=? a2) then a1 :: merge l1 l2 else a2 :: merge_aux a1 l1 l2'
  end.

相同的逻辑分别用agda和coq写
coq无法编译，请教一下原因