I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other:

Vec : (a : Type) -> (n : Nat) -> Type0
Rel : (a : Type) -> a -> a -> Type

data Vec : (a : Type) -> (n : Nat) -> Type0 where
  Nil : Rel Nat n 0 -> Vec a n
  Cons : a -> Vec a n' -> Rel Nat (S n') n -> Vec a n

data Rel : (a : Type) -> a -> a -> Type0 where
  RRefl : (a : Type) -> (x : a) -> Rel a x x
  RSucc : (m n : Nat) -> Rel Nat m n -> Rel Nat (S m) (S n)
  RCons : (e : Type) -> (m n: Nat) -> (h1 h2 : e) -> (t1 t2 : Vec e m) ->
            Rel e h1 h2 -> Rel (Vec e m) t1 t2 ->
            (rn : Rel Nat (S m) n) ->
            Rel (Vec e n) (Cons h1 t1 rn) (Cons h2 t2 rn) 

Right now, both Agda and Idris reject this definition, since Rel refers not only to Vec, but to Cons, a constructor of Vec.

I'm wondering:

  • Is this restriction an implementation detail, or is it critical for ensuring consistency of a type theory? i.e. if we allow this kind of mutual reference, can we prove False?
  • Are there standard techniques to get around this? Possibly using induction-induction or induction-recursion?

One idea I had is to define a sort of PreVec that takes a parameter of type (rel : Nat -> Nat -> Type). But will this cause problems with predicativity?

  • $\begingroup$ What is the motivation for this definition? I fail to see any use case. Rel seems to be a type-casing version of propositional equality which adds redundant equality proofs. $\endgroup$ Commented Nov 19, 2019 at 11:14
  • $\begingroup$ @AndrásKovács This is just meant to be a minimal example, what I have is different, and has additional cases that make it more than propositional equality $\endgroup$ Commented Nov 19, 2019 at 16:13
  • $\begingroup$ could you add the example which you actually want to use? Just from this, I cannot comment on how to meaningfully reformulate. $\endgroup$ Commented Nov 19, 2019 at 16:34


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.