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 / 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.
@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 / 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 / perms.v
Created December 5, 2019 09:21
computing n perm k the stupid way
Require Import SetoidClass Nat.
Fixpoint Fin n :=
match n with
| 0 => Empty_set
| S m => (unit + Fin m)%type
end.
Class Finite(X : Type)`{Setoid X} := {
card : nat;
@emarzion
emarzion / monotone_cofinal.v
Created February 7, 2020 09:16
A simple proof that monotone functions over the naturals are cofinal
Require Import Lia PeanoNat.
Definition monotone(f : nat -> nat) :=
forall x, f x < f (S x).
Definition cofinal(f : nat -> nat) :=
forall x, { y : nat & x < f y }.
Lemma monotone_cofinal : forall f, monotone f -> cofinal f.
Proof.
@emarzion
emarzion / rose.v
Created April 29, 2020 09:48
rose tree induction example
Require Import List.
Inductive rose(X : Type) : Type :=
| node : X -> list (rose X) -> rose X.
Fixpoint rose_map{X Y}(f : X -> Y)(r : rose X) : rose Y :=
match r with
| node _ x rs => node _ (f x) (List.map (rose_map f) rs)
end.
@emarzion
emarzion / ternary.v
Created September 28, 2020 22:50
isomorphism between binary and ternary cantor space
Require Import Wf_nat Lia.
Inductive three := a | b | c.
(* a => 0; b => 10; c => 11 *)
Fixpoint encode(f : nat -> three)(n : nat) : bool :=
match f 0 with
| a => match n with
| 0 => false
@emarzion
emarzion / int.v
Created November 22, 2020 04:47
intuitionistic proof that cantor space doesn't surject onto the natural numbers
Require Import Lia PeanoNat Bool.Bool.
Section Exhaustible.
Definition surj{X Y}(f : X -> Y) :=
forall y, exists x, f x = y.
Definition dec(P : Prop) := {P} + {~P}.
Definition exh(X : Type) := forall p : X -> bool,
@emarzion
emarzion / equations_example.v
Last active March 3, 2021 00:06
Require Import Equations.Equations.
Require Import Lia.
Require Import List.
Import ListNotations.
Fixpoint count_up n :=
match n with
| 0 => []
| S m => 0 :: map S (count_up m)
end.
@emarzion
emarzion / FPO_products.v
Last active May 3, 2021 00:29
Proof that sets with fixed-point operators is closed under binary products.
Definition FPO{X}(Y : (X -> X) -> X) :=
forall f, f (Y f) = Y f.
Section FPOs.
Variables A B : Type.
Variable Y_A : (A -> A) -> A.
Variable Y_B : (B -> B) -> B.
Hypothesis Y_A_FPO : FPO Y_A.