Переводить определения Coq в agda?

Question

Мне интересно, существует ли системный c способ интерпретации определений Coq как программ agda. Я работаю над переводом части основ программирования и не могу заставить функцию tUpdate работать ниже. Почему это не удается? Код coq прокомментирован.

--Definition total_map (A : Type) := string -> A.

totalMap : Set → Set
totalMap A = String → A

-- Definition t_empty {A : Type} (v : A) : total_map A :=
-- (fun _ => v).

tEmpty : {A : Set} (v : A) → totalMap A
tEmpty = λ v x → v

-- Definition t_update {A : Type} (m : total_map A)
-- (x : string) (v : A) :=
-- fun x' => if eqb_string x x' then v else m x'.

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → Set 
tUpdate m x v = λ x' → (if (x == x') then v else m x')

Лямбда-член приводит к появлению ошибки ниже ?

Редактировать:

Я понял, что обновление должно было вернуть карту, но я в замешательстве, так как coq может предположить это, а agda - нет? Я бы все же приветствовал более общий ответ на последний вопрос.

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → totalMap A
tUpdate m x v = λ x' → (if (x == x') then v else m x') 

Answer 1

Coq и Agda оба основаны на очень грубо одной и той же теории зависимых типов, поэтому в теории можно было бы взять проверочный термин, сгенерированный сценарием Coq, и преобразовать его в программу Agda. Тем не менее, есть много небольших (и не очень маленьких) различий, например, непредсказуемый Пропорция Кока, совокупность, различия в проверках завершения и т. Д., Которые сделают такой перевод трудным или невозможным.

Однако, что вы ' Запрашиваемый здесь не действительно автоматический переводчик c, а скорее набор правил для перевода Coq в Agda вручную. Поскольку многие базовые функции c могут быть сопоставлены один к одному, этот процесс намного проще. Однако любое использование тактики в коде Coq вам придется либо преобразовать в явный проверочный термин в Agda, либо написать свои собственные макросы отражения Agda (поскольку для Agda еще нет полной библиотеки tacti c).

Чтобы ответить на конкретную проблему c, с которой вы здесь столкнулись: Agda не пыталась определить тип возвращаемого значения функции tUpdate, потому что вы уже указали, что она Set самостоятельно. Если вы хотите, чтобы Agda сделала для вас вывод, вы можете просто заменить тип возвращаемого значения подчеркиванием _ (что в данном случае работает нормально):

tUpdate : {A : Set} (m : totalMap A) (x : String) (v : A) → _
tUpdate m x v = λ x' → (if (x == x') then v else m x')