Вопросы по теме 'agda'
Работа над аксиомами Пеано в Агде и наткнулся на камень преткновения
PA6 : ∀{m n} -> m ≡ n -> n ≡ m
это аксиома, которую я пытаюсь решить и поддержать, я пытался использовать конг (из основной библиотеки), но у меня проблемы с конструктором конг
PA6 = cong
ни к чему меня не приводит, я знаю, что...
676 просмотров
schedule
12.06.2022
Устранение subst для доказательства равенства
Я пытаюсь представить счетчики mod-n как разрез интервала [0, ..., n-1] на две части:
data Counter : ℕ → Set where
cut : (i j : ℕ) → Counter (suc (i + j))
Используя это, определить две важные операции несложно (некоторые доказательства...
248 просмотров
schedule
21.04.2024
Agda: пара векторов одинаковой длины
Как в Agda определить пару векторов одинаковой длины?
-- my first try, but need to have 'n' implicitly
b : ∀ ( n : ℕ ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n)
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ [])
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])
b _ = _
-- how can...
795 просмотров
schedule
28.06.2022
Последствия экземпляра для проверки типа
Я изучаю, как в Agda реализованы «классы типов». В качестве примера я пытаюсь реализовать римские цифры, композиция которых с # будет проверять тип.
Я не понимаю, почему Agda жалуется, что нет экземпляра для Join (Roman _ _) (Roman _ _) _ -...
131 просмотров
schedule
01.03.2023
вставка двойного отрицания в agda
Мне нужны пояснения по поводу двойных отрицаний в agda.
Несмотря на то
z≡z : 0 ≡ 0
z≡z = refl
Не могу понять, как доказать:
¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥
¬¬z≡z ?
Это длинная рука для ¬ (0 ≢ 0) . Возможно, я где-то пропустил идиому...
274 просмотров
schedule
27.02.2024
Agda: Почему я не могу найти совпадение с образцом по ссылке?
Я пытаюсь доказать что-то о делимости целых чисел. Сначала я попытался доказать, что делимость рефлексивна.
∣-refl : ∀{n} → n ∣ n
Потому что я определил делимость на основе вычитания ...
data _∣_ : ℤ → ℤ → Set where
0∣d : ∀{d} → zero ∣...
708 просмотров
schedule
21.03.2024
Как применить разрешимые, когда они известны?
Я пытаюсь доказать, что вставка дерева бинарной сортировки. Я нахожусь в середине доказательства, и среда выглядит так:
-- new rx : ℕ
Goal: SortedTree (node leaf x (node (insertTree new rl) rx rr))
Have: SortedTree (insertTree new (node rl...
68 просмотров
schedule
18.08.2022
Нетрудные доказательства преобразований AST в Agda
Я нахожусь в главе "простые императивные программы" в Software Foundations, попутно выполняя упражнения с Agda. В книге отмечается, что создание доказательств на AST-s утомительно, и продолжается представление средств автоматизации в Coq.
Как...
310 просмотров
schedule
22.05.2023
Использование перезаписи внутри цели не верхнего уровня требует вспомогательной функции?
У меня есть формализация Agda-исчисления с индексами де Брейна. Большая часть настройки не имеет отношения к моей проблеме, поэтому я буду использовать пустые типы для переименований Ren и действий и просто постулирую базовое переименование sucᴿ ,...
54 просмотров
schedule
13.08.2023
Неразрешимые ограничения размера
Я хочу определить функцию сохранения размера при выводе отношения перехода для исчисления числа Пи. Я не могу убедить Агду в том, что он действительно сохраняет размер. Я также получаю сообщение об ошибке, которое кажется бессмысленным, так что,...
55 просмотров
schedule
05.02.2022
Эквивалентность поиска плоской матрицы и 2D-матрицы (доказательство) — стремление к большей элегантности
У меня есть доказательство (очевидного) утверждения о том, что поиск элементов в сплющенном представлении матрицы в виде вектора длины m * n совпадает с представлением вектора вектора. Но мое доказательство кажется неуклюжим. [Я не буду приводить...
52 просмотров
schedule
25.12.2023
Универсальное программирование Arity в Agda
Как написать общие функции арности в Agda? Можно ли написать полностью зависимые и полиморфные вселенную общие функции с арностью?
655 просмотров
schedule
17.10.2022
Как сравнить Векторы натов в Агде
Я пытаюсь использовать Decidable Equality для сравнения двух векторов Nats в Agda. Я попытался открыть модуль Vector Equality, передав в качестве аргумента Nat DecSetoid следующим образом:
open import Data.Nat
open import Data.Vec
open import...
234 просмотров
schedule
18.08.2023
Саморепрезентация и вселенные в ОТТ
Вопрос касается теории наблюдательных типов .
Рассмотрим этот параметр:
data level : Set where
# : ℕ -> level
ω : level
_⊔_ : level -> level -> level
# α ⊔ # β = # (α ⊔ℕ β)
_ ⊔ _ = ω
_⊔ᵢ_ : level -> level -> level
α ⊔ᵢ...
187 просмотров
schedule
20.06.2022
Формализация звездной идемпотентности Клини в регулярных выражениях
Я пытаюсь формализовать некоторые свойства регулярных выражений (RE) в Agda. Я застрял на доказательстве идемпотентности звездной операции Клини.
Мне удалось это доказать
xs <-[[ (e *) * ]] -> xs <-[[ e * ]]
т.е. если строка xs...
392 просмотров
schedule
27.11.2023
Мира мало
Я все еще пытаюсь внедрить теорию типов наблюдений в себя и все это в Агду.
В настоящее время у меня есть следующая иерархия вселенных:
Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁
Чтобы определить равенство...
208 просмотров
schedule
10.06.2023
Механизм получения Haskell для Agda
Мне интересно, есть ли в Agda что-нибудь похожее на предложение deriving Eq в Haskell - тогда у меня также есть связанный вопрос ниже.
Например, предположим, что у меня есть типы для игрушечного языка,
data Type : Set where
Nat : Type...
291 просмотров
schedule
13.10.2022
Доказательство `T b`, когда` b` уже совпадает с
Я пытаюсь доказать простое:
open import Data.List
open import Data.Nat
open import Data.Bool
open import Data.Bool.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Unit
repeat : ∀ {a} {A : Set a} → ℕ → A → List A...
71 просмотров
schedule
18.09.2022
Нерелевантные имплициты: почему agda не делает этого доказательства?
Недавно я сделал тип для конечных множеств в Agda со следующей реализацией:
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open...
162 просмотров
schedule
22.11.2023
Отслеживание состояния при написании доказательств равенства, которые представляют собой длинные цепочки транзитивно связанных шагов
Я писал в Идрисе следующее доказательство:
n : Nat
n = S (k + k)
lemma: n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
lemma = sym $
rewrite plusZeroRightNeutral ((k * n) + k) in
rewrite plusAssociative ((k * n) + k) 1 ((k *...
103 просмотров
schedule
27.08.2022
