Skip to content

Instantly share code, notes, and snippets.

Avatar
🐓
Hacking Coq

Anton Trunov anton-trunov

🐓
Hacking Coq
View GitHub Profile
View coq-opam-switch.el
;; 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)))))
@anton-trunov
anton-trunov / P1_valley.v
Created May 18, 2017
Coq translation of a solution to the Valley Problem
View P1_valley.v
(* 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).
View keybase.md

Keybase proof

I hereby claim:

  • I am anton-trunov on github.
  • I am anton_trunov (https://keybase.io/anton_trunov) on keybase.
  • I have a public key ASDag_9uwDW3dyJML1JZk9sHb9xVtJSbiMNOGC6SYVD2igo

To claim this, I am signing this object:

View FinToNatDoesNotReduce.idr
import Data.Vect
-- let us pretend we have written this function
postulate vectorsInits : Vect n t -> Vect n (p : Fin k ** Vect (finToNat p) t)
total
contra : Void
contra with (vectorsInits {k = 0} [42])
contra | [(x ** _)] = absurd x
View tuple_rev_involutive.v
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.
@anton-trunov
anton-trunov / cancel.v
Created Mar 20, 2018
Self-contained code for an SSReflect view issue
View cancel.v
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).
View forw_rev_list_ind.v
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)
View make_diff.v
(* 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) }.
View P4_injections_surjections_on_finite_sets.v
(* 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
anton-trunov / P3_finite_cancellative_semigroups.v
Last active May 26, 2017
Solution to "Finite Cancellative Semigroups" problem
View P3_finite_cancellative_semigroups.v
(* 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.