{{ message }}

Instantly share code, notes, and snippets.

# roconnor

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.
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.
Last active Feb 21, 2016
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
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.