JasonGross

#!/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

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

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

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

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

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

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

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

JasonGross

Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Numbers.Cyclic.Int63.Int63.
Require Import Coq.Numbers.Cyclic.Int63.Ring63.
Require Import Coq.Init.Wf Wf_nat.

Local Open Scope Z_scope.
Local Open Scope int63_scope.
Local Coercion is_true : bool >-> Sortclass.

JasonGross

import tactic.norm_num
import algebra.group_power
open prod
universes u v w ℓ

inductive let_bound (α : Type*)
| base : α → let_bound
| dlet : ℤ → (ℤ → let_bound) → let_bound
| mlet {β : Type} : β → (β → let_bound) → let_bound
open let_bound