RTE does not work with the newer version of Coq

[ishowta]

問題点

~~明らかに含意しているのにrte_ja.shの出力がunknownとなってしまいます。
Coqについて勉強不足で、何が問題なのか分かりませんでした。~~ ReadmeでCoqのバージョンが指定されておらず、かつ最新のCoq8.11でRTEが動作しません。

環境

• python: 3.7.9
• coq: 8.11.2
• ccg2lambda: master branch (442a9ec9be7393d92c77a03856aa4a9c71c20078)
• OS: WSL Ubuntu20.04

やったこと

1. Readmeに書いてあるセットアップをしました。
2. 日本語のRTEを行うために、emnlp2016exp.shを参考にして以下のセットアップを行いました。

   cp ja/coqlib_ja.v coqlib.v
   coqc coqlib.v
   cp ja/tactics_coq_ja.txt tactics_coq.txt
   

3. sentence.txtに同じ文を入れました。（明らかに含意しているので）

   ソクラテスは人間である。
   ソクラテスは人間である。
   

4. 以下のスクリプトを実行しました。

    ./ja/rte_ja.sh out/sentence.txt ja/semantic_templates_ja_event.yaml 
   

   Output

   unknown
   

調べたこと

• 手動でCoqを動かすとnltac_set; nltac_final.のところでNo such goal.と出て止まりました。

  Require Export coqlib.
  Parameter _ソクラテス : Entity.
  Parameter _人間 : Entity -> Prop.
  Theorem t1: (and True (exists x, (and (_人間 x) (exists e, (and (and ((Nom e) = x) True) ((Nom e) = _ソクラテス)))))) -> (and True (exists x, (and (_人間 x) (exists e, (and (and ((Nom e) = x) True) ((Nom e) = _ソクラテス)))))). Set Firstorder Depth 1. nltac. nltac_set; nltac_final. Set Firstorder Depth 3. nltac_final. Qed.
  

参照

https://github.com/mynlp/ccg2lambda/blob/442a9ec9be7393d92c77a03856aa4a9c71c20078/scripts/theorem.py#L337-L343

[ishowta]

I downgraded Coq from 8.11 to 8.3 and it worked fine.