Skip to content

Instantly share code, notes, and snippets.

@damhiya

damhiya/SubstitutionSystem.v

Last active July 31, 2025 14:40
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save damhiya/8995fe14ce06d94e286baf55fdcb9e14 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save damhiya/8995fe14ce06d94e286baf55fdcb9e14 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SubstitutionSystem.v
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)
.
Arguments nil {A P}.
Arguments cons {A P} {x xs} P_x P_xs.
End Forall.
Module Fin.
Definition code (n : nat) : Type :=
match n with
| O => Empty_set
| S m => option (Fin.t m)
end.
Definition encode : forall {n}, Fin.t n -> code n :=
fun n i =>
match i with
| Fin.F1 => None
| Fin.FS j => Some j
end.
Definition decode : forall {n}, code n -> Fin.t n :=
fun n c =>
match n, c with
| 0, x => match x with end
| S m, None => Fin.F1
| S m, Some i => Fin.FS i
end.
Fixpoint from_list {A} (xs : list A) : fin (length xs) -> A :=
match xs with
| [] => fun i => match Fin.encode i with end
| x :: xs => fun i => match Fin.encode i with
| None => x
| Some i => from_list xs i
end
end.
Fixpoint from_Forall {A} {P} {xs : list A} (xs_all : Forall.t P xs) : forall (i : fin (length xs)), P (from_list xs i) :=
match xs_all in Forall.t _ xs return forall (i : fin (length xs)), P (from_list xs i) with
| Forall.nil => fun i => match Fin.encode i with end
| @Forall.cons _ _ x xs P_x P_xs => fun i => Fin.caseS' i (fun j => P (from_list (x :: xs) j)) P_x (from_Forall P_xs)
end.
End Fin.
Module Sig.
Record t : Type :=
{
Constructor : Type;
Arity : Constructor -> Type;
Change : forall c, Arity c -> Type -> Type;
Change_map : forall c (i : Arity c) [A B] (f : A -> B), Change c i A -> Change c i B;
Change_shift : forall [Z : Type -> Type] (Z_map : forall [A B], (A -> B) -> (Z A -> Z B)) (Z_ptd : forall [A], A -> Z A) c (i : Arity c) [A B : Type], (A -> Z B) -> (Change c i A -> Z (Change c i B));
}.
Record ext (S : t) (F : Type -> Type) (A : Type) : Type :=
{
constructor : S.(Constructor);
arguments : forall (i : S.(Arity) constructor), F (S.(Change) constructor i A)
}.
Arguments constructor {S F A} e.
Arguments arguments {S F A} e.
Definition map1 {S : t} {F : Type -> Type} (F_map : forall [A B], (A -> B) -> (F A -> F B)) [A B] (f : A -> B) (e : ext S F A) : ext S F B :=
{|
constructor := e.(constructor);
arguments := fun i => F_map (S.(Change_map) e.(constructor) i f) (e.(arguments) i);
|}.
Definition map2 {S : t} [F G : Type -> Type] (α : forall [A], F A -> G A) [A] (e : ext S F A) : ext S G A :=
{|
constructor := e.(constructor);
arguments := fun i => α (e.(arguments) i);
|}.
(* strength derived from shift *)
Definition st
{S : t}
{F Z : Type -> Type}
(F_map : forall [A B], (A -> B) -> (F A -> F B))
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
: forall [A], Sig.ext S F (Z A) -> Sig.ext S (F ∘ Z) A :=
fun A e =>
{|
constructor := e.(constructor);
arguments := fun i => F_map (S.(Change_shift) Z_map Z_ptd e.(constructor) i id) (e.(arguments) i);
|}.
Definition transfer_gbind
{S : t}
{X : Type -> Type}
{Z : Type -> Type}
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
(k : forall [A B], (A -> Z B) -> (X A -> X B))
: forall [A B], (A -> Z B) -> (ext S X A -> ext S X B) :=
fun A B f e =>
{|
constructor := e.(constructor);
arguments := fun i => k (S.(Change_shift) Z_map Z_ptd e.(constructor) i f) (e.(arguments) i)
|}.
Definition transfer_gbind_from_st
{S : t}
{X : Type -> Type}
{Z : Type -> Type}
(X_map : forall [A B], (A -> B) -> (X A -> X B))
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
(k : forall [A B], (A -> Z B) -> (X A -> X B))
: forall [A B], (A -> Z B) -> (ext S X A -> ext S X B) :=
fun A B f e => map2 (F := X ∘ Z) (G := X) (fun A => k (id : Z A -> Z A)) (st X_map Z_map Z_ptd (map1 X_map f e)).
Fact transfer_gbind_eq
{S : t}
{X : Type -> Type}
{Z : Type -> Type}
(X_map : forall [A B], (A -> B) -> (X A -> X B))
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
(k : forall [A B], (A -> Z B) -> (X A -> X B))
[A B]
(f : A -> Z B)
(e : ext S X A)
: transfer_gbind Z_map Z_ptd k f e = transfer_gbind_from_st X_map Z_map Z_ptd k f e.
Proof.
destruct e as [c args]; simpl.
unfold transfer_gbind, transfer_gbind_from_st, map2; simpl. f_equal. extensionality i.
Abort.
End Sig.
Module Term.
Inductive t (S : Sig.t) (A : Type) : Type :=
| var : A -> t S A
| cons : Sig.ext S (t S) A -> t S A
.
Arguments var {S} [A] x.
Arguments cons {S} [A] ts.
Fixpoint map {S} [A B] (f : A -> B) (tm : t S A) {struct tm} : t S B :=
match tm with
| var x => var (f x)
| cons ts => cons (Sig.map1 map f ts)
end.
Fail Fixpoint gjoin {S} {Z : Type -> Type} (Z_map : forall [A B], (A -> B) -> (Z A -> Z B)) (Z_ptd : forall [A], A -> Z A) (Z_inc : forall [A], Z A -> t S A) [A] (tm : t S (Z A)) {struct tm} : t S A :=
match tm with
| var t => Z_inc t
| cons ts => cons (Sig.map2 (gjoin Z_map Z_ptd Z_inc) (Sig.st map Z_map Z_ptd ts))
end.
Fail Fixpoint join {S} [A : Type] (tm : t S (t S A)) {struct tm} : t S A :=
match tm with
| var t => t
| cons ts => cons (Sig.map2 join (Sig.st map map var ts))
end.
Fixpoint gbind {S} {Z : Type -> Type} (Z_map : forall [A B], (A -> B) -> (Z A -> Z B)) (Z_ptd : forall [A], A -> Z A) (Z_inc : forall [A], Z A -> t S A) [A B] (f : A -> Z B) (tm : t S A) : t S B :=
match tm with
| var x => Z_inc (f x)
| cons ts => cons (Sig.transfer_gbind Z_map Z_ptd (gbind Z_map Z_ptd Z_inc) f ts)
end.
Fixpoint bind {S} [A B] (f : A -> t S B) (tm : t S A) : t S B :=
match tm with
| var x => f x
| cons ts => cons (Sig.transfer_gbind map var bind f ts)
end.
Definition gjoin {S} {Z : Type -> Type} (Z_map : forall [A B], (A -> B) -> (Z A -> Z B)) (Z_ptd : forall [A], A -> Z A) (Z_inc : forall [A], Z A -> t S A) [A] (tm : t S (Z A)) : t S A :=
gbind Z_map Z_ptd Z_inc id tm.
Definition join {S} [A : Type] (tm : t S (t S A)) : t S A :=
bind id tm.
End Term.
Module Lam.
Variant Constructor : Type :=
| _lam
| _app
.
Definition Arity (c : Constructor) : Type :=
match c with
| _lam => fin 1
| _app => fin 2
end.
Definition Change c : Arity c -> Type -> Type :=
match c with
| _lam => Fin.from_list [option]
| _app => Fin.from_list [id; id]
end.
Definition id_map : forall [A B], (A -> B) -> (id A -> id B) :=
fun A B f => f.
Definition Change_map c : forall (i : Arity c), forall [A B], (A -> B) -> Change c i A -> Change c i B.
refine (match c with
| _lam => Fin.from_Forall (_ : Forall.t (fun F => forall A B, (A -> B) -> (F A -> F B)) [option])
| _app => Fin.from_Forall (_ : Forall.t (fun F => forall A B, (A -> B) -> (F A -> F B)) [id;id])
end).
- exact (Forall.cons option_map Forall.nil).
- exact (Forall.cons id_map (Forall.cons id_map Forall.nil)).
Defined.
Definition option_shift
{Z : Type -> Type}
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
: forall [A B], (A -> Z B) -> (option A -> Z (option B)) :=
fun A B f v =>
match v with
| Some v => Z_map Some (f v)
| None => Z_ptd None
end.
Definition id_shift
{Z : Type -> Type}
: forall [A B], (A -> Z B) -> (id A -> Z (id B)) :=
fun A B f => f.
Definition Change_shift
[Z : Type -> Type]
(Z_map : forall [A B], (A -> B) -> (Z A -> Z B))
(Z_ptd : forall [A], A -> Z A)
c
: forall (i : Arity c), forall [A B : Type], (A -> Z B) -> (Change c i A -> Z (Change c i B)).
refine (match c with
| _lam => Fin.from_Forall (_ : Forall.t (fun F => forall A B, (A -> Z B) -> (F A -> Z (F B))) [option])
| _app => Fin.from_Forall (_ : Forall.t (fun F => forall A B, (A -> Z B) -> (F A -> Z (F B))) [id;id])
end).
- exact (Forall.cons (option_shift Z_map Z_ptd) Forall.nil).
- exact (Forall.cons id_shift (Forall.cons id_shift Forall.nil)).
Defined.
Definition S : Sig.t :=
{|
Sig.Constructor := Constructor;
Sig.Arity := Arity;
Sig.Change := Change;
Sig.Change_map := Change_map;
Sig.Change_shift := Change_shift;
|}.
Definition t := Term.t S.
Definition var : forall [A], A -> t A := Term.var.
Definition lam : forall [A], t (option A) -> t A.
intros A t.
eapply Term.cons.
refine (Sig.Build_ext S _ _ _lam _).
intros i. simpl in *.
destruct (Fin.encode i) as [j|].
- destruct (Fin.encode j).
- eapply t.
Defined.
Definition app : forall [A], t A -> t A -> t A.
intros A t1 t2.
eapply Term.cons.
refine (Sig.Build_ext S _ _ _app _).
intros i. simpl in *.
destruct (Fin.encode i) as [j|].
- destruct (Fin.encode j) as [k|].
+ destruct (Fin.encode k).
+ eapply t2.
- eapply t1.
Defined.
End Lam.
Section EXAMPLES.
Example tm_id {A} : Lam.t A := Lam.lam (Lam.var None).
Example tm_ω {A} : Lam.t A := Lam.lam (Lam.app (Lam.var None) (Lam.var None)).
Example tm_Ω {A} : Lam.t A := Lam.app tm_ω tm_ω.
End EXAMPLES.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment