Anton Trunov anton-trunov

I hereby claim:

To claim this, I am signing this object:

	;; The following works with OPAM 2.0.x
	;; Put this piece of code into your .emacs and use it interactively as
	;; M-x coq-change-compiler
	;; If you change your OPAM installation by e.g. adding more switches, then
	;; run M-x coq-update-opam-switches and coq-change-compiler will show the updated set of switches.

	(defun opam-ask-var (switch package var)
	(ignore-errors (car (process-lines
	"opam" "var" "--safe" "--switch" switch (concat package ":" var)))))

	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.

	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).

	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)

	(* 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) }.

	(* 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.

	(* 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.

	(* 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.

	(* 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.