Skip to content

Instantly share code, notes, and snippets.

Vadim Zaliva vzaliva

View GitHub Profile
View Type_Fix.v
Require Import Setoid Morphisms Relations.
Record S {i o: nat} : Type.
Definition C {i o: nat} (f: @S i o): @S i o. Admitted.
Definition B {o:nat} (z:nat): @S (o+o) o. Admitted.
Definition X {i o:nat} (z:nat): @S i o. Admitted.
Parameter R: forall {i o}, relation (@S i o).
Instance R_proper {i o}: Proper (R ==> R ==> iff) (@R i o). Admitted.
Definition Rext {i o} := pointwise_relation nat (@R i o).
Lemma Rewrite (x:nat): forall z, R (C (@B x z)) (B z). Admitted.
@vzaliva
vzaliva / VecPermutation.v
Created Oct 20, 2017
Vector Permutations on Coq. First attempt
View VecPermutation.v
Require Import Coq.Arith.Arith.
Require Export Coq.Vectors.Vector.
Require Import Coq.Program.Equality. (* for dependent induction *)
Require Import Setoid Morphisms.
(* CoLoR: `opam install coq-color` *)
Require Export CoLoR.Util.Vector.VecUtil.
Open Scope vector_scope.
View a.v
Require Import MathClasses.interfaces.canonical_names.
Require Import MathClasses.implementations.peano_naturals.
Require Import CoLoR.Util.Vector.VecUtil.
Section Ex.
Variable (CarrierA : Type).
Parameter CarrierAe: Equiv CarrierA.
Parameter A : forall (T : Type), T -> T.
Lemma Foo {x}: (A _ x) = x. Admitted.
View rewrite_test.v
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Data.Monads.WriterMonad.
Require Import ExtLib.Data.Monads.IdentityMonad.
Require Import ExtLib.Data.PPair.
Require Export Coq.Setoids.Setoid.
Require Import Coq.Vectors.Vector.
Set Implicit Arguments.
@vzaliva
vzaliva / Vbuild_proper.v
Created Jul 29, 2017
Vbuild_proper experiments
View Vbuild_proper.v
Require Import MathClasses.interfaces.canonical_names.
Require Import MathClasses.implementations.peano_naturals.
Require Import CoLoR.Util.Vector.VecUtil.
Section Ex.
Parameter A : nat -> nat.
Lemma Foo {x}: (A x) = x. Admitted.
@vzaliva
vzaliva / remove-old-kernels.sh
Created Apr 1, 2017
Script to free space on /boot partition by removing old kernels
View remove-old-kernels.sh
#!/bin/bash
kernelver=$(uname -r | sed -r 's/-[a-z]+//')
unused=`dpkg -l linux-{image,headers}-"[0-9]*" | awk '/ii/{print $2}' | grep -ve $kernelver`
echo "Your current kernel is version is $kernelver"
if [ -z "$unused" ]; then
echo "No old kernels to remove."
exit 0
fi
@vzaliva
vzaliva / WriterComonad.v
Last active Mar 9, 2017
Writer Comonad in Coq
View WriterComonad.v
Require Import Coq.Program.Basics.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Data.Monads.IdentityMonad.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Data.Monads.WriterMonad.
Require Import ExtLib.Data.PPair.
Require Import ExtLib.Structures.CoMonad.
Require Import ExtLib.Core.Type.
@vzaliva
vzaliva / set_lang.py
Last active Jun 7, 2017
Script to toggle between the two last used language in Gnome
View set_lang.py
#!/usr/bin/env python3
#
# Script to toggle between the two last used language in Gnome
#
# History:
#
# Original script by Jacob Vlijm
# Saving last language and togging: Vadim Zaliva
#
# See also: http://askubuntu.com/questions/871678/how-can-i-quickly-switch-between-two-out-of-multiple-languages
@vzaliva
vzaliva / ThinkLight
Created May 22, 2016
This script controll keyboard backlight on IBM ThinkPad X-series
View ThinkLight
#!/bin/bash
# Vadim Zaliva lord@crocodile.org
# based on https://gist.github.com/hadess/6847281
if [[ $EUID -ne 0 ]]; then
echo "This script must be run as root" 1>&2
exit 1
fi
You can’t perform that action at this time.