Skip to content

Instantly share code, notes, and snippets.

Avatar

Ryan Scott RyanGlScott

View GitHub Profile
View SimplifiedExample.v
From Coq Require Import Program.Basics.
From Coq Require Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.
Import VectorNotations.
Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.
View ZifyTermTakeOne.v
From Coq Require Import Program.Basics.
From Coq Require Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.
Import VectorNotations.
Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.
@RyanGlScott
RyanGlScott / HDList.hs
Created Jul 23, 2022
Heterogeneous difference lists
View HDList.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module HDList where
import qualified Control.Category as Cat (Category(..))
import Data.Function (on)
@RyanGlScott
RyanGlScott / DList.v
Last active Jul 24, 2022
Proofs of the difference list invariant for various operations
View DList.v
Require Import Lists.List.
Import ListNotations.
Open Scope list_scope.
Require Import Logic.FunctionalExtensionality.
Require Import Lists.Streams.
Inductive DList (a : Type) : Type :=
| MkDList : (list a -> list a) -> DList a.
Arguments MkDList {a} f.
@RyanGlScott
RyanGlScott / FromToVec.hs
Created Aug 28, 2021
Proofs involving conversion from and to length-indexed vectors
View FromToVec.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module FromToVec where
@RyanGlScott
RyanGlScott / Main.hs
Last active May 19, 2021
Is this use of unsafeCoerce valid?
View Main.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where
@RyanGlScott
RyanGlScott / TakesForeverToCompile.hs
Created Jul 21, 2019
Try compiling with -O1 if you have a lot of time on your hands
View TakesForeverToCompile.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
View ThePowerOfDefun.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- Requires GHC 8.10 or later
module ThePowerOfDefun where
@RyanGlScott
RyanGlScott / SingletonsVTA.hs
Created May 31, 2019
A sketch of how we might single visible type applications
View SingletonsVTA.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
@RyanGlScott
RyanGlScott / QuickSort.v
Last active May 28, 2019
Correctness proof for QuickSort in Coq
View QuickSort.v
(* Largely inspired by https://github.com/coq/coq/wiki/QuickSort *)
Require Import Arith.Wf_nat Bool List Nat Omega.
Require Import Sorting.Permutation Sorting.Sorted.
Definition flip_ltb (x : nat) : nat -> bool :=
fun (y : nat) => y <? x.
Definition flip_geb (x : nat) : nat -> bool :=
fun (y : nat) => x <=? y.