pingu/mambo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Cut it out :D

Browse Source
This commit is contained in:
pingu
2025-12-30 10:30:10 +01:00
parent 6feae5fb04
commit d74a05393a
1 changed files with 31 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

34
mambo.agda
View File

@@ -215,10 +215,38 @@ weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁)
weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁)) weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁))
cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
cut Γ' x x₁ = {!!} cut [] x (var x₁) = mp (⇒ᵢ (var x₁)) x
cut (Γ' , x₂) x (var (zero x₁ xs)) = var (zero x₂ (Γ' ++ _))
cut (Γ' , x₂) x (var (succ _ xs x₃)) = weak (cut Γ' x (var x₃)) λ {X} → succ X (Γ' ++ _)
cut Γ' x (mp x₁ x₂) = mp (cut Γ' x x₁) (cut Γ' x x₂)
cut Γ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut Γ' x x₁) (cut Γ' x x₂)
cut Γ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut Γ' x x₁)
cut Γ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut Γ' x x₁)
cut Γ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut Γ' x x₁)
cut Γ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut Γ' x x₁)
cut Γ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut Γ' x x₁) (cut (Γ' , _) x x₂) (cut (Γ' , _ ) x x₃)
cut Γ' x (⇒ᵢ x₁) = ⇒ᵢ (cut (Γ' , _) x x₁)
cut Γ' x (¬ᵢ x₁) = ¬ᵢ (cut (Γ' , _) x x₁)
cut Γ' x (¬ₑ x₁ x₂) = ¬ₑ (cut Γ' x x₁) (cut Γ' x x₂)
cut Γ' x (⊥ₑ x₁) = ⊥ₑ (cut Γ' x x₁)
cut Γ' x (□ᵢ x₁) = □ᵢ x₁
cut Γ' x (□ₑ x₁ x₂) = □ₑ (cut Γ' x x₁) (cut Γ' (weak-modal x (λ {X = X₁} → succ X₁ _)) x₂)
cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B cut-modal : (Δ' : Context) → [] / Δ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
cut-modal = {!!} cut-modal Δ' x (var x₁) = var x₁
cut-modal Δ' x (mp x₁ x₂) = mp (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
cut-modal Δ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
cut-modal Δ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut-modal Δ' x x₁)
cut-modal Δ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut-modal Δ' x x₁)
cut-modal Δ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut-modal Δ' x x₁)
cut-modal Δ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut-modal Δ' x x₁)
cut-modal Δ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂) (cut-modal Δ' x x₃)
cut-modal Δ' x (⇒ᵢ x₁) = ⇒ᵢ (cut-modal Δ' x x₁)
cut-modal Δ' x (¬ᵢ x₁) = ¬ᵢ (cut-modal Δ' x x₁)
cut-modal Δ' x (¬ₑ x₁ x₂) = ¬ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
cut-modal Δ' x (⊥ₑ x₁) = ⊥ₑ (cut-modal Δ' x x₁)
cut-modal Δ' x (□ᵢ x₁) = □ᵢ (cut Δ' x x₁)
cut-modal Δ' x (□ₑ x₁ x₂) = □ₑ (cut-modal Δ' x x₁) (cut-modal (Δ' , _) x x₂)
KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))) KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))