test: Add tests and some fix

3 files changed, 190 insertions, 14 deletions

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 6d9a87ec..323448ae 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -78,7 +78,7 @@
 
 (defun coq-test-exit ()
   "Exit the Coq process."
-  (proof-shell-exit t))
+  (proof-shell-exit t)) 
 
 ; (coq-test-on-file nil (message (buffer-file-name)) (message "OK") 42)
 
@@ -172,6 +172,12 @@ For example, COMMENT could be (*test-definition*)"
   (goto-char (point-min))
   (search-forward comment))
 
+(defun should-response (message)
+  (should (equal message
+		 (string-trim
+                  (with-current-buffer "*response*"
+                    (buffer-substring-no-properties (point-min) (point-max)))))))
+
 ;; TODO: Use https://github.com/rejeep/ert-async.el
 ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html
 
@@ -182,6 +188,7 @@ For example, COMMENT could be (*test-definition*)"
      ;; (should (process-list)) ; wouldn't be a strong enough assert.
      (should (get-process "coq")))))
 
+
 (ert-deftest coq-test-print ()
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
@@ -189,10 +196,7 @@ For example, COMMENT could be (*test-definition*)"
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
      (proof-shell-wait)
-     (should (equal "trois is defined"
-		    (string-trim
-                     (with-current-buffer "*response*"
-                       (buffer-substring-no-properties (point-min) (point-max)))))))))
+     (should-response "trois is defined"))))
 
 
 (ert-deftest coq-test-position ()
@@ -200,9 +204,10 @@ For example, COMMENT could be (*test-definition*)"
    (coq-test-full-path "test1.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
+     (let ((proof-point (point)))
      (proof-goto-point)
      (proof-shell-wait)
-     (should (equal (proof-queue-or-locked-end) (point))))))
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
 (ert-deftest coq-test-insert ()
@@ -216,15 +221,31 @@ For example, COMMENT could be (*test-definition*)"
        (coq-test-goto-before "(*test-insert*)")
        (move-beginning-of-line nil)
        (insert "\n")
-       (previous-line)
-       (insert "  (0)")
-       (coq-test-goto-after "(0)")
        ;; The locked end point should go up compared to before 
-       (should (< (proof-queue-or-locked-end) proof-point)))))) 
+       (should (< (proof-queue-or-locked-end) proof-point))))))
+
+
+(ert-deftest coq-test-lemma-false ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test1.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-lemma2*)")
+     (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
+     (proof-goto-point)
+     (proof-shell-wait)
+     (should-response "Error: Unable to unify \"false\" with \"true\".")
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
+
 
+(ert-deftest coq-test-wholefile ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test_wholefile.v")
+   (lambda ()
+     (let ((proof-point (save-excursion (coq-test-goto-after "(*end here*)"))))
+     (proof-process-buffer)
+     (proof-shell-wait)
+     (should (equal (proof-queue-or-locked-end)  proof-point))))))
 
