fresh vs forall - Yet Another Ranha

tm : type.
step : tm -> tm -> type.

sn : tm -> type.
sn_ : ({U:tm} step T U -> sn U) -> sn T.

lem : (sn T) -> (step T U) -> (sn U) -> type.
%mode lem +D1 +D2 -D3.

lem_pr : lem (sn_ Pred : sn T)
	  (StepTU : step T U)
	  (Pred U StepTU).
%terminates {} (lem _ _ _).

まずそもそもの所、これで上手くやりたい事が出来ているのかどうか分からないのですが・・・。

話の発端は、
http://www2.tcs.ifi.lmu.de/~abel/entcs04.pdf
のp11

For the same reason, Tait’s proof cannot be formalized directly in Twelf.

と、p12

Due to the interpretation of quantification in Twelf

の辺りなのですが、上記の通りにやってあげれば良いんじゃないのかしらとしか思えなくて、何がどう・・・どうなってるんだろう。

Twelfでまんまencodeしたものは、universal quantificationではなくてfreshに成る、したがってmathematical languageに書き戻した時に元とは違って来てしまいますよ、と書いているのですが、何か困る事が起こるのかしら？
そして何故、freshになってしまうのか?というのが分からない所です。

上でやっている事は、Strong Normalizationのformalize(これがsnとsn_.sn_が特にinductiveなruleの代わり)のつもりで、lemは項Tが強正規化可能であり、Tを1-step reductionすると項Uが得られる時、項Uもまた強正規化可能である　つまり、強正規化可能はreductionのもとで閉じているを試しに証明した感じになっています。(つもりです...

しかしTwelfが分からないぽん！！

Agda2で書くと

module SN where

data Tm : Set0 where
  c : Tm
  app : Tm -> Tm -> Tm
  abs : Tm -- 面倒臭いのでパス (Tm -> Tm) -> TmでFull HOASぽくやるとnegative

data Unit : Set0 where
  unit : Unit

-- 1-step reductionのつもり
step : Tm -> Tm -> Set0
step a b = Unit

-- Strong Normalizationの定義
{-
∀n.(step m n) → SN n
----------------------
        SN m
-}
data SN1 (m : Tm) : Set0 where
  sn1 : ((n : Tm) -> (step m n) -> SN1 n) -> SN1 m

-- ∀m n.(SN m) ∧ (step m n) → SN n
th1 : {m n : Tm} -> SN1 m -> (step m n) -> SN1 n
th1 {m} {n} (sn1 p) s = p n s
  where
    p' : (o : Tm) -> (step m o) -> SN1 o
    p' = p

{-
(step m n) → SN n
------------------
      SN m
-}
-- この定義だと項nがerasureされちゃうので
-- ∀m n.(SN m) ∧ (step m n) → SN n
-- は証明出来なく成ってしまう
data SN2 (m : Tm) : Set0 where
  sn2 : (n : Tm) -> ((step m n) -> SN2 n) -> SN2 m

th2 : {m n : Tm} -> SN2 m -> (step m n) -> SN2 n
th2 {m} {n} (sn2 .n p) s = p' s'
  where
    p' : (step m n) -> SN2 n
    p' = p

    s' : step m n
    s' = s

こうなるはずで、このSN1とSN2に相当するものをTwelfで書いて、SN2でformalizeしても何か証明出来そうな予感がして、実際に出来ると不味いとかそんな感じなのか・・・しら・・・？

むしろそれよりはSN1にsyntax的な意味でそのまま落として、それが何故か証明出来ないとかの方が必要な話なのではないかしら。

Twelfでやってみる

tm : type.
step : tm -> tm -> type.

sn : tm -> type.
sn_ : {T:tm} ({U:tm} step T U -> sn U) -> sn T.
sn2 : {T:tm} {U:tm} (step T U -> sn U) -> sn T.

lem : (sn T) -> (step T U) -> (sn U) -> type.
%mode lem +DSnT +DStepTU -DSnU.

lem_hoge : lem
	    (sn_ T Pred : sn T)
	    (StepTU : step T U)
	    (Pred U StepTU : sn U).

lem_hoge2 : lem
	     (sn2 T U Pred : sn T)
	     (StepTU : step T U)
	     (Pred StepTU : sn U).

何か明らかに違うような気がするのですが。。。

これをTwelf Serverに投げると

lem_hoge :
   {T:tm} {U:tm} {Pred:{x:tm} step T x -> sn x} {StepTU:step T U}
      lem (sn_ T ([U1:tm] [x:step T U1] Pred U1 x)) StepTU (Pred U StepTU).
lem_hoge2 :
   {T:tm} {U:tm} {Pred:step T U -> sn U} {StepTU:step T U}
      lem (sn2 T U ([x:step T U] Pred x)) StepTU (Pred StepTU).

とかに成っていて、素直にパターンマッチ相当をするにはどうすれば良いんだろう。