Skip to content

Instantly share code, notes, and snippets.

roconnor

Block or report user

Report or block roconnor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@roconnor
roconnor / MemoBinTree.v
Last active May 14, 2018
Memo Trie for funcitons over binary trees in Coq (no support for memoizing structually recursive functions though)
View MemoBinTree.v
(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *)
Require Import Vectors.Vector.
Import VectorNotations.
Set Primitive Projections.
Set Implicit Arguments.
Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.
@roconnor
roconnor / MemoOrdBinTree.v
Created May 14, 2018
Memoization for structurally recursive funcitons over binary trees in Coq (with poor performance).
View MemoOrdBinTree.v
Require Import Arith.
Require Import Omega.
Set Primitive Projections.
Set Implicit Arguments.
Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.
View ExtendedIncompletenessInQ0
// Define Computably Enumerable (aka recursively enumerable) predicates.
CESet : (Nat -> o) -> o
CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m)
// Standard Model
interpT : (Nat -> Nat) -> Term -> Nat
interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m)
interpF : (Nat -> Nat) -> Formula -> o
@roconnor
roconnor / PatriciaTrie.v
Created Mar 5, 2012
Implementation of Patrica Tries in Coq
View PatriciaTrie.v
Require Import Bvector.
Require Import Eqdep_dec.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition bCompare (x y : bool) : comparison :=
match x, y with
| false, false => Eq
You can’t perform that action at this time.