Skip to content

Instantly share code, notes, and snippets.

View gmalecha's full-sized avatar

Gregory Malecha gmalecha

65 followers · 12 following
View GitHub Profile
@gmalecha
gmalecha / gist:899d0594a67b2d35da73
Created March 4, 2014 00:05
"Compilation" of univalence in Coq.
Require Import MirrorCore.Iso.
Set Implicit Arguments.
Set Strict Implicit.
Definition Pi (T : Type) (F : T -> Type) : Type :=
forall x : T, F x.
(** What is the generalization of [Functor] to a dependent function? **)
Class DFunctor (Q : Type -> Type) (F : Pi Q)
@gmalecha
gmalecha / even_refl.v
Created October 5, 2015 06:28
Simple computational reflection example.
Set Implicit Arguments.
Set Strict Implicit.
Inductive Even : nat -> Prop :=
| Even_O : Even 0
| Even_SS : forall n, Even n -> Even (S (S n)).
Goal Even 0.
apply Even_O.
Qed.
@gmalecha
gmalecha / ApproxNat.v
Created January 15, 2016 06:59
Approximating inductive types
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Fail Inductive X : Type := BAD : (X -> X) -> X.
Definition natF (T : Type) : Type :=
T + unit.
(* We define approximation using a fixpoint which computes a Type
* by repeatedly applying a function. The base case is the empty set.
@gmalecha
gmalecha / MtacCancel.v
Last active April 18, 2016 22:29
Trying out Mtac
(** An axiomatization of commutative monoids
**)
Parameter m : Type.
Parameter star : m -> m -> m.
Local Infix "*" := star.
Parameter one : m.
Axiom star_comm : forall a b : m, a * b = b * a.
Axiom star_assoc : forall a b c : m, (a * b) * c = a * (b * c).
Axiom one_star : forall a : m, one * a = a.
@gmalecha
gmalecha / QedHarmful.v
Created February 18, 2017 22:24
Code listing for gmalecha.github.io/reflections/2017/2017-02-18-Qed-Considered-Harmful/Qed-Considered-Harmful
Require Import Coq.Lists.List.
Set Implicit Arguments.
Set Strict Implicit.
Section hlist.
Context {T : Type}.
Variable F : T -> Type.
Inductive hlist : list T -> Type :=
| Hnil : hlist nil
@gmalecha
gmalecha / member_heq_eq.v
Last active February 22, 2017 07:00
Shell of the proof of member_heq_eq.
Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.
Set Implicit Arguments.
Set Strict Implicit.
Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.
@gmalecha
gmalecha / member_heq_eq.v
Last active February 22, 2017 07:04
Solution to member_heq_eq
Require Import Coq.Lists.List.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Member.
Set Implicit Arguments.
Set Strict Implicit.
Arguments MZ {_ _ _}.
Arguments MN {_ _ _ _} _.
@gmalecha
gmalecha / ComputationalReflection.v
Created June 10, 2017 17:45
Talk from SF Types, Theorems, and Programming Languages Meetup
Require Import Coq.Lists.List.
Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.
(**
** Speeding up Proofs with Computational Reflection
** Gregory Malecha
** gmalecha.github.io
**
**)
@gmalecha
gmalecha / ShapeIndexed.hs
Last active April 19, 2019 16:23
https://gmalecha.github.io/reflections/2017/pattern-matching-on-data-kinds
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
module ShapeIndexed where
import Data.Constraint
@gmalecha
gmalecha / TypedAndUntyped.hs
Last active February 15, 2020 20:33
A single representation for both strongly and weakly typed terms
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}