Skip to content

Instantly share code, notes, and snippets.

View JasonGross's full-sized avatar

Jason Gross JasonGross

186 followers · 11 following
View GitHub Profile
@JasonGross
JasonGross / adjust-class-compat.py
Last active March 14, 2024 19:12
Replace `:>` with `::` in `Class` definitions for coq/coq#18590
#!/usr/bin/env python
import subprocess
import re
def get_git_grep_files(pattern):
"""Run git grep to find files matching a pattern."""
result = subprocess.run(['git', 'grep', '--name-only', pattern], capture_output=True, text=True)
if result.returncode != 0:
raise Exception("git grep command failed")
files = result.stdout.strip().split('\n')
@JasonGross
JasonGross / toy_coherent.v
Created December 8, 2023 23:25
toy model for identifying a coherent subset of equalities, cf https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-198200
Import EqNotations.
Inductive TY := BOOL | UNIT.
Definition tyInterp (t : TY) := match t with BOOL => bool | UNIT => unit end.
Inductive EQ : TY -> TY -> Type :=
| RFL {t} : EQ t t
| SYM {a b} : EQ a b -> EQ b a
| TRANS {a b c} : EQ a b -> EQ b c -> EQ a c
.
Fixpoint eqInterp {a b : TY} (p : EQ a b) : tyInterp a = tyInterp b
@JasonGross
JasonGross / W.v
Last active September 23, 2023 18:21
A formulation for W-types which supports the correct recursion principle on nat
(** Some imports *)
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.Fin.
Require Import Coq.Logic.FunctionalExtensionality. (* only used for qinv equalities, not recursor *)
Set Primitive Projections.
Set Universe Polymorphism.
(** In [W A B], [A] labels the constructors and their non-recursive
arguments, while [B] describes the recursive arguments for each
constructor. *)
Inductive W (A : Type) (B : A -> Type) := sup (wnr : A) (wr : B wnr -> W A B).
@JasonGross
JasonGross / fast_fin.v
Created May 23, 2019 02:42
Fast boolean equality proofs on finite types
Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.
Lemma negb_existsb_nth_error {A} (ls : list A) (f : A -> bool) (H : existsb f ls = false) n v (H' : nth_error ls n = Some v)
: f v = false.
Proof.
revert dependent n; induction ls, n; cbn in *; intros; try congruence.
all: repeat first [ progress subst
| rewrite orb_false_iff in *
@JasonGross
JasonGross / In_UIP_attempt.v
Last active March 26, 2021 20:50
An attempt at a version of List.In which has UIP
Require Import Coq.Logic.EqdepFacts Coq.Logic.Eqdep_dec.
Require Import Coq.Lists.List.
Fixpoint In {A} (adjust : forall x y : A, x <> y -> x <> y) (a : A) (xs : list A) : Prop
:= match xs with
| nil => False
| x :: xs
=> x = a \/ ((exists pf : x <> a, adjust _ _ pf = pf) /\ In adjust a xs)
end.
@JasonGross
JasonGross / RangeAsClass.lean
Created March 16, 2021 16:57 — forked from pnwamk/RangeAsClass.lean
A type class for generic Ranges
import Init.Meta
-- This isn't strictly necessary of course - reverse could be a member of `Range`.
class Reverse (α : Type u) where
reverse : α → α
open Reverse (reverse)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
@JasonGross
JasonGross / html-scrape-classes.html
Last active November 3, 2020 17:50
Scrapers for Splash classes for 2015, in a combination of python and javascript
<html>
<!--// run `python -m SimpleHTTPServer 8000`, and visit http://localhost:8000/html-scrape-classes.html-->
<!--// run `python3 -m http.server 8000`, and visit http://localhost:8000/html-scrape-classes.html-->
<head>
<script type="text/javascript">
// follow the instructions at https://developers.google.com/google-apps/calendar/quickstart/js, using this in place of the quickstart file
// the output of the following javascript, run in the chrome console on https://esp.mit.edu/teach/Splash/2015/teacherreg, below
/*
var forPython = false;
var splashYear;// = 2016;
@JasonGross
JasonGross / fun_pow_id_to_iso.v
Last active September 10, 2020 21:08
Require Import Coq.Arith.Arith.
Open Scope function_scope.
Fixpoint fun_pow {A} (f : A -> A) (n : nat) (x : A) : A
:= match n with
| O => x
| S n => f (fun_pow f n x)
end.
Infix "^" := fun_pow : function_scope.
@JasonGross
JasonGross / semigroup_assoc.v
Last active August 25, 2020 21:06
prove that all associations of elements in a semigroup are equal
Require Import Coq.micromega.Lia.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.
Local Open Scope list_scope.
Inductive tree : nat -> Set :=
| leaf : tree 1
| node {x y} : tree x -> tree y -> tree (x + y).
@JasonGross
JasonGross / big_eq_dec.v
Last active June 18, 2020 08:52
Require Import Coq.NArith.NArith.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Logic.Eqdep_dec.
Definition decidable (P: Prop) := {P} + {~P}.
Definition eq_dec T := forall (x y:T), decidable (x=y).
Inductive spec_type: Set :=
| abruption