------------------------------------------------------------------------
-- 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 using (here; there)
open import Data.List.Any.BagAndSetEquality as BSEq
open import Data.List.Any.Membership.Propositional
open import Data.List.Any.Membership.Propositional.Properties
open import Data.List.Any.Properties
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (module Inverse)
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
import Relation.Binary.PropositionalEquality as P
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 $ P.subst  χ  σ / ρ  χ)
                   (sub-commutes (τ₁  τ₂))
                   (/-monoˡ σ⊑)

sub-⊑-μ :  {n} {σ : Ty (suc n)} {τ₁ τ₂} 
          σ  τ₁  τ₂  σ / sub (μ τ₁  τ₂)  μ τ₁  τ₂
sub-⊑-μ σ⊑τ₁⟶τ₂ = unfold (/-monoˡ σ⊑τ₁⟶τ₂)

-- All list elements are subterms.

sound :  {n σ} (τ : Ty n)  σ  τ   σ  τ
sound τ         (here P.refl) = refl
sound (τ₁  τ₂) (there σ∈)    =
  [ ⟶ˡ  sound τ₁ , ⟶ʳ  sound τ₂ ]′
    (Inverse.from (++↔ {xs = τ₁ }) ⟨$⟩ σ∈)
sound (μ τ₁  τ₂) (there (here P.refl)) = unfold refl
sound (μ τ₁  τ₂) (there (there σ∈))
  with Inverse.from (map-∈↔ {f = λ σ  σ / sub (μ τ₁  τ₂)}
                            {xs = τ₁  ++ τ₂ }) ⟨$⟩ σ∈
... | (χ , χ∈ , P.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 P.refl) = here P.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 ∗′                ≡⟨ P.refl 
    σ₁ / wk ↑⋆ k  ++ σ₂ / wk ↑⋆ k     ⊆⟨ wk-∗-commute k σ₁ ++-mono
                                           wk-∗-commute k σ₂ 
    σ₁  // wk ↑⋆ k ++ σ₂  // wk ↑⋆ k  ≡⟨ P.sym $ map-++-commute
                                              σ  σ / wk ↑⋆ k) (σ₁ ) (σ₂ ) 
    (σ₁  ++ σ₂ ) // wk ↑⋆ k           ≡⟨ P.refl 
    σ₁  σ₂ ∗′ // wk ↑⋆ k               
  wk-∗′-commute k (μ σ₁  σ₂) = begin
    (μ σ₁  σ₂) / wk ↑⋆ k ∗′                          ≡⟨ P.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              ≡⟨ P.refl 
    μ σ₁  σ₂ ∗′ // wk ↑⋆ k                           
    where
    σ = μ σ₁  σ₂

    lem₁ : _  _
    lem₁ = begin
      [ σ₁  σ₂ / wk ↑⋆ (suc k) / sub (σ / wk ↑⋆ k) ]  ≡⟨ P.cong [_] $ P.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)          ≡⟨ P.cong  σs  σs // sub (σ / wk ↑⋆ k)) $
                                                                 P.sym $ map-++-commute
                                                                    σ  σ / wk ↑⋆ suc k) (σ₁ ) (σ₂ ) 
      (σ₁  ++ σ₂ ) // wk ↑⋆ (suc k) // sub (σ / wk ↑⋆ k)  ≡⟨ P.sym $ //.sub-commutes (σ₁  ++ σ₂ ) 
      (σ₁  ++ σ₂ ) // sub σ // wk ↑⋆ k                    
  wk-∗′-commute k (var x) = begin
    var x / wk ↑⋆ k ∗′     ≡⟨ P.cong _∗′ (var-/-wk-↑⋆ k x) 
    var (lift k suc x) ∗′  ≡⟨ P.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 
  τ               ≡⟨ P.sym $ //.id-vanishes (τ ) 
  τ  // wk⋆ zero  
sub-∗′-commute-var zero (suc x) τ = begin
  var x / idˢ ∗′   ≡⟨ P.cong _∗′ (id-vanishes (var x)) 
  var x ∗′         ≡⟨ P.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 ∗′         ≡⟨ P.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                      ≡⟨ P.sym $ //./-weaken (τ ) 
  τ  // wk⋆ (suc k)                      

sub-∗-commute :  k {n} σ (τ : Ty n) 
                σ / sub τ ↑⋆ k   σ  // sub τ ↑⋆ k ++ τ  // wk⋆ k
sub-∗-commute k σ         τ     (here P.refl) = here P.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                         ≡⟨ P.cong₂ _++_
                                            (P.sym $ map-++-commute  σ  σ / ρ) (σ₁ ) (σ₂ ))
                                            P.refl 
  (σ₁  ++ σ₂ ) // ρ ++ τ  // wk⋆ k  
  where ρ = sub τ ↑⋆ k
sub-∗-commute k (μ σ₁  σ₂) τ (there (here P.refl)) =
  there $ here $ P.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)                              ≡⟨ P.cong₂ _++_
                                                           (P.sym $ map-++-commute
                                                                       σ  σ / ρ ) (σ₁ ) (σ₂ ))
                                                           P.refl 
      (σ₁  ++ σ₂ ) // ρ  ++
      τ  // wk⋆ (suc k)                              ) 
  ((σ₁  ++ σ₂ ) // ρ  ++
   τ  // wk⋆ (suc k)) // sub (σ / ρ)            ≡⟨ map-++-commute  χ  χ / sub (σ / ρ))
                                                                   ((σ₁  ++ σ₂ ) // ρ ) _ 
  (σ₁  ++ σ₂ ) // ρ  // sub (σ / ρ) ++
  τ  // wk⋆ (suc k) // sub (σ / ρ)              ≡⟨ P.cong₂ _++_
                                                      (P.sym $ //.sub-commutes (σ₁  ++ σ₂ ))
                                                      lem 
  (σ₁  ++ σ₂ ) // sub σ // ρ ++
  τ  // wk⋆ k                                   
  where
  ρ = sub τ ↑⋆ k
  σ = μ σ₁  σ₂

  lem = begin′
    τ  // wk⋆ (suc k) // sub (σ / ρ)  ≡⟨ P.cong₂ _//_ (//./-weaken (τ )) P.refl ⟩′
    τ  // wk⋆ k // wk // sub (σ / ρ)  ≡⟨ //.wk-sub-vanishes (τ  // wk⋆ k) ⟩′
    τ  // wk⋆ k                       ∎′
    where open P.≡-Reasoning
            renaming (begin_ to begin′_; _≡⟨_⟩_ to _≡⟨_⟩′_; _∎ to _∎′)

-- The list contains all subterms.

complete :  {n} {σ τ : Ty n}  σ  τ  σ  τ 
complete refl                      = here P.refl
complete (⟶ˡ σ⊑τ₁)                 = there (Inverse.to ++↔                            ⟨$⟩ inj₁ (complete σ⊑τ₁))
complete (⟶ʳ σ⊑τ₂)                 = there (Inverse.to (++↔ {P = P._≡_ _} {xs = _ }) ⟨$⟩ inj₂ (complete σ⊑τ₂))
complete (unfold {σ} {τ₁} {τ₂} σ⊑) =
  σ                                 ∈⟨ complete σ⊑ 
  unfold[μ τ₁  τ₂ ]               ⊆⟨ sub-∗-commute zero (τ₁  τ₂) τ 
  τ₁  τ₂  // sub τ ++ τ  // idˢ  ≡⟨ P.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 σ⊑τ , P.refl))