open import RecursiveTypes.Syntax
module RecursiveTypes.Subterm.RestrictedHypothesis
{n} (χ₁ χ₂ : Ty n) where
open import Category.Monad
open import Data.Function
open import Data.List as List
open RawMonad List.monad
open import Data.List.Any as Any
open Membership-≡ using (_∈_)
import Data.List.Any.Properties as AnyP
open AnyP.Membership-≡
import Data.List.Countdown as Countdown
open import Data.Product as Prod
open import Data.Sum as Sum
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.On as On
open import Relation.Binary.PropositionalEquality as PropEq
open import RecursiveTypes.Subterm as ST using (_⊑_; _∗)
Subterm : Ty n → Set
Subterm σ = σ ⊑ χ₁ ⊎ σ ⊑ χ₂
anti-mono : ∀ {σ₁ σ₂} → σ₂ ⊑ σ₁ → Subterm σ₁ → Subterm σ₂
anti-mono σ₂⊑σ₁ = Sum.map (ST.trans σ₂⊑σ₁) (ST.trans σ₂⊑σ₁)
RestrictedHyp : Set
RestrictedHyp = ∃ Subterm × ∃ Subterm
⟨_⟩ : RestrictedHyp → Hyp n
⟨_⟩ = Prod.map proj₁ proj₁
⟨_⟩⋆ : List RestrictedHyp → List (Hyp n)
⟨_⟩⋆ = List.map ⟨_⟩
_≈_ : Rel RestrictedHyp
_≈_ = _≡_ on₁ ⟨_⟩
open Membership
(record { isEquivalence =
On.isEquivalence ⟨_⟩ PropEq.isEquivalence })
using () renaming (_∈_ to _⟨∈⟩_)
subtermsOf : ∀ τ → (∀ {σ} → σ ⊑ τ → Subterm σ) → List (∃ Subterm)
subtermsOf τ f = List.map (Prod.map id f) (ST.subtermsOf τ)
subtermsOf-complete :
∀ {τ} (f : ∀ {σ} → σ ⊑ τ → Subterm σ) {σ} →
σ ⊑ τ → ∃ λ σ⊑τ → (σ , f σ⊑τ) ∈ subtermsOf τ f
subtermsOf-complete f σ⊑τ =
Prod.map id map-∈⁺ $ ST.subtermsOf-complete σ⊑τ
subtermsOf²-complete :
∀ {σ₁ τ₁ σ₂ τ₂}
(f : ∀ {σ} → σ ⊑ τ₁ → Subterm σ)
(g : ∀ {σ} → σ ⊑ τ₂ → Subterm σ) →
(σ₁⊑τ₁ : σ₁ ⊑ τ₁) (σ₂⊑τ₂ : σ₂ ⊑ τ₂) →
((σ₁ , f σ₁⊑τ₁) ≲ (σ₂ , g σ₂⊑τ₂)) ⟨∈⟩
(subtermsOf τ₁ f ⊗ subtermsOf τ₂ g)
subtermsOf²-complete f g σ₁⊑τ₁ σ₂⊑τ₂ =
Any.map (cong $ Prod.map proj₁ proj₁) $
⊗-∈⁺ (proj₂ $ subtermsOf-complete f σ₁⊑τ₁)
(proj₂ $ subtermsOf-complete g σ₂⊑τ₂)
⊑-χ₁ : List (∃ Subterm)
⊑-χ₁ = subtermsOf χ₁ inj₁
⊑-χ₂ : List (∃ Subterm)
⊑-χ₂ = subtermsOf χ₂ inj₂
restrictedHyps : List RestrictedHyp
restrictedHyps = (⊑-χ₁ ⊗ ⊑-χ₂) ++ (⊑-χ₂ ⊗ ⊑-χ₁) ++
(⊑-χ₁ ⊗ ⊑-χ₁) ++ (⊑-χ₂ ⊗ ⊑-χ₂)
complete : ∀ h → h ⟨∈⟩ restrictedHyps
complete ((σ , inj₁ σ⊑χ₁) ≲ (τ , inj₂ τ⊑χ₂)) =
AnyP.++⁺ˡ $
subtermsOf²-complete inj₁ inj₂ σ⊑χ₁ τ⊑χ₂
complete ((σ , inj₂ σ⊑χ₂) ≲ (τ , inj₁ τ⊑χ₁)) =
AnyP.++⁺ʳ (⊑-χ₁ ⊗ ⊑-χ₂) $
AnyP.++⁺ˡ $
subtermsOf²-complete inj₂ inj₁ σ⊑χ₂ τ⊑χ₁
complete ((σ , inj₁ σ⊑χ₁) ≲ (τ , inj₁ τ⊑χ₁)) =
AnyP.++⁺ʳ (⊑-χ₁ ⊗ ⊑-χ₂) $
AnyP.++⁺ʳ (⊑-χ₂ ⊗ ⊑-χ₁) $
AnyP.++⁺ˡ $
subtermsOf²-complete inj₁ inj₁ σ⊑χ₁ τ⊑χ₁
complete ((σ , inj₂ σ⊑χ₂) ≲ (τ , inj₂ τ⊑χ₂)) =
AnyP.++⁺ʳ (⊑-χ₁ ⊗ ⊑-χ₂) $
AnyP.++⁺ʳ (⊑-χ₂ ⊗ ⊑-χ₁) $
AnyP.++⁺ʳ (⊑-χ₁ ⊗ ⊑-χ₁) $
subtermsOf²-complete inj₂ inj₂ σ⊑χ₂ τ⊑χ₂
_≟_ : Decidable (_≡_ {Hyp n})
( σ₁ ≲ σ₂) ≟ (τ₁ ≲ τ₂) with σ₁ ≡? τ₁ | σ₂ ≡? τ₂
(.τ₁ ≲ .τ₂) ≟ (τ₁ ≲ τ₂) | yes refl | yes refl = yes refl
... | no σ₁≢τ₁ | _ = no (σ₁≢τ₁ ∘ cong proj₁)
... | _ | no σ₂≢τ₂ = no (σ₂≢τ₂ ∘ cong proj₂)
isDecEquivalence : IsDecEquivalence _≈_
isDecEquivalence =
On.isDecEquivalence ⟨_⟩ $
DecSetoid.isDecEquivalence (PropEq.decSetoid _≟_)
private
open module C =
Countdown (record { isDecEquivalence = isDecEquivalence })
public hiding (empty; emptyFromList)
empty : [] ⊕ length restrictedHyps
empty = C.emptyFromList restrictedHyps complete