Skip to content

Instantly share code, notes, and snippets.

View codyroux's full-sized avatar

codyroux

68 followers · 4 following
View GitHub Profile
@codyroux
codyroux / a_little_arithmetic.v
Last active September 5, 2017 14:33
An arithmetic development that uses equality over Type rather than Prop.
(* Sigma types *)
(* Inductive Sigma (A:Set)(B:A -> Set) :Set := Spair: forall a:A, forall b : B a,Sigma A B. *)
(* Definition E (A:Set)(B:A -> Set) (C: Sigma A B -> Set) (c: Sigma A B) *)
(* (d: (forall x:A, forall y:B x, C (Spair A B x y))): C c := *)
(* match c as c0 return (C c0) with *)
(* | Spair a b => d a b *)
(* end. *)
@codyroux
codyroux / euclid.v
Last active December 31, 2015 04:29
Arithmetic, again
(* Cleanup and proofs of user11942s code *)
Print sigT.
Print sum.
Print False.
Print unit.
@codyroux
codyroux / finite_is_dec.v
Created February 5, 2021 22:10
Andrej finite is dec
Definition directed (D : Prop -> Prop) :=
(exists p, D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\ (q -> r).
Definition finite (p : Prop) :=
forall D, directed D ->
(p -> exists q, D q /\ q) ->exists q, D q /\ (p -> q).
Lemma is_directed_with_p p : directed (fun q => ~q \/ (p /\ q)).
@codyroux
codyroux / dial_2.v
Created February 5, 2021 22:32
Valeria: Dial_2(Set) is a category
Record Dial_2 :=
{
U : Type;
X : Type;
alpha : U -> X -> Prop
}.
Record Mor (A B : Dial_2) :=
{
f : U A -> U B;
@codyroux
codyroux / tinylang.v
Created February 14, 2021 21:10
Set Implicit Arguments.
(* On importe le module qui definit les listes *)
Require Import List.
Print list.
Print option.
(* Une section permet de declarer des Hypotheses et des Variables *)
Section Typer.
@codyroux
codyroux / decreasing_diagrams.md
Created July 5, 2021 19:14

Confluence. It's not just a place where you can complain about colleagues to other colleagues.

It's also a property that is quite useful in many areas of CS!

As a reminder, a (non-deterministic) reduction relation --> is confluent if for every (multi-step) "peak" u *<-- t -->* v (I use -->* for the multi-step version of -->) there is a corresponding "valley": u -->* w *<-- v.

This basically says that your computation can't be "too"

@codyroux
codyroux / system_f.v
Created January 2, 2022 21:33
Aborted attempt to prove weak normalization (with weak reductions) of system F
(*
Ideas:
1. Strong reduction (ugh): Keep computing through lambdas. Most straightforward, but annoying, need to reason about db even more
2. Computability take an eval context as well, so that all predicates are "up to substitution".
Problem: how to we deal with "computable contexts"?
E.g. aplications: Do they thake the previous elements in the env or not?
Does "positive" style predicates help?
3. Screw this and go with names.
4. Reason about only closed terms (somehow?) Not sure how to formulate the main lemma.
@codyroux
codyroux / system_f_final.v
Created January 7, 2022 22:33
System F is normalizing, apparently.
(*
Ideas:
I'm borrowing generously from https://xavierleroy.org/talks/compilation-agay.pdf and
https://github.com/ajcave/code/blob/master/normalization/weak-head-bigstep-cbn.agda
But CBV.
*)
@codyroux
codyroux / HA2.v
Created February 6, 2022 03:54
Soundness of 2nd order arithmetic
(* A relatively straightforward formalization of HA^2 *)
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Inductive tm :=
| v(name : string)
| Succ(a : tm)
| Z
| Plus(a b : tm)
@codyroux
codyroux / is_a_neg_implies_em.v
Created September 3, 2022 15:44
Require Import Setoid.
Axiom is_a_neg : forall (P : Prop), exists (Q : Prop), P <-> ~Q.
Lemma not_not : forall P, ~~P -> P.
Proof.
intros P.
assert (h := is_a_neg P); destruct h as [Q h].
rewrite h.