Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Lysxia / lib.rs
Created May 8, 2024 20:04
Creusot experiments
#![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]
use ::std::vec;
extern crate creusot_contracts;
use creusot_contracts::*;
#[requires(t@.len() == n@)]
#[ensures(result ==> exists<i0: Int> exists<j0: Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
#[ensures(!result ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < n@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]
From Coq Require Import List.
Fixpoint map_In {A B : Type} (xs : list A) : (forall x, In x xs -> B) -> list B :=
match xs return (forall x, In x xs -> B) -> list B with
| nil => fun _ => nil
| cons x xs' => fun f => cons (f x (or_introl eq_refl)) (map_In xs' (fun x' In_x'_xs' => f x' (or_intror In_x'_xs')))
end.
{-# LANGUAGE
RankNTypes,
TypeOperators #-}
-- | User-defined handlers.
module Bluefin.Handlers
( Sig
, Handler
, with
(* formalization attached to my answer to https://cstheory.stackexchange.com/questions/53855/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-a *)
From Coq Require Import Lia.
Definition U : Type := forall A : Type, ((A -> A) -> A) -> A.
(* Try enumerating solutions by hand. After the initial [intros],
we can either complete the term with [exact xi],
or continue deeper with [apply f; intros xi]. *)
Goal U.
Proof.
@Lysxia
Lysxia / Coroutine.hs
Created March 29, 2024 16:56
Coroutines using effectful
#!/usr/bin/env cabal
{- cabal:
build-depends: base, effectful-core
-}
-- Usage: cabal run Coroutine.hs
{-# LANGUAGE
DataKinds,
FlexibleContexts,
(* https://proofassistants.stackexchange.com/questions/3841/assistance-using-destruct-on-an-equality-proof-for-functors/3843 *)
(* Proof of associativity of functor composition without UIP *)
(* 1. Intuition: treat equality as a proper algebraic structure:
think of it as a category (aka. the discrete category), not an equivalence relation. *)
(* 1a. An equality between morphisms, f = g, becomes the existence of a morphism between f and g. *)
(* 1b. In the definition of a category, homsets are thus categories.
The resulting structure is known as a 2-category. https://ncatlab.org/nlab/show/2-category
You can kepp applying the same generalization to the morphism category, resulting
@Lysxia
Lysxia / inits.hs
Created March 13, 2024 21:33
Benchmarking three versions of inits
{-# LANGUAGE BangPatterns #-}
import Criterion
import Criterion.Main
import Data.List (inits, scanl')
import Data.Primitive.Array
import GHC.Exts (RealWorld)
import System.IO.Unsafe
-- base implementation, using queues
@Lysxia
Lysxia / STO.v
Created December 14, 2023 10:43
(* A trick to print the simplified type of something *)
Definition type_of {A : Type} (a : A) : Type := A.
Arguments type_of _ /.
Notation simpl_type_of a := ltac:(let A := eval simpl in (type_of a) in exact A).
(* Example *)
Parameter p : forall x, 3 + x = x.
{- counter.hs: count comments and lines of code in .lagda.md files.
Usage:
cat src/*.lagda.md|runghc counter.hs
Counting method:
Triple backticks either start or end a code block.
Triple backtick lines are not counted.
Code lines starting with `--` are counted as comments
@Lysxia
Lysxia / T.agda
Last active August 22, 2023 22:09
-- Q: How to fix the last two commented lines?
--
-- Summary: Two intrinsically typed calculi A and B, and a translation from A to B.
-- The translation consists of a translation on types, followed by a translation on terms
-- indexed by the translation on types.
-- Agda won't let me case-split in the translation of (term) variables.
--
-- Signs of trouble:
-- - green slime in _A.∋_ and _B.∋_
-- - with clauses (rather than only pattern-matching on arguments)