CN: Fix lemmata tests (#454)

These tests are not enabled in the CI yet (they should be, but I couldn't figure it out and I'm away for the next 1.5 weeks). `as_auto_mutual_dt` was deleted because there's [a check in CN](https://github.com/rems-project/cerberus/blob/556171a17fca94b6aaf76bccfa7db63833428113/backend/cn/lib/wellTyped.ml#L2443-L2444) which prevents the indirect recursion used in [as_auto_mutual_dt/tree16.error.c](https://github.com/rems-project/cerberus/blob/master/tests/cn/tree16/as_auto_mutual_dt/tree16.error.c) from passing. Tested with the following: ```sh ➜ coqc --version The Coq Proof Assistant, version 8.19.2 compiled with OCaml 4.14.1 ```
rems-project · Jul 30, 2024 · 20d9d5c · 20d9d5c
1 parent 556171a
commit 20d9d5c
Show file tree

Hide file tree

Showing 9 changed files with 4 additions and 371 deletions.
diff --git a/tests/cn/mutual_rec/coq_lemmas/Makefile b/tests/cn/mutual_rec/coq_lemmas/Makefile
@@ -3,6 +3,6 @@
 
 all:
 	coq_makefile -f _CoqProject -o Makefile.coq
-	cn --lemmata theories/Gen_Spec.v ../mutual_rec.c
+	cn verify --lemmata theories/Gen_Spec.v ../mutual_rec.c
 	make -f Makefile.coq
 
diff --git a/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v b/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v
@@ -155,7 +155,7 @@ Lemma merge_flip: forall xs ys,
 Proof.
   intros.
   unfold merge.
-  rewrite plus_comm.
+  rewrite PeanoNat.Nat.add_comm.
   apply merge_w_flip.
   auto.
 Qed.

diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v
diff --git a/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile b/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile
@@ -3,6 +3,6 @@
 
 all:
 	coq_makefile -f _CoqProject -o Makefile.coq
-	cn --lemmata theories/Gen_Spec.v ../tree16.c
+	cn verify --lemmata theories/Gen_Spec.v ../tree16.c
 	make -f Makefile.coq