module DepEq

-- https://mathstodon.xyz/@MartinEscardo/114751459092567654
-- see also https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html

infixr 5 _≡_
infixl 6 _+_
infixl 6 _++_
infixr 7 _::_
infixr 5 _≡⟨_⟩_

data _≡_ : ∀ a. a → a → U where
  Refl : ∀ a. {x : a} → x ≡ x

cong : ∀ X Y. (f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
cong f Refl = Refl

data ℕ : U where
  S : ℕ → ℕ
  Z : ℕ

_+_ : ℕ → ℕ → ℕ
Z + m = m
S k + m = S (k + m)

+-assoc : (l m n : ℕ ) → l + (m + n) ≡ (l + m) + n
+-assoc Z m n = Refl
+-assoc (S k) m n = cong S (+-assoc k m n)



_≡⟨_⟩_ : {0 A : U} → {0 B : A → U } →  {0 x₀ x₁ : A} → B x₀ → x₀ ≡ x₁ → B x₁ → U
b₀ ≡⟨ Refl ⟩ b₁ = b₀ ≡ b₁

congd : {0 A : U} → {0 B : A → U} → (f : (a : A) → B a) → {0 a₀ a₁ : A} →
        (p : a₀ ≡ a₁) →
        _≡⟨_⟩_ {_} {B} (f a₀) p (f a₁)
congd f Refl = Refl

data Vect : U → ℕ → U where
  Nil : ∀ a. Vect a Z
  _::_ : ∀ a n . a → Vect a n → Vect a (S n)

_++_ : ∀ a n m. Vect a n → Vect a m → Vect a (n + m)
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

-- REVIEW - make sure we're freezing metas at the end of a typesig / def
cong-cons : ∀ a n m.  (x : a) → {xs : Vect a n} → {ys : Vect a m} → (p : n ≡ m) →
            _≡⟨_⟩_ {_} {Vect a} xs p ys → _≡⟨_⟩_ {_} {Vect a} (x :: xs) (cong S p) (x :: ys)
-- This is failing because the type doesn't reduce.  We need to process arg2 first, after determining that
-- TODO the type of the second argument is not useful to split until the first one is split
-- need to check the type when we decide to split on an argument
-- cong-cons _ Refl Refl = ?

-- and this one was having some trouble on the RHS, which turned out to `cong`
-- being undefined.
cong-cons _ Refl x = case x of Refl => Refl

-- Idris' complaint about B is more readable:

-- Error: While processing type of appAssoc. Can't solve constraint
-- between: Vec ?a ((?l + ?n) + ?m) and ?b ((?l + ?n) + ?m).

++-assoc : ∀ a l n m. (xs : Vect a l) → (ys : Vect a n) → (zs : Vect a m) →
           -- TODO newt + idris have trouble sorting out B
           _≡⟨_⟩_ {_} {Vect a} (xs ++ (ys ++ zs)) (+-assoc l n m) ((xs ++ ys) ++ zs)
++-assoc Nil ys zs = Refl
-- TODO need rhs hole to look more like this in newt:
-- hole : DepEq (x :: (xs ++ (ys ++ zs))) (cong S (plusAssoc k n m)) (x :: ((xs ++ ys) ++ zs))
++-assoc {a} {S k} {n} {m} (x :: xs) ys zs = cong-cons x (+-assoc k n m) (++-assoc xs ys zs)


