coq

1зной

1ответ

математические классы: Докажите, что MUNIT является его собственным отрицанием

Я только начал играть с библиотекой математики-классов, и я бы хотел, чтобы доказать следующую лемму: Require Import MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace Mat

4зной

2ответ

Есть ли способ автоматизировать доказательство Coq с помощью шагов перезаписи?

Я работаю на доказательства, и один из моих подзадач выглядит как это: Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p), negb a = negb b. Proof. intros.

1зной

2ответ

Как бороться с функцией с существующим с правой стороны?

Я не уверен ли я, используя правильные слова в названии вопроса, так вот код: Lemma In_map_iff : forall (A B : Type) (f : A -> B) (l : list A) (y : B), In y (map f l) <-> exists x, f x

0зной

1ответ

Как применить переписывание в правой части условного выражения без разделения на него?

Lemma in_app_iff : forall A l l' (a:A), In a (l++l') <-> In a l \/ In a l'. Proof. intros. split. - induction l. + simpl. induction l'. * simpl. intros. inversion

0зной

2ответ

Как доказать единственность функции в Coq при задании спецификации?

Учитывая спецификацию функции, например, specification_of_sum, как доказать в Coq, что существует только одна такая функция? Я изучаю математику, и я могу доказать это в руке, но мои навыки в Coq огра