test1.agda

module test1 where
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong₂) public


data List (A : Set) : Set where
  ∅   : List A
  _,_ : List A → A → List A
infixl 10 _,_

data _⊆_ {A} : List A → List A → Set where
  stop : ∀ {Γ} → Γ ⊆ Γ
  skip : ∀ {Γ Γ' A} → Γ ⊆ Γ' → Γ ⊆ Γ' , A
  keep : ∀ {Γ Γ' A} → Γ ⊆ Γ' → Γ , A ⊆ Γ' , A
infix 8 _⊆_


cong⊆₁ : ∀ {A} {L₁ L₁' L₂ : List A} → L₁ ⊆ L₂ → L₁ ≡ L₁' → L₁' ⊆ L₂
cong⊆₁ p refl = p

trans⊆ : ∀ {A} {Γ Γ' Γ'' : List A} → Γ ⊆ Γ' → Γ' ⊆ Γ'' → Γ ⊆ Γ''
trans⊆ e₁ stop             = e₁
trans⊆ e₁ (skip e₂)        = skip (trans⊆ e₁ e₂)
trans⊆ stop (keep e₂)      = keep e₂
trans⊆ (skip e₁) (keep e₂) = skip (trans⊆ e₁ e₂)
trans⊆ (keep e₁) (keep e₂) = keep (trans⊆ e₁ e₂)


-- List concatenation.
_⧺_ : ∀ {A} → List A → List A → List A
Γ ⧺ ∅     = Γ
Γ ⧺ Δ , A = (Γ ⧺ Δ) , A
infixl 9 _⧺_

assoc⧺ : ∀ {A} {L₁ L₂ L₃ : List A} → L₁ ⧺ (L₂ ⧺ L₃) ≡ (L₁ ⧺ L₂) ⧺ L₃
assoc⧺ {L₃ = ∅}      = refl
assoc⧺ {L₃ = xs , x} = cong₂ _,_ (assoc⧺ {L₃ = xs}) refl

unit⧺ₗ : ∀ {A} {L : List A} → ∅ ⧺ L ≡ L
unit⧺ₗ {L = ∅}      = refl
unit⧺ₗ {L = xs , x} = cong₂ _,_ (unit⧺ₗ {L = xs}) refl

⧺-⊆-dist : ∀ {A} {L₁ L₁' L₂ L₂' : List A} → L₁ ⊆ L₁' → L₂ ⊆ L₂' → L₁ ⧺ L₂ ⊆ L₁' ⧺ L₂'
⧺-⊆-dist stop stop     = stop
⧺-⊆-dist {L₂           = L₂} (skip γ) stop = {!!} --trans⊆ (⧺-⊆-dist γ stop) (⧺-⊆-dist (skip stop) stop)
⧺-⊆-dist (keep γ) stop = {!⧺-⊆-dist γ stop!}
⧺-⊆-dist γ (skip δ)    = skip (⧺-⊆-dist γ δ)
⧺-⊆-dist γ (keep δ)    = keep (⧺-⊆-dist γ δ)

⧺-⊆₁ : ∀ {A} {L₁ L₂ : List A} → L₁ ⊆ (L₁ ⧺ L₂)
⧺-⊆₁ {L₂ = ∅}      = stop
⧺-⊆₁ {L₂ = xs , x} = skip (⧺-⊆₁ {L₂ = xs})

⧺-⊆₂ : ∀ {A} {L₁ L₂ : List A} → L₂ ⊆ (L₁ ⧺ L₂)
⧺-⊆₂ {L₁ = ∅}           = cong⊆₁ stop unit⧺ₗ
⧺-⊆₂ {L₁ = xs , x} {L₂} = {!⧺-⊆₂ {L₁ = xs}!} --trans⊆ (⧺-⊆₂ {L₁ = xs}) (⧺-⊆-dist {L₁ = xs} {L₂ = L₂} (skip stop) stop)