-;;TODO
-;other tests
 
 (provide 'coq-tests)
 
diff --git a/ci/test1.v b/ci/test1.v
index fc1fc943..3812adbd 100644
--- a/ci/test1.v
+++ b/ci/test1.v
@@ -1,7 +1,7 @@
 Definition trois := 3. (*test-definition*)
 Print trois.
 Eval compute in 10 * trois * trois.
-
+ 
 
 
 Lemma easy_proof : forall A : Prop, A -> A.
@@ -9,4 +9,14 @@ Proof using .
   intros A.
   intros proof_of_A. (*test-insert*)
   exact proof_of_A.
-Qed. (*test-lemma*) 
+Qed. (*test-lemma*)
+
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  reflexivity.
+Qed. (*test-lemma2*)
+  
diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
new file mode 100644
index 00000000..0a87d9a6
--- /dev/null
+++ b/ci/test_wholefile.v
@@ -0,0 +1,145 @@
+(*taking from coq.inria.fr *)
+
+Require Export ArithRing.
+Require Export Compare_dec.
+Require Export Wf_nat.
+Require Export Arith.
+Require Export Omega.
+
+Theorem minus_minus : forall a b c : nat, a - b - c = a - (b + c).
+intros a; elim a; auto.
+intros n' Hrec b; case b; auto.
+Qed.
+
+Remark expand_mult2 : forall x : nat, 2 * x = x + x.
+intros x; ring.
+Qed.
+
+Theorem lt_neq : forall x y : nat, x < y -> x <> y.
+unfold not in |- *; intros x y H H1; elim (lt_irrefl x);
+ pattern x at 2 in |- *; rewrite H1; auto.
+Qed.
+Hint Resolve lt_neq.
+
+Theorem monotonic_inverse :
+ forall f : nat -> nat,
+ (forall x y : nat, x < y -> f x < f y) ->
+ forall x y : nat, f x < f y -> x < y.
+intros f Hmon x y Hlt; case (le_gt_dec y x); auto.
+intros Hle; elim (le_lt_or_eq _ _ Hle).
+intros Hlt'; elim (lt_asym _ _ Hlt); apply Hmon; auto.
+intros Heq; elim (lt_neq _ _ Hlt); rewrite Heq; auto.
+Qed.
+
+Theorem mult_lt : forall a b c : nat, c <> 0 -> a < b -> a * c < b * c.
+intros a b c; elim c.
+intros H; elim H; auto.
+intros c'; case c'.
+intros; omega.
+intros c'' Hrec Hneq Hlt;
+ repeat rewrite <- (fun x : nat => mult_n_Sm x (S c'')).
+auto with *.
+Qed.
+
+Remark add_sub_square_identity :
+ forall a b : nat,
+ (b + a - b) * (b + a - b) = (b + a) * (b + a) + b * b - 2 * ((b + a) * b).
+intros a b; rewrite minus_plus.
+repeat rewrite mult_plus_distr_r || rewrite <- (mult_comm (b + a)).
+replace (b * b + a * b + (b * a + a * a) + b * b) with
+ (b * b + a * b + (b * b + a * b + a * a)); try (ring; fail).
+rewrite expand_mult2; repeat rewrite minus_plus; auto with *.
+Qed.
+
+Theorem sub_square_identity :
+ forall a b : nat, b <= a -> (a - b) * (a - b) = a * a + b * b - 2 * (a * b).
+intros a b H; rewrite (le_plus_minus b a H); apply add_sub_square_identity.
+Qed.
+
+Theorem square_monotonic : forall x y : nat, x < y -> x * x < y * y.
+intros x; case x.
+intros y; case y; simpl in |- *; auto with *.
+intros x' y Hlt; apply lt_trans with (S x' * y).
+rewrite (mult_comm (S x') y); apply mult_lt; auto.
+apply mult_lt; omega.
+Qed.
+
+Theorem root_monotonic : forall x y : nat, x * x < y * y -> x < y.
+exact (monotonic_inverse (fun x : nat => x * x) square_monotonic).
+Qed.
+
+Remark square_recompose : forall x y : nat, x * y * (x * y) = x * x * (y * y).
+intros; ring.
+Qed.
+
+Remark mult2_recompose : forall x y : nat, x * (2 * y) = x * 2 * y.
+intros; ring.
+Qed.
+Section sqrt2_decrease.
+Variables (p q : nat) (pos_q : 0 < q) (hyp_sqrt : p * p = 2 * (q * q)).
+
+Theorem sqrt_q_non_zero : 0 <> q * q.
+generalize pos_q; case q.
+intros H; elim (lt_n_O 0); auto.
+intros n H.
+simpl in |- *; discriminate.
+Qed.
+Hint Resolve sqrt_q_non_zero.
+
+Ltac solve_comparison :=
+  apply root_monotonic; repeat rewrite square_recompose; rewrite hyp_sqrt;
+   rewrite mult2_recompose; apply mult_lt; auto with arith.
+
+Theorem comparison1 : q < p.
+replace q with (1 * q); try ring.
+replace p with (1 * p); try ring.
+solve_comparison.
+Qed.
+
+Theorem comparison2 : 2 * p < 3 * q.
+solve_comparison.
+Qed.
+
+Theorem comparison3 : 4 * q < 3 * p.
+solve_comparison.
+Qed.
+Hint Resolve comparison1 comparison2 comparison3: arith.
+
+Theorem comparison4 : 3 * q - 2 * p < q.
+apply plus_lt_reg_l with (2 * p).
+rewrite <- le_plus_minus; try (simple apply lt_le_weak; auto with arith).
+replace (3 * q) with (2 * q + q); try ring.
+apply plus_lt_le_compat; auto.
+repeat rewrite (mult_comm 2); apply mult_lt; auto with arith.
+Qed.
+
+Remark mult_minus_distr_l : forall a b c : nat, a * (b - c) = a * b - a * c.
+intros a b c; repeat rewrite (mult_comm a); apply mult_minus_distr_r.
+Qed.
+
+Remark minus_eq_decompose :
+ forall a b c d : nat, a = b -> c = d -> a - c = b - d.
+intros a b c d H H0; rewrite H; rewrite H0; auto.
+Qed.
+
+Theorem new_equality :
+ (3 * p - 4 * q) * (3 * p - 4 * q) = 2 * ((3 * q - 2 * p) * (3 * q - 2 * p)).
+repeat rewrite sub_square_identity; auto with arith.
+repeat rewrite square_recompose; rewrite mult_minus_distr_l.
+apply minus_eq_decompose; try rewrite hyp_sqrt; ring.
+Qed.
+End sqrt2_decrease.
+Hint Resolve lt_le_weak comparison2: sqrt.
+
+Theorem sqrt2_not_rational :
+ forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
+intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
+clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq));
+ intros Hlt_O_q Heq.
+apply (Hrec (3 * q - 2 * p) (comparison4 _ _ Hlt_O_q Heq) (3 * p - 4 * q)).
+apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 * p);
+ rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with *.
+apply new_equality; auto.
+Qed.
+
+(*end here*)