Lysxia

#![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])]

Lysxia

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.

Lysxia

{-# LANGUAGE
  RankNTypes,
  TypeOperators #-}

-- | User-defined handlers.

module Bluefin.Handlers
  ( Sig
  , Handler
  , with

Lysxia

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

#!/usr/bin/env cabal
{- cabal:
build-depends: base, effectful-core
-}

-- Usage: cabal run Coroutine.hs

{-# LANGUAGE
  DataKinds,
  FlexibleContexts,

Lysxia

-- Traversables as Graded functors
-- Graded functors as functors that commute with grading
--
-- Graded endofunctors on KleisliApp are Traversables
--
-- Laws omitted.

module T where

open import Level

Lysxia

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

-- Minimax and alpha-beta pruning
--
-- Minimax can trivially be generalized to work on any lattice (@gminimax@).
-- Then alpha-beta is actually an instance of minimax.
--
-- Contents:
-- 0. Basic definitions: players and games
-- 1. Direct implementations of minimax and alpha-beta
-- 2. Generalized minimax and instantiation to alpha-beta
-- 3. QuickCheck tests

Lysxia

{-# 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

{-# OPTIONS --without-K #-}
module C where

open import Function
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; trans; cong; sym)
open import Data.Empty
open import Data.Bool
open import Data.Product as Prod using (∃-syntax; Σ-syntax; _,_; _×_; ∃; proj₁; proj₂)
open import Data.Maybe as Maybe using (Maybe; just; nothing; is-just)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)