Update examples to use coq_codewars

Author: kazk

examples/failing/Solution.v

@@ -1 +1 @@
-Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.
+Theorem thm4 : 1 = 1. Proof. Admitted.

examples/failing/SolutionTest.v

@@ -1,16 +1,9 @@
-Require Import Solution.
-
-Theorem thm1 : 1 = 1 + 0. Proof. admit. Admitted.
-Print Assumptions thm1.
-
-Parameter thm2 : 1 + 0 = 0 + 1.
-Print Assumptions thm2.
-
-Theorem thm3 : 1 = 0 + 1. Proof. rewrite <- thm2. exact thm1. Qed.
-Print Assumptions thm3.
-
-Theorem thm4_check : 1 = 1.
-Proof.
-  exact thm4.
-  Print Assumptions thm4.
-Qed.
+Require Solution.
+From CW Require Import Loader.
+
+CWGroup "Solution.thm4".
+  CWTest "should have the correct type".
+    CWAssert Solution.thm4 : (1 = 1).
+  CWTest "should be closed under the global context".
+    CWAssert Solution.thm4 Assumes.
+CWEndGroup.

examples/passing/Solution.v

@@ -1,7 +1 @@
-Theorem plus_n_O : forall n:nat, n = n + 0.
-Proof.
-  intros n.
-  induction n.
-  - reflexivity.
-  - simpl. rewrite <- IHn. reflexivity.
-Qed.
+Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.

examples/passing/SolutionTest.v

@@ -1,6 +1,9 @@
-Require Import Solution.
-Theorem plus_n_O_check : forall n:nat, n = n + 0.
-Proof.
-  exact plus_n_O.
-  Print Assumptions plus_n_O.
-Qed.
+Require Solution.
+From CW Require Import Loader.
+
+CWGroup "Solution.thm4".
+  CWTest "should have the correct type".
+    CWAssert Solution.thm4 : (1 = 1).
+  CWTest "should be closed under the global context".
+    CWAssert Solution.thm4 Assumes.
+CWEndGroup.