Library GeneratorsEq
This file generates unsatisfiable formulas for problems
in the fragment SAT + EUF or SAT + EUF + ZArith.
We define families of boolean variables indexed by an integer.
Inductive x : nat → Prop :=
| mk_x : ∀ i, x i.
Inductive y : nat → Prop :=
| mk_y : ∀ i, y i.
Inductive z : nat → Prop :=
| mk_z : ∀ i, z i.
| mk_x : ∀ i, x i.
Inductive y : nat → Prop :=
| mk_y : ∀ i, y i.
Inductive z : nat → Prop :=
| mk_z : ∀ i, z i.
diamond_equations acc n appends to the formula acc all the
disjunctions (x i = y i ∧ y i = x (S i)) ∨
((x i = z i) ∧ (z i = x (S i)) for i ranging 0 to pred n.
It corresponds to "diamond" equalities on the chains x, y and z:
y0 y1
/ \ / \
x 0 ----> x 1 -----> .................. ----> x n
\ / \ /
z0 z1
such that each diamond constraint ensures that x i = x (S i) by
transitivity whether at the top or the bottom of the diamond.
Fixpoint diamond_equations (acc : Prop) (n : nat) : Prop :=
match n with
| O ⇒ acc
| S m ⇒
let eq1 := x m = y m ∧ y m = x n in
let eq2 := x m = z m ∧ z m = x n in
diamond_equations ((eq1 ∨ eq2) → acc) m
end.
match n with
| O ⇒ acc
| S m ⇒
let eq1 := x m = y m ∧ y m = x n in
let eq2 := x m = z m ∧ z m = x n in
diamond_equations ((eq1 ∨ eq2) → acc) m
end.
diamond n returns the implication diamond_equations n → x 0 = x n.
It is a valid formula with 1 + 4 × n equations between 1 + 3 × n
variables.
We now implement a variation of diamond where one layer of a
function symbol f is added to the x_i at every step. Whereas
diamond n is valid in SAT + equivalence, this one requires congruence.
fdiamond_equations f acc n appends to the formula acc all the
disjunctions x i = y i ∧ y i = f (x (S i)) ∨
((x i = z i) ∧ (z i = f (x (S i))) for i ranging 0 to pred n.
It corresponds to "diamond" equalities on the chains x, y and z:
y0 y1
/ \ / \
x 0 ---> f(x 1)-----> .................. ----> f^n(x n)
\ / \ /
z0 z1
such that each diamond constraint ensures that x i = f(x (S i))
by transitivity whether at the top or the bottom of the diamond.
NB : it is actually going in reverse order with respect to the above schema
but you get the idea.
Fixpoint fdiamond_equations (f : Prop → Prop) (acc : Prop) (n : nat) : Prop :=
match n with
| O ⇒ acc
| S m ⇒
let eq1 := x m = y m ∧ y m = f (x n) in
let eq2 := x m = z m ∧ z m = f (x n) in
fdiamond_equations f ((eq1 ∨ eq2) → acc) m
end.
match n with
| O ⇒ acc
| S m ⇒
let eq1 := x m = y m ∧ y m = f (x n) in
let eq2 := x m = z m ∧ z m = f (x n) in
fdiamond_equations f ((eq1 ∨ eq2) → acc) m
end.
fdiamond n returns the implication
fdiamond_equations f n → x 0 = f^n (x n).
It is a valid formula with 1 + 4 × n equations between 1 + 3 × n
variables.
Fixpoint power (f : Prop → Prop) n x :=
match n with 0 ⇒ x | S m ⇒ power f m (f x) end.
Definition fdiamond (f : Prop → Prop) (n : nat) : Prop :=
fdiamond_equations f (x 0 = power f n (x n)) n.
match n with 0 ⇒ x | S m ⇒ power f m (f x) end.
Definition fdiamond (f : Prop → Prop) (n : nat) : Prop :=
fdiamond_equations f (x 0 = power f n (x n)) n.
We define families of integer variables indexed by an integer.
diamond_Zequations acc n appends to the formula acc all the
disjunctions (x i = y i ∧ y i = 1 + x (S i)) ∨
((x i = z i) ∧ (z i = 1 + x (S i)) for i ranging 0 to pred n.
It corresponds to "diamond" equalities on the chains x, y and z:
y0 y1
/ \ / \
x 0 ----> x 1 -----> .................. ----> x n
\ / \ /
z0 z1
such that each diamond constraint ensures that x i = 1 + x (S i) by
transitivity whether at the top or the bottom of the diamond.
Fixpoint diamond_Zequations (acc : Prop) (n : nat) : Prop :=
match n with
| O ⇒ acc
| S m ⇒
let eq1 := zx m = zy m ∧ zy m = (1 + zx n)%Z in
let eq2 := zx m = zz m ∧ zz m = (1 + zx n)%Z in
diamond_Zequations ((eq1 ∨ eq2) → acc) m
end.
match n with
| O ⇒ acc
| S m ⇒
let eq1 := zx m = zy m ∧ zy m = (1 + zx n)%Z in
let eq2 := zx m = zz m ∧ zz m = (1 + zx n)%Z in
diamond_Zequations ((eq1 ∨ eq2) → acc) m
end.
Zdiamond n returns the implication
diamond_Zequations n → zx 0 - n = zx n.
It is a valid formula with 1 + 4 × n equations between 1 + 3 × n
variables.
Another goal which only contains arithmetic, no real congruence,
and basically no propositional value. It is a sequence of arithmetic
equalities which simulate the definition of a Fibonacci number.
Fixpoint fibo_defs (res : Prop) (n : nat) : Prop :=
match n with
| 0 ⇒ zx 0 = 1%Z → res
| S m ⇒
match m with
| 0 ⇒ zx 1 = zx 0 → fibo_defs res m
| S p ⇒ zx (S (S p)) = Zplus (zx (S p)) (zx p) → fibo_defs res m
end
end.
Fixpoint fibo (n : nat) (z : Z) : Z :=
match n with
| 0 ⇒ 1%Z
| S m ⇒
match m with
| 0 ⇒ 1%Z
| S p ⇒ Zplus (fibo p (z-2)) (fibo m (z-1))
end
end.
Definition fibo_arith (n : nat) :=
fibo_defs (zx n = fibo n (Z_of_nat n)) n.
match n with
| 0 ⇒ zx 0 = 1%Z → res
| S m ⇒
match m with
| 0 ⇒ zx 1 = zx 0 → fibo_defs res m
| S p ⇒ zx (S (S p)) = Zplus (zx (S p)) (zx p) → fibo_defs res m
end
end.
Fixpoint fibo (n : nat) (z : Z) : Z :=
match n with
| 0 ⇒ 1%Z
| S m ⇒
match m with
| 0 ⇒ 1%Z
| S p ⇒ Zplus (fibo p (z-2)) (fibo m (z-1))
end
end.
Definition fibo_arith (n : nat) :=
fibo_defs (zx n = fibo n (Z_of_nat n)) n.