From aff2a0367ad2a9e675da29c185663a45631917f8 Mon Sep 17 00:00:00 2001
From: Ewen Broudin-Caradec <ewen.broudin--caradec@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 18:07:06 +0100
Subject: [PATCH] Dependant Injectivity

---
 src/Agda/Core/Syntax.agda      |  4 +++
 src/Agda/Core/Unification.agda | 57 +++++++++++++++++++++++++++++++---
 2 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/src/Agda/Core/Syntax.agda b/src/Agda/Core/Syntax.agda
index a344e59..3fe6673 100644
--- a/src/Agda/Core/Syntax.agda
+++ b/src/Agda/Core/Syntax.agda
@@ -368,6 +368,10 @@ revIdSubst : {@0 α : Scope Name} → Rezz α → α ⇒ ~ α
 revIdSubst {α} r = subst0 (λ s →  s ⇒ (~ α)) (revsInvolution α) (revSubst (idSubst (rezz~ r)))
 {-# COMPILE AGDA2HS revIdSubst #-}
 
+revIdSubst' : {@0 α : Scope Name} → Rezz α → ~ α ⇒ α
+revIdSubst' {α} r = subst0 (λ s →  (~ α) ⇒ s) (revsInvolution α) (revIdSubst (rezz~ r))
+{-# COMPILE AGDA2HS revIdSubst' #-}
+
 raise : {@0 α β : Scope Name} → Rezz α → Term β → Term (α <> β)
 raise r = weakenTerm (subJoinDrop r subRefl)
 {-# COMPILE AGDA2HS raise #-}
diff --git a/src/Agda/Core/Unification.agda b/src/Agda/Core/Unification.agda
index 4ffaaf0..ceb1a0a 100644
--- a/src/Agda/Core/Unification.agda
+++ b/src/Agda/Core/Unification.agda
@@ -212,9 +212,9 @@ open TelescopeEq
                           {- PART THREE : Unification Step By Step -}
 ---------------------------------------------------------------------------------------------------
 private variable
-  @0 e₀ : Name
+  @0 e₀ e₁ : Name
   @0 α α' β β' : Scope Name
-  δ₁ δ₂ : α ⇒ β
+  δ₁ δ₂ : β ⇒ α
   ds : Sort α
 
 data UnificationStep (Γ : Context α) : TelescopicEq α β → Context α' → TelescopicEq α' β' → Set
@@ -258,7 +258,7 @@ data UnificationStep {α = α} Γ where
     {pSubst : dataParScope d ⇒ α}                                              -- value of the parameters of d
     {iSubst : dataIxScope d ⇒ α}                                               -- value of the indices of d
     {Δe₀ : Telescope (e₀ ◃ α) β}
-    { (⟨ c₀ ⟩ cFromd) : NameIn (dataConstructorScope dt)}                      -- c is a constructor of dt
+    ( (⟨ c₀ ⟩ cFromd) : NameIn (dataConstructorScope dt))                      -- c is a constructor of dt
     (let cFromCon , con = dataConstructors dt (⟨ c₀ ⟩ cFromd)
          c = (⟨ c₀ ⟩ cFromCon)                                                 -- c is a constructor of a datatype
          γ : Scope Name
@@ -276,4 +276,53 @@ data UnificationStep {α = α} Γ where
          Δγ = subst τ Δe₀)
     ------------------------------------------------------------------- ⚠ NOT a rewrite rule ⚠ (c = (⟨ c₀ ⟩ cFromCon))
     → Γ , ⌈ e₀ ↦ TCon c σ₁ ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ TCon c σ₂ ◃ δ₂ ⌉ ∶ ⌈ e₀ ∶ El ds (TData d pSubst iSubst) ◃ Δe₀ ⌉
-      ↣ᵤ Γ , concatSubst σ₁ δ₁ ≟ concatSubst σ₂ δ₂ ∶ addTel Σ Δγ
\ No newline at end of file
+      ↣ᵤ Γ , concatSubst σ₁ δ₁ ≟ concatSubst σ₂ δ₂ ∶ addTel Σ Δγ
+
+ {- solve equalities of the form c i = c j for a constructor c of a datatype d -}
+  InjectivityDep :
+    {- from β = ixs <> (e₀ ◃ β₀) to β' = γ <> β₀ -}
+    {β₀ : Scope Name}
+    {δ₁ δ₂ : β₀ ⇒ α}
+    {d : NameIn dataScope}                                                     -- the datatype
+    (let dt = sigData sig d
+         pars = dataParScope d
+         ixs = dataIxScope d)
+    {ds : Sort (~ ixs <> α)}
+    {pSubst : pars ⇒ α}                                                        -- value of the parameters of d
+    {iSubst₁ iSubst₂ : ixs ⇒ α}                                                -- value of the indices of d
+    {Δe₀ixs : Telescope (e₀ ◃ (~ ixs <>  α)) β₀}
+    { (⟨ c₀ ⟩ cFromd) : NameIn (dataConstructorScope dt)}                      -- c is a constructor of dt
+    (let cFromCon , con = dataConstructors dt (⟨ c₀ ⟩ cFromd)
+         c = (⟨ c₀ ⟩ cFromCon)                                                 -- c is a constructor of a datatype
+         γ : Scope Name
+         γ = fieldScope c)                                                     -- name of the arguments of c
+    {σ₁ σ₂ : γ ⇒ α}
+    (let Σ : Telescope α γ
+         Σ = subst pSubst (conTelescope con)                                   -- type of the arguments of c
+
+         iTel : Telescope α ixs
+         iTel = subst pSubst (dataIndexTel dt)
+
+         iSubste : ixs ⇒ (~ ixs <> α)
+         iSubste = weakenSubst (subJoinHere (rezz _) subRefl) (revIdSubst (rezz ixs))
+         weakenα : α ⇒ (~ ixs <> α)
+         weakenα = weaken (subJoinDrop (rezz _) subRefl) (idSubst (rezz α))
+
+         σe : γ ⇒ (~ γ <> α)
+         σe = weaken (subJoinHere (rezz _) subRefl) (revIdSubst (rezz γ))
+         τ₀ : [ e₀ ] ⇒ (~ γ <> α)
+         τ₀ = subst0 (λ ξ₀ → ξ₀ ⇒ (~ γ <> α)) (rightIdentity _) ⌈ e₀ ↦ TCon c σe ◃ ⌈⌉ ⌉
+         τ₁ : ~ ixs ⇒ (~ γ <> α)
+         τ₁ = subst (subst (liftSubst (rezz _) pSubst) (conIndices con)) (revIdSubst' (rezz _))
+         τ₂ : α ⇒ (~ γ <> α)
+         τ₂ = weaken (subJoinDrop (rezz _) subRefl) (idSubst (rezz α))
+         τ : (e₀ ◃ (~ ixs <>  α)) ⇒ (~ γ <> α)
+         τ = concatSubst τ₀ (concatSubst τ₁ τ₂)
+         Δγ : Telescope (~ γ <> α) β₀
+         Δγ = substTelescope τ Δe₀ixs)
+    ------------------------------------------------------------------- ⚠ NOT a rewrite rule ⚠
+    → Γ , concatSubst iSubst₁ ⌈ e₀ ↦ TCon c σ₁ ◃ δ₁ ⌉ ≟ concatSubst iSubst₂ ⌈ e₀ ↦ TCon c σ₂ ◃ δ₂ ⌉
+          ∶ addTel iTel ⌈ e₀ ∶ El ds (TData d (subst weakenα pSubst) iSubste) ◃ Δe₀ixs ⌉
+      ↣ᵤ Γ , concatSubst σ₁ δ₁ ≟ concatSubst σ₂ δ₂ ∶ addTel Σ Δγ
+{- End of module UnificationStep -}
+