module RecursiveTypes.Subterm where
open import Algebra
open import Data.Fin using (Fin; zero; suc; lift)
open import Data.Nat
open import Data.List using (List; []; _∷_; [_]; _++_)
open import Data.List.Properties
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡
open import Data.List.Any.Properties
open import Data.List.Any.Membership
open import Data.List.Any.BagAndSetEquality as BSEq
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalent)
open import Function.Inverse using (module Inverse)
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality hiding (trans)
open import Data.Fin.Substitution
private
open module SetM {A : Set} =
CommutativeMonoid (BSEq.commutativeMonoid set A)
using (_≈_)
open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
hiding (subst) renaming (id to idˢ)
open // using (_//_)
infix 4 _⊑_
data _⊑_ {n} : Ty n → Ty n → Set where
refl : ∀ {τ} → τ ⊑ τ
unfold : ∀ {σ τ₁ τ₂} (σ⊑ : σ ⊑ unfold[μ τ₁ ⟶ τ₂ ]) → σ ⊑ μ τ₁ ⟶ τ₂
⟶ˡ : ∀ {σ τ₁ τ₂} (σ⊑τ₁ : σ ⊑ τ₁) → σ ⊑ τ₁ ⟶ τ₂
⟶ʳ : ∀ {σ τ₁ τ₂} (σ⊑τ₂ : σ ⊑ τ₂) → σ ⊑ τ₁ ⟶ τ₂
unfold′ : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
unfold[μ τ₁ ⟶ τ₂ ] ⊑ μ τ₁ ⟶ τ₂
unfold′ = unfold refl
⟶ˡ′ : ∀ {n} {τ₁ τ₂ : Ty n} → τ₁ ⊑ τ₁ ⟶ τ₂
⟶ˡ′ = ⟶ˡ refl
⟶ʳ′ : ∀ {n} {τ₁ τ₂ : Ty n} → τ₂ ⊑ τ₁ ⟶ τ₂
⟶ʳ′ = ⟶ʳ refl
trans : ∀ {n} {σ τ χ : Ty n} →
σ ⊑ τ → τ ⊑ χ → σ ⊑ χ
trans σ⊑τ refl = σ⊑τ
trans σ⊑τ (unfold τ⊑) = unfold (trans σ⊑τ τ⊑)
trans σ⊑τ (⟶ˡ τ⊑δ₁) = ⟶ˡ (trans σ⊑τ τ⊑δ₁)
trans σ⊑τ (⟶ʳ τ⊑δ₂) = ⟶ʳ (trans σ⊑τ τ⊑δ₂)
mutual
infix 7 _∗ _∗′
_∗ : ∀ {n} → Ty n → List (Ty n)
τ ∗ = τ ∷ τ ∗′
_∗′ : ∀ {n} → Ty n → List (Ty n)
(τ₁ ⟶ τ₂) ∗′ = τ₁ ∗ ++ τ₂ ∗
(μ τ₁ ⟶ τ₂) ∗′ = (τ₁ ⟶ τ₂ ∷ τ₁ ∗ ++ τ₂ ∗) // sub (μ τ₁ ⟶ τ₂)
τ ∗′ = []
/-monoˡ : ∀ {m n σ τ} {ρ : Sub Ty m n} →
σ ⊑ τ → σ / ρ ⊑ τ / ρ
/-monoˡ refl = refl
/-monoˡ (⟶ˡ σ⊑τ₁) = ⟶ˡ (/-monoˡ σ⊑τ₁)
/-monoˡ (⟶ʳ σ⊑τ₂) = ⟶ʳ (/-monoˡ σ⊑τ₂)
/-monoˡ {ρ = ρ} (unfold {σ} {τ₁} {τ₂} σ⊑) =
unfold $ subst (λ χ → σ / ρ ⊑ χ)
(sub-commutes (τ₁ ⟶ τ₂))
(/-monoˡ σ⊑)
sub-⊑-μ : ∀ {n} {σ : Ty (suc n)} {τ₁ τ₂} →
σ ⊑ τ₁ ⟶ τ₂ → σ / sub (μ τ₁ ⟶ τ₂) ⊑ μ τ₁ ⟶ τ₂
sub-⊑-μ σ⊑τ₁⟶τ₂ = unfold (/-monoˡ σ⊑τ₁⟶τ₂)
sound : ∀ {n σ} (τ : Ty n) → σ ∈ τ ∗ → σ ⊑ τ
sound τ (here refl) = refl
sound (τ₁ ⟶ τ₂) (there σ∈) =
[ ⟶ˡ ∘ sound τ₁ , ⟶ʳ ∘ sound τ₂ ]′
(Inverse.from (++⇿ {xs = τ₁ ∗}) ⟨$⟩ σ∈)
sound (μ τ₁ ⟶ τ₂) (there (here refl)) = unfold refl
sound (μ τ₁ ⟶ τ₂) (there (there σ∈))
with Inverse.from (map-∈⇿ {xs = τ₁ ∗ ++ τ₂ ∗}) ⟨$⟩ σ∈
... | (χ , χ∈ , refl) =
sub-⊑-μ $ [ ⟶ˡ ∘ sound τ₁ , ⟶ʳ ∘ sound τ₂ ]′
(Inverse.from (++⇿ {xs = τ₁ ∗}) ⟨$⟩ χ∈)
sound ⊥ (there ())
sound ⊤ (there ())
sound (var x) (there ())
++-lemma : ∀ {A} xs ys {zs : List A} →
(xs ++ zs) ++ (ys ++ zs) ≈ (xs ++ ys) ++ zs
++-lemma xs ys {zs} = begin
(xs ++ zs) ++ (ys ++ zs) ≈⟨ SetM.assoc xs zs (ys ++ zs) ⟩
xs ++ (zs ++ (ys ++ zs)) ≈⟨ SetM.∙-cong (SetM.refl {x = xs}) (begin
zs ++ (ys ++ zs) ≈⟨ SetM.∙-cong (SetM.refl {x = zs}) (SetM.comm ys zs) ⟩
zs ++ (zs ++ ys) ≈⟨ SetM.sym $ SetM.assoc zs zs ys ⟩
(zs ++ zs) ++ ys ≈⟨ SetM.∙-cong (++-idempotent zs) SetM.refl ⟩
zs ++ ys ≈⟨ SetM.comm zs ys ⟩
ys ++ zs ∎) ⟩
xs ++ (ys ++ zs) ≈⟨ SetM.sym $ SetM.assoc xs ys zs ⟩
(xs ++ ys) ++ zs ∎
where open EqR ([ set ]-Equality _)
open ⊆-Reasoning
mutual
wk-∗-commute : ∀ k {n} (σ : Ty (k + n)) →
σ / wk ↑⋆ k ∗ ⊆ σ ∗ // wk ↑⋆ k
wk-∗-commute k σ (here refl) = here refl
wk-∗-commute k σ (there •∈•) = there $ wk-∗′-commute k σ •∈•
wk-∗′-commute : ∀ k {n} (σ : Ty (k + n)) →
σ / wk ↑⋆ k ∗′ ⊆ σ ∗′ // wk ↑⋆ k
wk-∗′-commute k (σ₁ ⟶ σ₂) = begin
σ₁ ⟶ σ₂ / wk ↑⋆ k ∗′ ≡⟨ refl ⟩
σ₁ / wk ↑⋆ k ∗ ++ σ₂ / wk ↑⋆ k ∗ ⊆⟨ wk-∗-commute k σ₁ ++-mono
wk-∗-commute k σ₂ ⟩
σ₁ ∗ // wk ↑⋆ k ++ σ₂ ∗ // wk ↑⋆ k ≡⟨ sym $ map-++-commute
(λ σ → σ / wk ↑⋆ k) (σ₁ ∗) (σ₂ ∗) ⟩
(σ₁ ∗ ++ σ₂ ∗) // wk ↑⋆ k ≡⟨ refl ⟩
σ₁ ⟶ σ₂ ∗′ // wk ↑⋆ k ∎
wk-∗′-commute k (μ σ₁ ⟶ σ₂) = begin
(μ σ₁ ⟶ σ₂) / wk ↑⋆ k ∗′ ≡⟨ refl ⟩
σ₁ ⟶ σ₂ / wk ↑⋆ (suc k) / sub (σ / wk ↑⋆ k) ∷
(σ₁ / wk ↑⋆ (suc k) ∗ ++ σ₂ / wk ↑⋆ (suc k) ∗)
// sub (σ / wk ↑⋆ k) ⊆⟨ lem₁ ++-mono lem₂ ⟩
σ₁ ⟶ σ₂ / sub σ / wk ↑⋆ k ∷
(σ₁ ∗ ++ σ₂ ∗) // sub σ // wk ↑⋆ k ≡⟨ refl ⟩
μ σ₁ ⟶ σ₂ ∗′ // wk ↑⋆ k ∎
where
σ = μ σ₁ ⟶ σ₂
lem₁ : _ ⊆ _
lem₁ = begin
[ σ₁ ⟶ σ₂ / wk ↑⋆ (suc k) / sub (σ / wk ↑⋆ k) ] ≡⟨ cong [_] $ sym $
sub-commutes (σ₁ ⟶ σ₂) ⟩
[ σ₁ ⟶ σ₂ / sub σ / wk ↑⋆ k ] ∎
lem₂ : _ ⊆ _
lem₂ = begin
(σ₁ / wk ↑⋆ (suc k) ∗ ++
σ₂ / wk ↑⋆ (suc k) ∗) // sub (σ / wk ↑⋆ k) ⊆⟨ map-mono _ $ wk-∗-commute (suc k) σ₁ ++-mono
wk-∗-commute (suc k) σ₂ ⟩
(σ₁ ∗ // wk ↑⋆ (suc k) ++
σ₂ ∗ // wk ↑⋆ (suc k)) // sub (σ / wk ↑⋆ k) ≡⟨ cong (λ σs → σs // sub (σ / wk ↑⋆ k)) $
sym $ map-++-commute
(λ σ → σ / wk ↑⋆ suc k) (σ₁ ∗) (σ₂ ∗) ⟩
(σ₁ ∗ ++ σ₂ ∗) // wk ↑⋆ (suc k) // sub (σ / wk ↑⋆ k) ≡⟨ sym $ //.sub-commutes (σ₁ ∗ ++ σ₂ ∗) ⟩
(σ₁ ∗ ++ σ₂ ∗) // sub σ // wk ↑⋆ k ∎
wk-∗′-commute k (var x) = begin
var x / wk ↑⋆ k ∗′ ≡⟨ cong _∗′ (var-/-wk-↑⋆ k x) ⟩
var (lift k suc x) ∗′ ≡⟨ refl ⟩
[] ⊆⟨ (λ ()) ⟩
var x ∗′ // wk ↑⋆ k ∎
wk-∗′-commute k ⊥ = λ ()
wk-∗′-commute k ⊤ = λ ()
sub-∗′-commute-var : ∀ k {n} x (τ : Ty n) →
var x / sub τ ↑⋆ k ∗′ ⊆ τ ∗ // wk⋆ k
sub-∗′-commute-var zero zero τ = begin
τ ∗′ ⊆⟨ there ⟩
τ ∗ ≡⟨ sym $ //.id-vanishes (τ ∗) ⟩
τ ∗ // wk⋆ zero ∎
sub-∗′-commute-var zero (suc x) τ = begin
var x / idˢ ∗′ ≡⟨ cong _∗′ (id-vanishes (var x)) ⟩
var x ∗′ ≡⟨ refl ⟩
[] ⊆⟨ (λ ()) ⟩
τ ∗ // wk⋆ zero ∎
sub-∗′-commute-var (suc k) zero τ = begin
[] ⊆⟨ (λ ()) ⟩
τ ∗ // wk⋆ (suc k) ∎
sub-∗′-commute-var (suc k) (suc x) τ = begin
var (suc x) / sub τ ↑⋆ suc k ∗′ ≡⟨ cong _∗′ (suc-/-↑ x) ⟩
var x / sub τ ↑⋆ k / wk ∗′ ⊆⟨ wk-∗′-commute zero (var x / sub τ ↑⋆ k) ⟩
var x / sub τ ↑⋆ k ∗′ // wk ⊆⟨ map-mono _ (sub-∗′-commute-var k x τ) ⟩
τ ∗ // wk⋆ k // wk ≡⟨ sym $ //./-weaken (τ ∗) ⟩
τ ∗ // wk⋆ (suc k) ∎
sub-∗-commute : ∀ k {n} σ (τ : Ty n) →
σ / sub τ ↑⋆ k ∗ ⊆ σ ∗ // sub τ ↑⋆ k ++ τ ∗ // wk⋆ k
sub-∗-commute k σ τ (here refl) = here refl
sub-∗-commute k ⊥ τ •∈• = Inverse.to ++⇿ ⟨$⟩ inj₁ •∈•
sub-∗-commute k ⊤ τ •∈• = Inverse.to ++⇿ ⟨$⟩ inj₁ •∈•
sub-∗-commute k (var x) τ (there •∈•) = there $ sub-∗′-commute-var k x τ •∈•
sub-∗-commute k (σ₁ ⟶ σ₂) τ {χ} (there •∈•) = there $
χ ∈⟨ •∈• ⟩
(σ₁ / ρ) ∗ ++ (σ₂ / ρ) ∗ ⊆⟨ sub-∗-commute k σ₁ τ ++-mono
sub-∗-commute k σ₂ τ ⟩
(σ₁ ∗ // ρ ++ τ ∗ // wk⋆ k) ++
(σ₂ ∗ // ρ ++ τ ∗ // wk⋆ k) ≈⟨ ++-lemma (σ₁ ∗ // ρ) (σ₂ ∗ // ρ) ⟩
(σ₁ ∗ // ρ ++ σ₂ ∗ // ρ) ++
τ ∗ // wk⋆ k ≡⟨ cong₂ _++_
(sym $ map-++-commute (λ σ → σ / ρ) (σ₁ ∗) (σ₂ ∗))
refl ⟩
(σ₁ ∗ ++ σ₂ ∗) // ρ ++ τ ∗ // wk⋆ k ∎
where ρ = sub τ ↑⋆ k
sub-∗-commute k (μ σ₁ ⟶ σ₂) τ (there (here refl)) =
there $ here $ sym $ sub-commutes (σ₁ ⟶ σ₂)
sub-∗-commute k (μ σ₁ ⟶ σ₂) τ {χ} (there (there •∈•)) = there $ there $
χ ∈⟨ •∈• ⟩
((σ₁ / ρ ↑) ∗ ++ (σ₂ / ρ ↑) ∗) // sub (σ / ρ) ⊆⟨ map-mono _ (begin
(σ₁ / ρ ↑) ∗ ++ (σ₂ / ρ ↑) ∗ ⊆⟨ sub-∗-commute (suc k) σ₁ τ ++-mono
sub-∗-commute (suc k) σ₂ τ ⟩
(σ₁ ∗ // ρ ↑ ++ τ ∗ // wk⋆ (suc k)) ++
(σ₂ ∗ // ρ ↑ ++ τ ∗ // wk⋆ (suc k)) ≈⟨ ++-lemma (σ₁ ∗ // ρ ↑) (σ₂ ∗ // ρ ↑) ⟩
(σ₁ ∗ // ρ ↑ ++ σ₂ ∗ // ρ ↑) ++
τ ∗ // wk⋆ (suc k) ≡⟨ cong₂ _++_
(sym $ map-++-commute
(λ σ → σ / ρ ↑) (σ₁ ∗) (σ₂ ∗))
refl ⟩
(σ₁ ∗ ++ σ₂ ∗) // ρ ↑ ++
τ ∗ // wk⋆ (suc k) ∎) ⟩
((σ₁ ∗ ++ σ₂ ∗) // ρ ↑ ++
τ ∗ // wk⋆ (suc k)) // sub (σ / ρ) ≡⟨ map-++-commute (λ χ → χ / sub (σ / ρ))
((σ₁ ∗ ++ σ₂ ∗) // ρ ↑) _ ⟩
(σ₁ ∗ ++ σ₂ ∗) // ρ ↑ // sub (σ / ρ) ++
τ ∗ // wk⋆ (suc k) // sub (σ / ρ) ≡⟨ cong₂ _++_
(sym $ //.sub-commutes (σ₁ ∗ ++ σ₂ ∗))
lem ⟩
(σ₁ ∗ ++ σ₂ ∗) // sub σ // ρ ++
τ ∗ // wk⋆ k ∎
where
ρ = sub τ ↑⋆ k
σ = μ σ₁ ⟶ σ₂
lem = begin′
τ ∗ // wk⋆ (suc k) // sub (σ / ρ) ≡⟨ cong₂ _//_ (//./-weaken (τ ∗)) refl ⟩′
τ ∗ // wk⋆ k // wk // sub (σ / ρ) ≡⟨ //.wk-sub-vanishes (τ ∗ // wk⋆ k) ⟩′
τ ∗ // wk⋆ k ∎′
where open ≡-Reasoning
renaming (begin_ to begin′_; _≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′)
complete : ∀ {n} {σ τ : Ty n} → σ ⊑ τ → σ ∈ τ ∗
complete refl = here refl
complete (⟶ˡ σ⊑τ₁) = there (Inverse.to ++⇿ ⟨$⟩ inj₁ (complete σ⊑τ₁))
complete (⟶ʳ σ⊑τ₂) = there (Inverse.to (++⇿ {xs = _ ∗}) ⟨$⟩ inj₂ (complete σ⊑τ₂))
complete (unfold {σ} {τ₁} {τ₂} σ⊑) =
σ ∈⟨ complete σ⊑ ⟩
unfold[μ τ₁ ⟶ τ₂ ] ∗ ⊆⟨ sub-∗-commute zero (τ₁ ⟶ τ₂) τ ⟩
τ₁ ⟶ τ₂ ∗ // sub τ ++ τ ∗ // idˢ ≡⟨ cong (_++_ (τ₁ ⟶ τ₂ ∗ // sub τ))
(//.id-vanishes (τ ∗)) ⟩
τ ∗′ ++ τ ∗ ⊆⟨ there {x = τ} {xs = τ ∗′} ++-mono id ⟩
τ ∗ ++ τ ∗ ≈⟨ ++-idempotent (τ ∗) ⟩
τ ∗ ∎
where τ = μ τ₁ ⟶ τ₂
subtermsOf : ∀ {n} (τ : Ty n) → List (∃ λ σ → σ ⊑ τ)
subtermsOf τ = map-with-∈ (τ ∗) (,_ ∘′ sound τ)
subtermsOf-complete : ∀ {n} {σ τ : Ty n} →
σ ⊑ τ → ∃ λ σ⊑τ → (σ , σ⊑τ) ∈ subtermsOf τ
subtermsOf-complete {σ = σ} {τ} σ⊑τ =
(, Inverse.to (map-with-∈⇿ {f = ,_ ∘′ sound τ}) ⟨$⟩
(σ , complete σ⊑τ , refl))