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 / walks.v
Created July 12, 2022 05:00
walking a graph
Require Import List.
Import ListNotations.
CoInductive Graph (X : Type) : Type :=
| node : X -> list (Graph X) -> Graph X.
Arguments node {_}.
Fixpoint walks {X} (n : nat) (g : Graph X)
{struct n} : list (list X) :=
@emarzion
emarzion / non_decr_functional.v
Last active June 22, 2022 02:08
Defining a functional that finds a non-decreasing abscissa for any function from nat to nat
Require Import Lia.
Lemma non_decr_point_aux : forall (n : nat) (f : nat -> nat),
f 0 <= n -> { x : nat & f x <= f (S x) }.
Proof.
induction n; intros f f0.
- exists 0; lia.
- destruct (Compare_dec.le_lt_dec (f 0) (f 1))
as [f0_nondecr|f0_decr].
+ exists 0; exact f0_nondecr.
@emarzion
emarzion / countable_sig_fin.v
Created November 11, 2021 05:13
A countable sum of non-empty finite sets is countable
Require Import Lia.
Require Import Wf_nat.
Section Fin.
Fixpoint Fin n : Type :=
match n with
| 0 => Empty_set
| S m => unit + Fin 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.
@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 / 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 / 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 / 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 / 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 / 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;