------------------------------------------------------------------------
-- Brandt and Henglein's subterm relation
------------------------------------------------------------------------

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 (_//_)

------------------------------------------------------------------------
-- Subterms

-- The subterm relation.

infix 4 _⊑_

data _⊑_ {n} : Ty n  Ty n  Set where
  refl   :  {τ}  τ  τ
  unfold :  {σ τ₁ τ₂} (σ⊑ : σ  unfold[μ τ₁  τ₂ ])  σ  μ τ₁  τ₂
  ⟶ˡ     :  {σ τ₁ τ₂} (σ⊑τ₁ : σ  τ₁)  σ  τ₁  τ₂
  ⟶ʳ     :  {σ τ₁ τ₂} (σ⊑τ₂ : σ  τ₂)  σ  τ₁  τ₂

-- Some simple consequences.

unfold′ :  {n} {τ₁ τ₂ : Ty (suc n)} 
          unfold[μ τ₁  τ₂ ]  μ τ₁  τ₂
unfold′ = unfold refl

⟶ˡ′ :  {n} {τ₁ τ₂ : Ty n}  τ₁  τ₁  τ₂
⟶ˡ′ = ⟶ˡ refl

⟶ʳ′ :  {n} {τ₁ τ₂ : Ty n}  τ₂  τ₁  τ₂
⟶ʳ′ = ⟶ʳ refl

-- The subterm relation is transitive.

trans :  {n} {σ τ χ : Ty n} 
        σ  τ  τ  χ  σ  χ
trans σ⊑τ refl        = σ⊑τ
trans σ⊑τ (unfold τ⊑) = unfold (trans σ⊑τ τ⊑)
trans σ⊑τ (⟶ˡ τ⊑δ₁)   = ⟶ˡ (trans σ⊑τ τ⊑δ₁)
trans σ⊑τ (⟶ʳ τ⊑δ₂)   = ⟶ʳ (trans σ⊑τ τ⊑δ₂)

------------------------------------------------------------------------
-- Subterm closure

-- The list τ_∗ contains exactly the subterms of τ (possibly with
-- duplicates).
--
-- The important property is completeness, which ensures that the
-- number of distinct subterms of a given type is always finite.

mutual

  infix 7 _∗ _∗′

  _∗ :  {n}  Ty n  List (Ty n)
  τ  = τ  τ ∗′

  _∗′ :  {n}  Ty n  List (Ty n)
  (τ₁  τ₂)   ∗′ = τ₁  ++ τ₂ 
  (μ τ₁  τ₂) ∗′ = (τ₁  τ₂  τ₁  ++ τ₂ ) // sub (μ τ₁  τ₂)
  τ           ∗′ = []

------------------------------------------------------------------------
-- Soundness

-- _/_ is monotonous in its left argument.

/-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ˡ σ⊑τ₁⟶τ₂)

-- All list elements are subterms.

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 ())

------------------------------------------------------------------------
-- Completeness

++-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

  -- Weakening "commutes" with _∗.

  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  = λ ()

-- Substitution "commutes" with _∗.

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 _∎′)

-- The list contains all subterms.

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 τ = μ τ₁  τ₂

------------------------------------------------------------------------
-- A wrapper function

-- Pairs up subterms with proofs.

subtermsOf :  {n} (τ : Ty n)  List ( λ σ  σ  τ)
subtermsOf τ = map-with-∈ (τ ) (,_ ∘′ sound τ)

-- subtermsOf is complete.

subtermsOf-complete :  {n} {σ τ : Ty n} 
                      σ  τ   λ σ⊑τ  (σ , σ⊑τ)  subtermsOf τ
subtermsOf-complete {σ = σ} {τ} σ⊑τ =
  (, Inverse.to (map-with-∈⇿ {f = ,_ ∘′ sound τ}) ⟨$⟩
       (σ , complete σ⊑τ , refl))