Skip to content

Instantly share code, notes, and snippets.

@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 / 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 / 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;
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.

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.
*)
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.
Notation "P ≢ Q" := (~(P <-> Q))(at level 100).
Theorem no_middle : ~(exists P, (P ≢ True) /\ (P ≢ False)).
Proof.
intro h.
destruct h as [P [h1 h2]].
apply h2.
split; [ | intros h; contradiction].
intros h3.
apply h1; split; auto.