Soonwon Moon damhiya

damhiya / SubstitutionSystem.v

Last active July 31, 2025 14:40

	Set Primitive Projections.

	From Coq Require Import Program.
	From stdpp Require Import fin.

	Module Forall.

	Inductive t {A : Type} (P : A -> Type) : list A -> Type :=
	\| nil : t P List.nil
	\| cons : forall {x xs}, P x -> t P xs -> t P (cons x xs)

damhiya / IndexedContainer.v

Last active August 1, 2025 05:14

	Set Primitive Projections.

	Module Container.

	Record t (I : Type) (O : Type) : Type :=
	{
	Command : forall (o : O), Type; (* shape *)
	Response : forall (o : O) (c : Command o), Type; (* position or degree *)
	next : forall (o : O) (c : Command o) (r : Response o c), I;
	} as C.

damhiya / Stlc.v

Last active July 25, 2025 10:45

damhiya / Syntax.v

Last active June 14, 2025 13:52

Intrinsically well-scoped de Bruijn representation with fancy notation

	From Coq Require Import String.
	From stdpp Require Import base strings.

	Section AUX.

	#[global] Instance option_eq_dec_normalizable A `{dec : EqDecision A} : EqDecision (option A).
	Proof.
	intros x y. destruct x as [x\|], y as [y\|].
	- destruct (decide (x = y)).
	+ left. congruence.

damhiya / Cubical.HITs.CauchyReal.Base.agda

Created June 8, 2025 08:27

Cauchy real

	{-# OPTIONS --safe #-}
	module Cubical.HITs.CauchyReal.Base where

	open import Cubical.Foundations.Prelude
	open import Cubical.Data.Rationals.Base
	open import Cubical.Data.Rationals.Order
	open import Cubical.Data.Rationals.Properties
	open import Cubical.Data.PositiveRational.Base

	-- Higher inductive-inductive construction of Cauchy real, as in the HoTT book.

damhiya / Minimization.v

Last active June 8, 2025 07:52

Minimization

	From Coq Require Import Lia.

	Section TERMINATION.

	Inductive terminate (P : nat -> Prop) : nat -> Prop :=
	\| found : forall n, P n -> terminate P n
	\| step : forall n, terminate P (S n) -> terminate P n
	.

	Fixpoint terminate_ind_dep

damhiya / Quotient.v

Last active May 12, 2025 07:12

quotient

	Set Primitive Projections.

	From Coq Require
	Program
	Logic.ProofIrrelevance
	Logic.PropExtensionality
	Logic.FunctionalExtensionality
	Logic.Epsilon
	Relations.Relation_Operators.

damhiya / lambda.v

Created January 23, 2025 13:31

	From Coq Require Fin.

	Definition ifun (X Y : nat -> Type) : Type := forall i, X i -> Y i.
	Definition δ (X : nat -> Type) (n : nat) := X (S n).
	Definition prod (X Y : nat -> Type) (n : nat) := (X n * Y n)%type.
	Definition sum (X Y : nat -> Type) (n : nat) := (X n + Y n)%type.

	Definition TermF' (X : nat -> Type) := sum (δ X) (prod X X).

	Variant TermF (X : nat -> Type) : nat -> Type :=

damhiya / bits.v

Created August 26, 2024 16:56

Breaking subject reduction in Coq using positive coinductive types

	CoInductive bits : Set :=
	\| c0 : bits -> bits
	\| c1 : bits -> bits.

	Lemma bits_eta : forall xs, match xs with
	\| c0 xs' => c0 xs'
	\| c1 xs' => c1 xs'
	end = xs.
	Proof.
	intro xs. destruct xs; reflexivity.

damhiya / FAlg.hs

Last active May 23, 2024 03:58

recursor