Search code examples
idrisproof-of-correctness

Does it help if proofs are orthogonal?

Suppose I have a function

f : Vect m Nat -> Vect n Nat -> {auto _ : Proof m n} -> Foo m n

where

data Proof : Nat -> Nat -> Type where
  Eq : Proof x x
  One : Proof 1 _

I can make a Proof 1 1 as Eq or One. Thus these aren't "orthogonal". In more complicated examples, I can have recursive data constructors where I might be able to provide a proof as Constructor1 Constructor2 or Constructor3 Constructor1. Does it matter if constructors aren't orthogonal? In particular, does it hinder proof search?

Solution

  • Orthogonal data constructors make it simpler and clearer to implement functions. With overlapping constructors, you will be duplicating behaviour between patterns e.g.

    foo : Proof x y -> ?
foo Eq = ?eq
foo One = ?one  -- duplicates `foo (Eq {x = 1})`