Skip to content

Instantly share code, notes, and snippets.

View emarzion's full-sized avatar
☕

Evan Marzion emarzion

☕
7 followers · 4 following
  • Wauwatosa
View GitHub Profile
@emarzion
emarzion / variadic_curry.v
Created February 16, 2019 04:50
variadic currying function
Definition f_id : forall X Y, (X -> Y) -> X -> Y := fun X Y f => f.
Definition next : forall W X Y Z, ((X -> Y) -> Z) -> (W * X -> Y) -> W -> Z :=
fun W X Y Z f g x => f (fun y => g (x,y)).
Fixpoint arity X n :=
match n with
| 0 => X
| S m => X -> arity X m
@emarzion
emarzion / cyclic_inj.v
Created May 12, 2018 01:34
Call a function cyclic if any point can be reached from another point after finitely many application of the function in question. I provide an entirely constructive proof that all cyclic functions are injections.
Set Implicit Arguments.
Require Import Omega.
Require Import Wf_nat.
Require Import Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
(* simultaneously produces a proof of the arith. equation eq and uses it to rewrite in the goal *)
Ltac omega_rewrite eq :=
let Hf := fresh in
@emarzion
emarzion / nat list encoding.v
Created November 26, 2017 19:15
A certified encoding of lists of natural numbers into natural numbers
Set Implicit Arguments.
Require Import Omega.
(* equivalence of types along with elementary facts *)
Definition equiv(X Y : Type) := {f : X -> Y & {g : Y -> X & (forall x, g (f x) = x) /\
(forall y, f (g y) = y)}}.
Lemma equiv_trans(X Y Z : Type) : equiv X Y -> equiv Y Z -> equiv X Z.
Proof.