module Universe where
open import Data.Nat
data SPT : ℕ -> Set1 where
vz : {n : ℕ} -> SPT (suc n)
vs : {n : ℕ} -> SPT n -> SPT (suc n)
_[_] : {n : ℕ} -> SPT (suc n) -> SPT n -> SPT n
“0” : {n : ℕ} -> SPT n
“1” : {n : ℕ} -> SPT n
_“+”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
_“×”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
_“->”_ : {n : ℕ} -> (K : Set) -> SPT n -> SPT n
“μ”_ : {n : ℕ} -> SPT (suc n) -> SPT n
data Tel : ℕ -> (ℕ -> Set1) -> Set2 where
ε : (F : ℕ -> Set1) -> Tel zero F
_^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) F
data ⟦_⟧_ : {n : ℕ} -> SPT n -> Tel n SPT -> Set2 where
top : {n : ℕ} -> {T' : Tel n SPT} -> {T : SPT n} ->
⟦ T ⟧ T' -> ⟦ vz ⟧ (T ^ T')
pop : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
⟦ T ⟧ T' -> ⟦ vs T ⟧ (S ^ T')
def : {n : ℕ} -> {T' : Tel n SPT} -> {A : SPT n} -> {F : SPT (suc n)} ->
⟦ F ⟧ (A ^ T') -> ⟦ F [ A ] ⟧ T'
void : {n : ℕ} -> {T' : Tel n SPT} ->
⟦ “1” ⟧ T'
inl : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
⟦ S ⟧ T' -> ⟦ S “+” T ⟧ T'
inr : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
⟦ T ⟧ T' -> ⟦ S “+” T ⟧ T'
pair : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ S “×” T ⟧ T'
funk : {n : ℕ} -> {T' : Tel n SPT} -> {K : Set} -> {T : SPT n} ->
(f : K -> ⟦ T ⟧ T') -> ⟦ (K “->” T) ⟧ T'
miso : {n : ℕ} -> {T' : Tel n SPT} -> {F : SPT (suc n)} ->
⟦ F ⟧ ((“μ” F) ^ T') -> ⟦ (“μ” F) ⟧ T'
“Nat” : {n : ℕ} -> SPT n
“Nat” = “μ” (“1” “+” vz)
“zero” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T'
“zero” = miso (inl (void))
“succ” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“succ” x = miso (inr (top x))
data “Nat”-View : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> Set2 where
isZero : {n : ℕ} -> {T' : Tel n SPT} -> “Nat”-View {n} {T'} “zero”
isSucc : {n : ℕ} -> {T' : Tel n SPT} -> (x : ⟦ “Nat” ⟧ T') -> “Nat”-View {n} {T'} (“succ” x)
viewNat : {n : ℕ} -> {T' : Tel n SPT} -> (n : ⟦ “Nat” ⟧ T') -> “Nat”-View n
viewNat {n} {T'} (miso Q) = aux1 Q
where aux3 : (r : ⟦ vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inr r))
aux3 (top x) = isSucc x
aux2 : (l : ⟦ “1” ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inl l))
aux2 void = isZero
aux1 : (u : ⟦ “1” “+” vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso u)
aux1 (inl U) = aux2 U
aux1 (inr V) = aux3 V
“add” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“add” x y with viewNat x
“add” (miso (inl (void))) y | isZero = y
“add” (miso (inr (top x))) y | isSucc .x = “succ” (“add” x y)
test = “add” {zero} {ε SPT}
(“succ” (“succ” (“succ” “zero”)))
(“succ” (“succ” “zero”))
{- =
miso
(inr
(top
(miso
(inr
(top
(miso
(inr
(top
(miso (inr (top (miso (inr (top (miso (inl void)))))))))))))))) -}
Emulate Agda style pattern matching in Coq using ideas frow Eliminating Dependent Pattern Matching..
Require Import JMeq.
Infix "==" := JMeq (at level 31).
Notation "[ x : X ] == [ y : Y ]" := (@JMeq X x Y y) (at level 30).
Notation "X =/= Y" := (JMeq _ X _ Y -> False) (at level 30).
Derive NoConfusion nat.
Definition noConfusion_nat (P : Type) (u v : nat) : JMeq u v -> NoConfusion_nat P u v.
intros.
elim H.
elim u;
simpl; intros; tauto.
Defined.
Inductive SPT : nat -> Type :=
| vz {n} : SPT (S n)
| vs {n} : SPT n -> SPT (S n)
| of {n} : SPT (S n) -> SPT n -> SPT n
| q_zero_q {n} : SPT n
| q_one_q {n} : SPT n
| q_sum_q {n} : SPT n -> SPT n -> SPT n
| q_mul_q {n} : SPT n -> SPT n -> SPT n
| q_arrow_q {n} : Type -> SPT n -> SPT n
| q_mu_q {n} : SPT (S n) -> SPT n.
Derive NoConfusion SPT.
Definition noConfusion_SPT (P : Type) (e1 : nat) (u v : SPT e1) : JMeq u v -> NoConfusion_SPT P e1 u v.
intros.
elim H.
elim u;
simpl; intros; tauto.
Defined.
Inductive Tel : nat -> (nat -> Type) -> Type :=
| eps : forall {F}, Tel 0 F
| telCons : forall {F} {n}, Tel n F -> F n -> Tel (S n) F.
Infix ";" := telCons (at level 27, left associativity).
Derive NoConfusion Tel.
Definition noConfusion_Tel (P : Type) (e1 : nat) (e2 : nat -> Type) (u v : Tel e1 e2) : JMeq u v -> NoConfusion_Tel P e1 e2 u v.
intros.
elim H.
elim u;
simpl; intros; tauto.
Defined.
Reserved Notation "⟦ type ⟧ scope" (at level 30, no associativity).
Inductive Interpretation : forall n, SPT n -> Tel n SPT -> Type :=
| top {n} {T' : Tel n SPT} {T : SPT n}
: ⟦ T ⟧ T' -> ⟦ vz ⟧ (T';T)
| pop {n} {T' : Tel n SPT} {S T : SPT n}
: ⟦ T ⟧ T' -> ⟦ vs T ⟧ (T';S)
| def {n} {T' : Tel n SPT} {A : SPT n} {F : SPT (S n)}
: ⟦ F ⟧ (T'; A) -> ⟦ of F A ⟧ T'
| void {n} {T' : Tel n SPT}
: ⟦ q_one_q ⟧ T'
| inl {n} {T' : Tel n SPT} {S T : SPT n}
: ⟦ S ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| inr {n} {T' : Tel n SPT} {S T : SPT n}
: ⟦ T ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| pair {n} {T' : Tel n SPT} {S T : SPT n}
: ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ q_mul_q S T ⟧ T'
| funk {n} {T' : Tel n SPT} {K : Type} {T : SPT n}
: (K -> ⟦ T ⟧ T') -> ⟦ q_arrow_q K T ⟧ T'
| miso {n} {T' : Tel n SPT} {F : SPT (S n)}
: ⟦ F ⟧ (T';q_mu_q F) -> ⟦ q_mu_q F ⟧ T'
where "⟦ type ⟧ scope" := (Interpretation _ type scope).
Derive NoConfusion Interpretation.
Definition noConfusion_Interpretation (P : Type) (e1 : nat) (e2 : SPT e1) (e3 : Tel e1 SPT) (u v : ⟦e2 ⟧ e3) : JMeq u v -> NoConfusion_Interpretation P e1 e2 e3 u v.
intros.
elim H.
elim u;
simpl; intros; tauto.
Defined.
Definition mu_injective (P : Type) (e1 : nat) (u v : SPT (S e1))
: (e1 == e1 -> u == v -> P) -> (q_mu_q u == q_mu_q v -> P)
:= fun m Eq =>
noConfusion_SPT P _ (q_mu_q u) (q_mu_q v) Eq m.
Definition mu_vz_clash (P : Type) (n : nat) (F : SPT (S (S n)))
: q_mu_q F == vz -> P
:= fun Eq =>
noConfusion_SPT P (S n) (q_mu_q F) vz Eq.
Definition q_Nat_q {n} : SPT n := q_mu_q (q_sum_q q_one_q vz).
Definition q_O_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' := miso (inl void).
Definition q_S_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> ⟦ q_Nat_q ⟧ T' := fun x => miso (inr (top x)).
Inductive q_Nat_q'View {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> Type :=
| isO : q_Nat_q'View q_O_q
| isS : forall x : ⟦ q_Nat_q ⟧ T', q_Nat_q'View (q_S_q x).
Ltac dpm_lift := repeat match goal with H : _ |- _ => intro Eq; revert H; revert Eq end.
Ltac dpm_prepare :=
match goal with
| |- @JMeq _ ?x _ ?x -> _ => intros _; dpm_prepare
| |- @JMeq _ _ _ _ -> _ => dpm_lift
| _ => intro; dpm_prepare
end.
Ltac dpm_subst := intro Eql;
match type of Eql with @JMeq _ ?x _ ?y =>
(rewrite Eql; clear x Eql) || (rewrite <- Eql; clear y Eql)
end.
Ltac dpm_confusion := intro Eql;
match goal with |- ?P =>
apply (noConfusion_nat P _ _ Eql)||
apply (noConfusion_SPT P _ _ _ Eql)||
apply (noConfusion_Tel P _ _ _ _ Eql)||
apply (noConfusion_Interpretation P _ _ _ _ _ Eql)
end.
Ltac dpm_specialize := repeat (dpm_prepare; (dpm_subst||dpm_confusion)).
Definition view'q_Nat_q
(n : nat) (Ts : Tel n SPT) (x : ⟦ q_Nat_q ⟧ Ts) : (@q_Nat_q'View n Ts x).
intros.
refine
(Interpretation_rect
(fun n' S' Ts' x' =>
n == n' -> @q_Nat_q n == S' -> Ts == Ts' -> x == x' ->
q_Nat_q'View x)
_ _ _ _ _ _ _ _ _
n q_Nat_q Ts x
(JMeq_refl n) (JMeq_refl (@q_Nat_q n)) (JMeq_refl Ts) (JMeq_refl x));
unfold q_Nat_q in *;
dpm_specialize;
intros _.
refine
(Interpretation_rect
(fun n0' S' Ts' i' =>
S n0 == n0' -> q_sum_q q_one_q vz == S' -> T'; q_mu_q (q_sum_q q_one_q vz) == Ts' -> i == i' ->
q_Nat_q'View (miso i))
_ _ _ _ _ _ _ _ _
(S n0) (q_sum_q q_one_q vz) (T'; q_mu_q (q_sum_q q_one_q vz)) i
(JMeq_refl (S n0)) (JMeq_refl (q_sum_q q_one_q vz)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i));
dpm_specialize;
intros _.
refine
(Interpretation_rect
(fun n0' S' Ts' i0' =>
S n0 == n0' -> q_one_q == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
q_Nat_q'View (miso (inl i0)))
_ _ _ _ _ _ _ _ _
(S n0) q_one_q (T'; q_mu_q (q_sum_q q_one_q vz)) i0
(JMeq_refl (S n0)) (JMeq_refl (q_one_q)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize.
exact isO.
refine
(Interpretation_rect
(fun n0' S' Ts' i0' =>
S n0 == n0' -> vz == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
q_Nat_q'View (miso (inr i0)))
_ _ _ _ _ _ _ _ _
(S n0) vz (T'; q_mu_q (q_sum_q q_one_q vz)) i0
(JMeq_refl (S n0)) (JMeq_refl vz) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize;
intros _.
exact (isS i).
Defined.
No comments:
Post a Comment