anton-trunov

(* This is a Coq translation of this solution: https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/mathprobs/p01.agda *)
(* to this https://coq-math-problems.github.io/Problem1/ *)
 
Require Import Coq.Arith.Arith.

Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.

Definition n_valley n (f : nat -> nat) i := forall i', i' < n -> f (S (i' + i)) = f (i' + i).

Lemma is_n_valley {f} n : decr f -> forall i, n_valley n f i \/ (exists i', f i' < f i).

anton-trunov

-- http://stackoverflow.com/questions/44079181/idris-vect-fromlist-usage-with-generated-list

total
takeExact : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
takeExact Z xs = Just []
takeExact (S n) [] = Nothing
takeExact (S n) (x :: xs) with (takeExact n xs)
  takeExact (S n) (x :: xs) | Nothing = Nothing
  takeExact (S n) (x :: xs) | (Just v) = Just (x :: v)

anton-trunov

(* https://coq-math-problems.github.io/Problem2/ *)

Require Import Coq.Arith.Arith.
Require Import Coq.Classes.Morphisms.

Definition LPO := forall f : nat -> bool, (exists x, f x = true) \/ (forall x, f x = false).

Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.

Definition infvalley (f : nat -> nat) (x : nat) := forall y, x <= y -> f y = f x.

anton-trunov

(* https://stackoverflow.com/questions/44059569/coq-goal-variable-not-transformed-by-induction-when-appearing-on-left-side-of-a/ *)

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Disjoint {X : Type}: list X -> list X -> Prop :=
  | disjoint_nil: Disjoint [] []
  | disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2
  | disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2).
Hint Constructors Disjoint.

anton-trunov

(* https://coq-math-problems.github.io/Problem3/ *)

Definition inj{X Y}(f : X -> Y) := forall x x', f x = f x' -> x = x'.

Definition surj{X Y}(f : X -> Y) := forall y, {x : X | f x = y}.

Definition ded_fin(X : Set) := forall f : X -> X, inj f -> surj f.

Section df_inh_cancel_sgroups.

anton-trunov

(* https://coq-math-problems.github.io/Problem4/ *)

Definition inj {X Y} (f : X -> Y) := forall x x', f x = f x' -> x = x'.

Definition surj {X Y} (f : X -> Y) := forall y, {x : X | f x = y}.

Definition left_inv {X Y} (g : Y -> X) (f : X -> Y) := forall x, g (f x) = x.

Definition right_inv {X Y} (g : Y -> X) (f : X -> Y) := left_inv f g.

anton-trunov

(* https://stackoverflow.com/questions/44612214/how-to-deal-with-really-large-terms-generated-by-program-fixpoint-in-coq *)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Relations.Relations.
Require Import Coq.Program.Program.

Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}.
Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.

anton-trunov

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.

Lemma forw_rev_list_ind {A}
        (P : list A -> Prop)
        (Pnil : P [])
        (Psingle : (forall a, P [a]))
        (Pmore : (forall a b, forall xs, P xs -> P ([a] ++ xs ++ [b])))
        (xs : list A)

anton-trunov

From Coq Require Import ssreflect ssrfun ssrbool List.
Import ListNotations.
Set Implicit Arguments.
Unset Strict Implicit.

Section Heap.
Definition heap := nat.
Definition valid (h : heap) : bool := true.
Definition empty : heap := 0.
Definition join (h1 h2 : heap) := nosimpl (h1 + h2).

anton-trunov

From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype seq tuple.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition trev T n (t : n.-tuple T) := [tuple of rev t].

Lemma trevK T n : involutive (@trev T n).
Proof. by move=>t; apply: val_inj; rewrite /= revK. Qed.