Armaël Guéneau

2018-11-12 20:54:54 UTC

Dear coq-club,

Consider the following proof script:

Require Import ZArith Psatz.

Open Scope Z_scope.

Goal forall a b c,

(((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\

((0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\

((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\

(0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\

((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\

((0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)) /\

((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\

(0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)

->

False.

Proof.

intros.

Time Fail Fail lia. (* Succeeds but takes 6s *)

(* trivially split on /\ by hand *)

repeat match goal with h: _ /\ _ |- _ => destruct h end.

Time lia. (* Takes 0.06s *)

Qed.

Does anyone have an explanation? Why is lia struggling so much on the

first goal, and why does manually splitting conjunctions makes it

suddenly much easier?

Cheers,

Armaël

Consider the following proof script:

Require Import ZArith Psatz.

Open Scope Z_scope.

Goal forall a b c,

(((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\

((0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\

((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\

(0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\

((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\

((0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)) /\

((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\

(0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)

->

False.

Proof.

intros.

Time Fail Fail lia. (* Succeeds but takes 6s *)

(* trivially split on /\ by hand *)

repeat match goal with h: _ /\ _ |- _ => destruct h end.

Time lia. (* Takes 0.06s *)

Qed.

Does anyone have an explanation? Why is lia struggling so much on the

first goal, and why does manually splitting conjunctions makes it

suddenly much easier?

Cheers,

Armaël