Skip to content

Instantly share code, notes, and snippets.

(* The goal of this file is to define the free bounded distributive lattice
on a set of generators, subject to some equations and inequations.
To do so, we first define the signature for distributive lattices,
then its equational theory, and show that any model of this
equational theory yield an instance of [IsBoundedDistributiveLattice].
We introduce the notion of a presentation of a bounded distributive
lattice and obtain free objects by interpreting such a presentation
as an extension of the equational theory of distributive lattices.
We use these tools to define the presentation of the underlying
distributive lattice of the Spectrum of a ring as presented in
module GradualSTLC where
open import Agda.Primitive
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Maybe
@kyoDralliam
kyoDralliam / acc_idc.v
Created March 18, 2022 12:44
Accessibility and extraction of infinite decending chains
From Equations Require Import Equations.
From Coq Require Import ssreflect.
Section Defs.
Context {A : Type} (R : A -> A -> Prop).
Definition entire := forall x, exists y, R y x.
Definition idc_from a0 :=
exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).
@kyoDralliam
kyoDralliam / some.v
Created April 12, 2022 12:35
Discriminator and Projector for Some in option type
From Coq Require Import ssreflect.
From Coq Require Import StrictProp.
From Coq Require Import List.
(* Access to nth element of a list,
stdpp's notation for simpler test writing *)
Notation "l !! n" := (nth_error l n) (at level 20).
(** Discriminator for Some *)
@kyoDralliam
kyoDralliam / unnestingEq.v
Created December 9, 2022 11:12
Trying to unnest the "pathological" example of an inductive type that nests with an indexed family, here equality (compiles with coq 8.16, equations 1.3)
(** Trying to unnest the "pathological" example of an inductive type
that nests with an indexed family, here equality *)
Inductive I := K : forall x : I, x = x -> I.
(* A more general induction principle for I than what Coq generates *)
Section GeneralElim.