Описание тега lean
Lean - это средство доказательства теорем с открытым исходным кодом, разрабатываемое Microsoft Research, а его стандартная библиотека - в Университете Карнеги-Меллона. Доказательство теорем Lean направлено на устранение разрыва между интерактивным и автоматическим доказательством теорем.
2
ответа
Как определить частично упорядоченные множества в Lean?
Я хочу доказать эту теорему в доказательстве теоремы Лин. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить infimum / supremum. Как это делается в Lean? В учебнике упоминаются сетоиды, которые я…
27 мар '16 в 18:48
1
ответ
Почему lean добавляет неявные переменные к леммам из eq?
Следующий код имеет странное поведение variable (toto : Type) check eq.symm --output: eq.symm : ?a toto = ?b toto → ?b toto = ?a toto Я ожидал бы, что проверка не учитывает не относящуюся к делу неявную переменную toto, показывая мне тип eq.symm. Эт…
06 июн '16 в 13:56
1
ответ
От включения набора для установления равенства в Lean
Учитывая доказательство включения множества и его обратное, я хотел бы показать, что два множества равны. Например, я знаю, как доказать следующее утверждение и его обратное утверждение: open set universe u variable elem_type : Type u variable A : s…
13 авг '17 в 09:28
1
ответ
Можно ли в Lean использовать decidable_linear_order с пользовательским отношением равенства?
Lean поставляется с decidable_linear_order класс типов, содержащий полезные леммы об упорядочении и его отношении к равенству, такие как: lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a Равенства в э…
08 июл '17 в 05:44
1
ответ
Не могу заставить классы типа работать в Lean
У меня возникли проблемы с пониманием, как вызвать использование классов типов Лин. Вот попытка на небольшом примере: section the_section structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a) definition P A := exists (a : A…
18 июн '16 в 13:51
2
ответа
Индуктивный тип, построенный по списку этого типа в Lean
Я хотел бы определить индуктивный тип, который может быть построен из списка самого себя в Lean. тем не мение inductive a : Type := | aFromAs : list a → a выдает ошибку: failed to infer inductive datatype resultant universe, provide the universe lev…
18 ноя '16 в 01:56
0
ответов
Определение выбора в Lean
В Lean "выбор" реализуется в соответствии с: Наша аксиома выбора теперь выражается просто следующим образом: axiom choice {α : Sort u} : nonempty α → α Учитывая только утверждение h о том, что α непусто, выбор h магически порождает элемент α. Теперь…
19 фев '19 в 11:13
1
ответ
Безболезненный способ показать простое неравенство над целым числом
У меня есть следующее состояние: a : ℕ, a_1 : ℕ, nltm : of_nat a_1 + 1 < of_nat a + 1 ⊢ of_nat a_1 < of_nat a Обратите внимание, что of_nat конструкции Z, Есть ли безболезненный способ достижения цели?
06 янв '18 в 15:08
3
ответа
Как доказать a = b → a + 1 = b + 1 в худой?
Я работаю над 4-й главой учебного пособия. Я хотел бы быть в состоянии доказать простые равенства, такие как a = b → a + 1 = b + 1 без использования среды Calc. Другими словами, я хотел бы явно построить проверочный термин: example (a b : nat) (H1 :…
30 янв '17 в 22:11
1
ответ
Что представляет собой действительный тип в Lean?
Я сделал первые 3 главы бережливого урока, и я уже сделал несколько доказательств в логике высказываний. Сейчас я пытаюсь немного вернуться и задать себе глупые вопросы. Мое понимание таково: Термины могут иметь типы: constant A : Type, A это термин…
07 дек '16 в 20:42
0
ответов
В чем разница между типом и типом *?
Я видел какой-то случай Type* в этом проекте. Бег #check Type* дает Type u_1 : Type (u_1+1) а также #check Type дает Type : Type 1, Выполнение поиска по языковой ссылке и Ctrl-FГлава "Выражения" не дает никакой информации о Type*, Для чего он исполь…
06 окт '18 в 01:41
1
ответ
В чем разница между худой, f* и dafny?
Они из Microsoft и кажутся помощниками? Помимо синтаксических различий, есть ли практические аспекты, которые отличают их друг от друга (например, способность делать автоматизацию, выразительную силу и т. Д.)? Я новичок в формальной проверке. Редакт…
02 сен '17 в 05:57
2
ответа
Почему более новые языки с независимой типизацией не приняли подход SSReflect?
Есть два соглашения, которые я нашел в расширении SSReflect Coq, которые кажутся особенно полезными, но которые я не видел широко принятыми в новых языках с зависимой типизацией (Lean, Agda, Idris). Во-первых, там, где это возможно, предикаты выража…
25 мар '18 в 15:20
1
ответ
Почему я получаю "Значение символа как переменная void: ..." при попытке установить lean-rootdir?
Я загрузил lean для Linux в Ubuntu, распаковал его, установил Emacs, установил lean-mode и company-lean через MELPA, жалуется, что переменная lean-rootdir не установлена. Когда я пытаюсь установить его, я получаю ошибку в заголовке.
25 июл '18 в 20:25
1
ответ
Почему Lean заставляет рекурсивные аргументы типа появляться после нерекурсивных?
Следующее определение отклонено Lean: inductive natlist | nil : natlist | cons: natlist → ℕ → natlist с сообщением об ошибке "arg #2 of natlist.cons не является рекурсивным, но это происходит после рекурсивных аргументов " И следующее определение пр…
21 янв '17 в 04:42
2
ответа
Начинающий не может импортировать в Lean
Я абсолютный новичок, а не программист, пытающийся научиться формальной проверке с помощью Logic и Proof. Я не могу импортировать что-либо в Lean. Я извлекаю файл tar для двоичного файла в /tmp тогда делай /tmp/lean-3.4.1-linux/bin/./lean /tmp/test.…
11 июн '18 в 20:40
0
ответов
Настройка зависимых типов функциональных пространств
Предположим, у нас есть следующее определение, которое представляет ограниченное целое число в интервале Clopen <a, b), def zbound (x₁ x₂ : ℤ) := { n : ℤ // x₁ ≤ n ∧ n < x₂ } Теперь я хочу функциональное пространство от zbound x₁ x₂ в bool упа…
17 янв '18 в 20:32
2
ответа
Как убрать скобки в алгебраических выражениях с помощью Lean
Я пытаюсь доказать одну алгебраическую теорему, используя Лин. Мой код import algebra.group import algebra.ring open algebra variable {A : Type} variables [s : ring A] (a b c : A) include s theorem clown (a b c d e : A) : (a + b + e) * ( c + d) = a …
24 окт '18 в 22:05
1
ответ
Почему и класс типов, и механизм неявных аргументов?
Таким образом, мы можем иметь явные аргументы, обозначенные (),Мы также можем иметь неявные аргументы, обозначаемые как {}, Все идет нормально. Однако зачем нам также [] обозначения для классов типов конкретно? В чем разница между следующими двумя: …
10 июл '17 в 14:00
1
ответ
Использовать получение в тактическом режиме в доказательстве теоремы Лин
Как мне использовать гипотезу формы H : exists x, P x в тактическом режиме? В режиме термина я бы использовал obtain x Hx, from H,
28 июн '16 в 12:42