Skip to content

Instantly share code, notes, and snippets.

View mmalvarez's full-sized avatar

Mario Alvarez mmalvarez

29 followers · 3 following
View GitHub Profile
@mmalvarez
mmalvarez / mutual.v
Created May 28, 2020 21:42
Require Import Nat Bool.
Inductive aexp : Set :=
APlus : aexp -> aexp -> aexp
| AConst : nat -> aexp
| ACase : bexp -> aexp -> aexp -> aexp
with bexp : Set :=
BAnd : bexp -> bexp -> bexp
| BConst : bool -> bexp
| BLt : aexp -> aexp -> bexp.
@mmalvarez
mmalvarez / dictionary_clean.ml
Created March 10, 2016 22:34
Material from Final Exam Review Session, 3/10/2016
(* Winter 2012, Problem 1
Dictionary *)
(* a. *)
let rec find d k =
match d with
| [] -> raise Not_found
| (k',v') :: t -> (* TODO *)
let rec add d k v =
@mmalvarez
mmalvarez / Week4.ml
Last active January 26, 2016 04:53
CSE 130 W2016 - Code from 1/25 Discussion Section (Folding)
(* Section - Jan 25, 2016 *)
type 'a map = (int * 'a) list;;
(* associative maps *)
let get k m =
List.fold_left
(fun acc (k',v') ->
if k = k' then acc@[v'] else acc)
[]
m;;
@mmalvarez
mmalvarez / Week2.ml
Last active January 12, 2016 14:22
CSE 130 W2016 - Code from 1/11 Discussion Section (Lists)
(* Problem 1 - Collatz Conjecture
It is conjectured (but not proven) that if you take any number, and
iterate the following process, eventually the result converges to 1.
The process:
- if the number is odd, multiply by 3 and add 1
- if the number is even, divide it by 2
Let's make functions to find collatz sequences for numbers
*)
@mmalvarez
mmalvarez / FloatEmbed.v
Created November 28, 2015 09:12
(* Specialization of the Embedding framework to our floating-point language *)
Require Import Source.
Require Import Embed.
Require Import TLA.Syntax.
Require Import TLA.Semantics.
Require Import Coq.Reals.Rbase.
Require Import Coq.Strings.String.
Require Import micromega.Psatz.
Require Import ExtLib.Tactics.
Require Import ExtLib.Data.Option.
@mmalvarez
mmalvarez / Embed.v
Created November 28, 2015 09:10
Require Import TLA.Syntax.
Require Import TLA.Semantics.
Require Import TLA.ProofRules.
Require Import String.
Local Open Scope HP_scope.
Local Open Scope string_scope.
Require Import List.
Require Import Strings.String.
Import ListNotations.
Require Import Rdefinitions.
@mmalvarez
mmalvarez / arithable.v
Created August 5, 2015 20:38
Coq typeclasses describing types capable of arithmetic operations
Require Import Charge.Logics.ILInsts.
(* need "arithable" typeclass with addition, subtraction, multipliction, division
make Terms arithable, as well as real numbers and stuff
*)
Class Arithable (T : Type) : Type :=
{ a_plus : T -> T -> T;
a_minus : T -> T -> T;
a_mult : T -> T -> T
}.
@mmalvarez
mmalvarez / transparify.rb
Created July 24, 2015 00:22
Turn QED's in a Coq development into Defined's. Useful for when you need to compute on proofs but they've been QED'd.
# script to transform all theorems in all Coq files
# in the given directory's tree
# such that Qed's become Defined's.
loc = ARGV.first
ldir = Dir.open loc
$vfiles = []
# where is the directory to look
@mmalvarez
mmalvarez / coq-searchany.patch
Created March 5, 2015 21:42
Coq SearchAny Patch
From 8fa45911905da8fd1732f79ec95b0c9733c07d6c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= <clement.pitclaudel@live.com>
Date: Mon, 16 Feb 2015 08:34:20 -0500
Subject: [PATCH 1/3] vernac: Add a SearchAny command to print all identifiers
"SearchAny" does the same as "SearchPattern _", but it doesn't print
definition bodies, yielding an about 10x reduction in the size of the
answer. This is useful for tools that need to list all identifiers in
context at a given point in a proof (for en example of such a tool see
https://github.com/cpitclaudel/company-coq/)