1
Я пытаюсь написать следующую функцию:Agda: доказать, что, когда значения равны, то их аргументы конструктора равны
justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}
Я не знаю, как написать это. Для меня это интуитивно для аксиоматики, но компилятор не принимает refl как доказательство этого.
Я, как правило, должен доказывать такие вещи, например, показывая, что если два непустых списка равны, то их головы равны.
Каков общий подход к этому вопросу? Связано ли это с «зеленым слизком» Конора Макбрайда о функциях в возвращении конструкторов?
Вы пробовали сопоставление образцов на 'pf'? – Vitus
emacs просто расширяет его до 'refl' ... Мне, вероятно, не хватает очевидного, но я не вижу, как это помогает. – jmite
Мне кажется, что 'cong' будет полезен здесь, но я не знаю, как написать функцию, которая принимает' just x' в 'x', поскольку она по своей сути будет частичной. – jmite