The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

Hello,

If you just want to write a proposition that a particular constraint
system has a solution, then you can just write, e.g.,

Implicit Types x : Z.

Theorem t : exists x1, exists x2, exists x3, x1 <> x2 /\ x1 + x2 + x3 = 5.

Then you can prove the existence of a solution only for this
particular system. However, if you want to reason about arbitrary
systems and prove meta-results, like "every system with at most three
constraints has a solution", then you need to encode constraints as a
Coq datatype. Then you will be able to write functions that operate on
such systems, e.g., create them or take them apart. This is in
contrast to propositions like t : Prop above: you can pass t around as
a first-class value, but you can't match it against a pattern.

So, for example, you could have the following development.

Require Import List.
Require Import Omega.

Inductive constraint : Set :=
| cneq : nat -> nat -> constraint (* cneq i1 i2 means x_{i1} <> x_{i2}
| ceq : list nat -> nat -> constraint. (* ceq (i1 :: i2 :: ...) k
means x_{i1} + x_{i2} + ... = k *)

(* sum_idx (i_1 :: i_2 :: ...) (x_1 :: x_2 :: ...) = x_{i_1} + x_{i_2} + ... 
*)

Fixpoint sum_idx (is xs : list nat) : nat :=
match is with
| nil => 0
| i :: is' => nth i xs 0 + sum_idx is' xs
end.

(* Note: the following two function create propositions! *)

Definition con_eval (c : constraint) (xs : list nat) : Prop :=
match c with
| cneq i1 i2 => nth i1 xs 0 <> nth i2 xs 0
| ceq is k => sum_idx is xs = k
end.

Fixpoint con_list_eval (cs : list constraint) (xs : list nat) : Prop :=
match cs with
| nil => True
| c :: cs' => con_eval c xs /\ con_list_eval cs' xs
end.

Definition cs1 : constraint := cneq 0 1.
Definition cs2 : constraint := ceq (0 :: 1 :: 2 :: nil) 5.

Theorem t : exists xs : list nat, con_list_eval (cs1 :: cs2 :: nil) xs.
Proof.
exists (1 :: 2 :: 2 :: nil). simpl. repeat split; omega.
Defined.

Record true_con_system := mk_true_con_system {
  cs : list constraint;
  xs : list nat;
  cs_true : con_list_eval cs xs
}.

This is something called reflection; there is a chapter about it in
the Coq book. It is used to prove meta-results by encoding Coq
propositions as Coq datatypes.

Let us know if this does not answer your question.

Evgeny