日々の流転

λ. Propositional equality の証明の equality

Propositional equality の型である Id a b の要素はせいぜい一つしかないので、要素が二つ与えられたらそれらは等しいに決まっている。それを証明したい。が、以下のコードは内側のcaseの部分で「Error in the definition of eqId because: cannot case: exps [x, x] must be distinct variables.」というエラーになってしまう。(e1へのcaseでa,b,xがunifyされているためこのようなエラーメッセージになってる。2005-05-16 の case on non-var でも書いたが、この制約は必要以上に厳しい気がする)

eqId (|A::Set) (|a,|b :: A) (e1,e2 :: Id a b)
  :: Id e1 e2
  = case e1 of
    (ref x)->
      case e2 of
      (ref y)->
        ref@_ (ref@_ x)

Agdaでこの命題を証明する方法はあるだろうか?　SET.alfa では Id a b の Collapsed も定義されてないし、やっぱり無理なのか?　Per Martin-Löfの Intuitionistic Type Theory でもこれは証明できるので、「Martin-Löf. の型理論に基づく対話型定理証明支援系」と呼ばれているAgdaでこれが証明できないとしたら、納得いかん。

(2005-09-17 追記) Intuitionistic Type Theory は propositional equality type の strong elimination を含む extensional な型理論だから、「Agdaでも証明できるべき」という理由にはならない気がしてきた。というか、私はその辺りの話が全然分かってない。Intuitionistic Type Theory 以降の Martin-Löf 流の型理論を学ぶには何を読めば良いのだろう?　Bengt Nordström, Kent Petersson, Jan M. Smith の Programming in Martin-Löf's Type Theory - An Introduction ?

(2006-02-05 追記) Thierry Coquand の Pattern matching with dependent types の p.9 には次のように書いてあった。

By contrast, it is not clear how to represent the following computation rule in term of the usual elimination rules⁴. We have seen that the unique contextual mapping

{y := x, p := refl(N,x), q := refl(N,x)}: (x : N) → Δ,

is a covering of Δ = x,y : N; p,q : Id(N, x, y). It follows that it is correct to add a new constant f : (x,y : N; p,q : Id(N,x,y))Id(Id(N,x,y),p,q) together with the computation rule

f(x, x, refl(N,x), refl(N,x)) = refl(Id(N,x,x), refl(N,x)) (x : N).

---

⁴ This problem has been independently suggested by Thomas Streicher.

(2006-04-18 追記) Michael Hedberg の A coherence theorem for Martin-Löf's type theory には次のように書かれていた。というわけで、elimIdではいくら頑張っても証明できないことになります。証明するにはAgdaに対して何らかの拡張が必要になるでしょう。

Although one might expect the identity sets to be collapse, it is impossible to prove in general that they are, as long as type theory is restricted to the standard elimination rules. This negative result is proved by Hofmann and Streicher [11], using a groupoid interpretation of type theory.

---

[11] M. Hofmann and T. Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.

(2006-05-14追記) この「A groupoid model refutes uniqueness of identity proofs」を読んだ。20060514#p01を参照。