{{ message }}

Instantly share code, notes, and snippets.

🐓
Hacking Coq

# Anton Trunov anton-trunov

🐓
Hacking Coq
Last active May 4, 2022
See relevant PG issue -- https://github.com/ProofGeneral/PG/issues/210
View coq-opam-switch.el
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 ;; 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)))))
Created May 18, 2017
Coq translation of a solution to the Valley Problem
View P1_valley.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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).
Created Sep 3, 2019
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:

Created Apr 29, 2018
View FinToNatDoesNotReduce.idr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Created Mar 28, 2018
View tuple_rev_involutive.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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.
Created Mar 20, 2018
Self-contained code for an SSReflect view issue
View cancel.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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).
Created Sep 19, 2017
View forw_rev_list_ind.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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)
Created Jun 18, 2017
View make_diff.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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) }.
Last active Jun 4, 2017
A solution to https://coq-math-problems.github.io/Problem4/
View P4_injections_surjections_on_finite_sets.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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.
Last active May 26, 2017
Solution to "Finite Cancellative Semigroups" problem
View P3_finite_cancellative_semigroups.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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.