The Coq mailing list

[Chantal KELLER <chantal.keller AT wanadoo.fr>]

Hello Marko,

The main (current) problem with SMTCoq is that it is working in bool and not 
in Prop (we are working on changing it). However, as you said you do not care 
if it is a bit slow, you can first change your goal into a boolean problem 
(using autorewrite) then use SMTCoq. Attached is your example; it works fine 
with coqtop in less than ten seconds.

Chantal.

> In the future, there is hope using SAT, SMT techniques.
> The most mature prototype is probably SMTCoq:
> http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html
Require Import SMTCoq.
Require Import ZArith.
Open Scope Z_scope.


Lemma False_false: False <-> (false = true).
Proof. split; auto; discriminate. Qed.

Lemma Impl_implb: forall x y, ((x = true) -> (y = true)) <-> (implb x y = true).
Proof. intros x y; split; case x; case y; auto. Qed.

Lemma And_andb: forall x y, ((x = true) /\ (y = true)) <-> (andb x y = true).
Proof. intros x y; split; case x; case y; auto; intros [H1 H2]; discriminate. Qed.

Lemma Or_orb: forall x y, ((x = true) \/ (y = true)) <-> (orb x y = true).
Proof. intros x y; split; case x; case y; auto; intros [H|H]; discriminate. Qed.

Hint Rewrite Zle_is_le_bool Zge_is_le_bool Zlt_is_lt_bool Zgt_is_gt_bool Zeq_is_eq_bool False_false Impl_implb And_andb Or_orb : b.




Section Test.

Parameter a b : Z.

Definition H1 := 3 >= a /\ 1 >= b -> 3 - a <= 1 - b.
Definition H2 := 3 >= a /\ 1 < b -> 3 - a <= b - 1.
Definition H3 := 3 < a /\ 1 >= b -> a - 3 <= 1 - b.
Definition H4 := 3 < a /\ 1 < b -> a - 3 <= b - 1.

Definition H5 := 3 >= a /\ 3 >= b -> 3 - a <= 3 - b.
Definition H6 := 3 >= a /\ 3 < b -> 3 - a <= b - 3.
Definition H7 := 3 < a /\ 3 >= b -> a - 3 <= 3 - b.
Definition H8 := 3 < a /\ 3 < b -> a - 3 <= b - 3.

Definition H9 := 1 >= b -> 1 - b = 1.
Definition H10 := 1 < b -> b - 1 = 1.

Definition H11 := 1 = b /\ ((3 = 1 -> False) \/ 3 = 1 /\ (3 <= a /\ 3 <= 5
\/ a <= 3 /\ 5 <= 3)) \/ 5 = a /\ ((3 = 5 -> False) \/ 3 = 5 /\ (3 <= b /\
3 <= 1 \/ b <= 3 /\ 1 <= 3)) -> False.

Definition H12 := 1 <= b.
Definition H13 := b <= 8.
Definition H14 := 1 <= a.
Definition H15 := a <= 8.

Definition H16 := 3 >= b -> 2 <= 3 - b.
Definition H17 := 3 < b -> 2 <= b - 3.

Goal H1 -> H2 -> H3 -> H4 -> H5 -> H6 -> H7 -> H8 -> H9 -> H10 -> H11 -> H12 -> H13 -> H14 -> H15 -> H16 -> H17 -> False.
unfold H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17.
autorewrite with b.
verit.
Qed.