Описание тега logical-foundations

Описание тега Вопросы с тегом
Вопросы, связанные с курсом логических основ Пенсильванского университета
0 ответов

Логические основания ошибок

Я прохожу курс "Основы логики" и сталкиваюсь со следующими ошибками: Строки не определены Lists.v, код: Definition manual_grade_for_rev_injective : option (nat*string) := None. Отклик: Ошибка: ссылочная строка не найдена в текущей среде. После того …
14 фев '19 в 12:03
2 ответа

Основы coq: функция bin_to_nat

Я прохожу курс "Основы логики" и застрял на последнем упражнении в Основах: Имея двоичное число, запишите преобразователь в его унарное представление: Inductive bin : Type := | Z | A (n : bin) | B (n : bin). Fixpoint bin_to_nat (m:bin) : nat := (* W…
19 янв '19 в 21:02
1 ответ

Меньше, чем функция

Я прохожу курс обучения "Логические основы". Решение проблемы: Имея меньшую или равную функцию: Fixpoint leb (n m : nat) : bool := match n with | O => true | S n' => match m with | O => false | S m' => leb n' m' end end. создать функцию …
31 дек '18 в 14:11
1 ответ

Индуктивные типы, несущие доказательства

В "Основах программного обеспечения" есть одно упражнение, которое я уже некоторое время пытаюсь решить правильно, но на самом деле я попал в тупик, пытаясь записать требуемую функцию. Вот соответствующая часть упражнения Рассмотрим другое, более эф…
14 дек '18 в 21:19
1 ответ

Правильно ли ассоциируются тактики Coq или левые?

Я прошел через основы программного обеспечения и получил пример: repeat (try (left; reflexivity); right). и был смущен, что это значит. Например, мы получаем: try [ (left; reflexivity); right ] или же [try (left; reflexivity);] right второй или перв…
12 дек '18 в 19:59
0 ответов

Требовать экспорт изменений требований в каждом файле

Я новичок в Coq, и в настоящее время прохожу серию уроков Software Foundations. Тем не менее, я продолжаю бороться с получением Require Export часть работает с первой попытки, каждый файл требует новой стратегии для работы. На этот раз, однако, я за…
07 фев '19 в 10:48
3 ответа

Церковные цифры

В модуле Поли есть 4 упражнения, связанные с церковными цифрами: Definition cnat := forall X : Type, (X -> X) -> X -> X. Насколько я понимаю, cnat - это функция, которая принимает функцию f(x), это аргумент x и возвращает значение этого арг…
16 фев '19 в 21:40
1 ответ

Основы программного обеспечения: проверка leb_complete и leb_correct

Я работал над Томом 1 Бенджамина Пирса и др., Основы программного обеспечения, и я застрял на нескольких проблемах в главе IndProp. К сожалению, я не знаю лучшего места, чтобы спросить: у кого-нибудь есть намеки? Theorem leb_complete : forall n m, l…
01 дек '17 в 22:01
3 ответа

IndProp: ev_plus_plus

(** **** Exercise: 3 stars, standard, optional (ev_plus_plus) This exercise just requires applying existing lemmas. No induction or even case analysis is needed, though some of the rewriting may be tedious. *) Theorem ev_plus_plus : forall n m p, ev…
25 май '19 в 20:16
1 ответ

Логика: excid_middle_irrefutable

Вот задание из книги: Доказательство соответствия Coq общей исключенной средней аксиоме требует сложных рассуждений, которые не могут быть выполнены в самой Coq. Однако следующая теорема подразумевает, что всегда безопасно принять аксиому разрешимос…
21 май '19 в 22:18
1 ответ

Как заставить coq упростить выражения внутри гипотезы импликации

Я пытаюсь доказать следующую лемму: Inductive even : nat → Prop := | ev_0 : even 0 | ev_SS (n : nat) (H : even n) : even (S (S n)). Lemma even_Sn_not_even_n : forall n, even (S n) <-> not (even n). Proof. intros n. split. + intros H. unfold no…
28 май '19 в 21:59
1 ответ

Тактика: застрял в eqb_trans

Пытаясь решить eqb_trans, я застрял: Theorem eqb_trans : forall n m p, n =? m = true -> m =? p = true -> n =? p = true. Очевидно, что мы должны использовать eqb_true для его решения: Theorem eqb_true : forall n m, n =? m = true -> n = m. --…
19 апр '19 в 14:30
1 ответ

Логика: упражнение In_app_iff

Пытаясь решить Exceize In_app_iff из главы "Логика", я пришел к этому чудовищу: (* Lemma used later *) Lemma list_nil_app : forall (A : Type) (l : list A), l ++ [] = l. Proof. intros A l. induction l as [| n l' IHl']. - simpl. reflexivity. - simpl. …
24 апр '19 в 21:08
1 ответ

Логика: In_example_2

Вот код из книги: Example In_example_2 : forall n, In n [2; 4] -> exists n', n = 2 * n'. Proof. (* WORKED IN CLASS *) simpl. intros n [H | [H | []]]. - exists 1. rewrite <- H. reflexivity. - exists 2. rewrite <- H. reflexivity. Qed. После s…
25 апр '19 в 08:58
1 ответ

Логика: All_In не может расширять вложенные поля

Я сталкиваюсь с довольно странной проблемой: coq не хочет перемещать переменную полностью в контекст. В старые времена это делалось: Example and_exercise : forall n m : nat, n + m = 0 -> n = 0 /\ m = 0. Proof. intros n m. Он генерирует: n, m : na…
25 апр '19 в 19:33
1 ответ

Логика: все определения и теорема All_In

Вот задача: Черпая вдохновение из [In], напишите рекурсивную функцию [All], утверждая, что некоторое свойство [P] содержит все элементы списка [l]. Чтобы убедиться, что ваше определение верно, докажите лемму [All_In] ниже. (Конечно, ваше определение…
26 апр '19 в 19:30
1 ответ

Логика: лексма auxilliry для tr_rev_correct

В главе "Логика" представлена ​​хвостовая рекурсивная версия функции обратного списка. Нам нужно доказать, что это работает правильно: Fixpoint rev_append {X} (l1 l2 : list X) : list X := match l1 with | [] => l2 | x :: l1' => rev_append l1' (…
05 май '19 в 12:27
1 ответ

Логика: evenb_double_conv

Theorem evenb_double_conv : forall n, exists k, n = if evenb n then double k else S (double k). Proof. (* Hint: Use the [evenb_S] lemma from [Induction.v]. *) intros n. induction n as [|n' IHn']. - simpl. exists O. simpl. reflexivity. - rewrite -&gt…
05 май '19 в 15:56
1 ответ

Тактика: filter_exercise

(** **** Exercise: 3 stars, advanced (filter_exercise) This one is a bit challenging. Pay attention to the form of your induction hypothesis. *) Theorem filter_exercise : forall (X : Type) (test : X -> bool) (x : X) (l lf : list X), filter test l…
19 апр '19 в 16:53
1 ответ

even_Sn_not_even_n - применить одну гипотезу в другой

К сожалению, я снова застрял: Inductive even : nat > Prop := | ev_0 : even 0 | ev_SS (n : nat) (H : even n) : even (S (S n)). Lemma even_Sn_not_even_n : forall n, even (S n) <-> not (even n). Proof. intros n. split. + intros H. unfold not. …
29 май '19 в 06:05