Skip to content

Instantly share code, notes, and snippets.

View Janno's full-sized avatar

Jan-Oliver Kaiser Janno

16 followers · 5 following
  • bluerock.io, Max Planck Institute for Software Systems (MPI-SWS)
  • Saarbrücken, Germany
View GitHub Profile
@Janno
Janno / fast.v
Created March 14, 2024 16:20
fast.v fails immediately, slow.v takes forever
Module Test1.
Axiom Timeless : forall {X:Type} (x:X), Prop.
Axiom biIndex : Type.
Axiom gFunctors : Type.
Axiom genv : Type.
Axiom State : Set.
Axiom code : Set.
Axiom roundup_gname : Set.
Axiom ptr : Set.
@Janno
Janno / vis.html
Last active March 2, 2024 01:15
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<style>
* {
--totalwidth: 1024px;
font-family: sans-serif;
font-weight: 300;
@Janno
Janno / slow.lean
Created March 22, 2023 17:59
A slow unification call in an unknown version of Lean
class op {T : Type} := (op_op : T -> T -> T)
instance nat_op : @op nat := op.mk (nat.add)
def tc_op {T:Type} [o : @op T] : T -> T -> T := @op.op_op T o
infixl `#`:50 := tc_op
def mk_evar (n : nat) := n
section test
@Janno
Janno / names.v
Last active June 24, 2021 13:36
name stuff
From Ltac2 Require Import Init Control Constr Std Ltac2.
From Ltac2 Require Int Option List Array Ident Char String.
Import Constr.Unsafe.
Set Default Proof Mode "Classic".
From Coq Require Import String.
Ltac2 rec generate_constructors_rev ind k :=
if Int.lt k 0 then
@Janno
Janno / myfile.v
Last active August 17, 2020 13:49
Module Test.
Polymorphic Section With.
Monomorphic Parameter MyGoal : Prop.
Polymorphic Parameter MyAssum1@{U1}: forall T1:Type@{U1}, Prop.
Polymorphic Parameter MyAssum2@{U2}: forall T2:Type@{U2}, Prop.
Polymorphic Parameter MyProof@{U1 U2+|U1 < U2+} : forall (T1 : Type) (T2 : Type), MyAssum1@{U1} T1 -> MyAssum2@{U2} T2 -> MyGoal.
Set Printing Depth 1000.
Polymorphic Definition my_tactic@{U1 U2 U1' U2'+} : tactic :=
Eval cbv beta fix match
@Janno
Janno / elpi-reification-port.v
Last active July 7, 2020 15:30
Mtac2 Port of a reification/reflection example from elpi.
(*
Installing Mtac2 for 8.11:
opam repo add mtac2-dev git+https://github.com/Mtac2/opam.git
opam update mtac2-dev
opam install coq-mtac2.dev.8.11
*)
@Janno
Janno / discrinimationtrees.v
Created June 17, 2020 15:27
From Coq Require Import Lia.
Axiom P : nat -> Prop.
Module wasteful_search.
Class Simplify (n : nat) :=
{ simplified_to : nat; simplified_ok : P n -> P simplified_to }.
@Janno
Janno / context_pattern.v
Created May 21, 2020 14:49
From Mtac2 Require Import Specif Mtac2 MTele MFix MTeleMatch.
Close Scope tactic_scope. (* Really need to fix this! *)
From Unicoq Require Import Unicoq.
Definition make_pattern_tele :=
mfix go (T : Type) : forall f: T, M MTele :=
mtmmatch T as T return forall f: T, M _ with
| [? X P] forall x : X, P x =u>
fun f =>
\nu_f for f as x,
@Janno
Janno / slow_cumul.v
Last active March 3, 2020 14:26
Slow Cumulativity Checking
Require Coq.Strings.String.
Require Coq.Lists.List.
Set Implicit Arguments.
Set Universe Polymorphism.
Inductive nelist {A : Type} : Type :=
| ne_sing : A -> nelist
| ne_cons : A -> nelist -> nelist.
@Janno
Janno / bidir.v
Created February 13, 2020 19:58
extreme slowdowns due to bidirectionality.
(* -*- mode: coq; coq-prog-args: ("-emacs" "-I" "src" "-R" "theories" "Mtac2" "-top" "DepDestruct") -*- *)
(* File reduced by coq-bug-finder from original input, then from 550 lines to 340 lines, then from 1172 lines to 339 lines, then from 960 lines to 344 lines, then from 501 lines to 402 lines, then from 631 lines to 468 lines, then from 595 lines to 528 lines, then from 612 lines to 559 lines, then from 657 lines to 571 lines, then from 1675 lines to 571 lines, then from 634 lines to 571 lines, then from 641 lines to 571 lines, then from 640 lines to 571 lines, then from 642 lines to 571 lines, then from 660 lines to 571 lines, then from 637 lines to 571 lines, then from 871 lines to 571 lines, then from 699 lines to 571 lines, then from 630 lines to 571 lines, then from 626 lines to 571 lines, then from 851 lines to 571 lines, then from 936 lines to 594 lines, then from 749 lines to 594 lines, then from 674 lines to 594 lines, then from 869 lines to 610 lines, then from 926 lines to 609 lines, then from