Coq-задачи (поинтереснее)

1. Закон Пирса.

   Require Import Classical.
   Theorem Peirce: forall a b: Prop, ((a -> b) -> a) -> a.
   

2. Ослабленный закон Пирса.

   Theorem Weak_Peirce: forall a b : Prop, ((((a -> b) -> a) -> a) -> b) -> b.
   

3. Теорема Кантора.

   Require Import Classical.
   Theorem Cantor: forall A : Set, ~ exists f: (A -> Prop) -> A,
   forall P Q : (A -> Prop), (f P = f Q -> P = Q).
   

4. Двойное отрицание закона Пирса (выводимо в интуиционистском исчислении высказываний в силу теоремы Гливенко).

   Theorem DN_Peirce: forall a b: Prop, ~~(((a -> b) -> a) -> a).
   

5. Двойное отрицание закона исключённого третьего (выводимо в интуиционистском исчислении высказываний в силу теоремы Гливенко).

   Theorem DN_TND : forall a b : Prop, ~~(a \/ ~a).
   

6. Сумма первых n кубов равна квадрату суммы первых n чисел

   Require Import Arith.
   
   Fixpoint sum (n : nat) (f : nat -> nat)  := 
   match n with 
   | O => 0
   | S x => sum x f + f x
   end.
   
   Definition square (x : nat) := x*x.
   Definition cube (x : nat) := x*x*x.
   
   
   Theorem cubesum : forall n : nat, sum n cube = square (sum n (fun n => n)).
   

7. Сформулируйте и докажите в Coq, что число, составленное из 3ⁿ одинаковых цифр (в десятичной системе), делится на 3ⁿ.