小编fra*_*ala的帖子

情况就是这样:我有两个表,其中一个引用另一个表(例如,table2引用table1).在创建这些表时,我确实将外键约束设置为DEFERRABLE,将ON UPDATE和ON DELETE子句设置为NO ACTION(这是默认值).

但是,当运行下面的事务时,我收到以下错误.

交易:

START TRANSACTION;
SET CONSTRAINTS ALL DEFERRED;
UPDATE table1 SET blah blah;
UPDATE table2 SET blah blah;
COMMIT;

错误:

ERROR:  update or delete on table "table1" violates foreign key constraint "table1_column_fkey" on table "table2"
DETAIL:  Key (column1)=(blahblah) is still referenced from table "table2".

和桌子结构:

CREATE TABLE table1(
    column1 CHAR(10),
    [...]
    PRIMARY KEY (column1)
);

CREATE TABLE table2(
    primkey CHAR(9),
    [...]
    column2 CHAR(10) NOT NULL,
    PRIMARY KEY(primkey),
    FOREIGN KEY(column2) REFERENCES table1(column1) DEFERRABLE
);

我想要做的是在事务进行时推迟外键检查,直到它提交为止.我只是看不出为什么这个错误会返回,我怎么能让事务工作.

match goal with当在用户定义的策略中进行模式匹配（with ）时，我们可以使用?x绑定一个 Gallina term，以便稍后我们可以引用它。我们可以在一个子句中使用多个这样的标识符 ( ... ?x ... ?y ...)，甚至可以使用相同的标识符 ( ... ?x ... ?x ...) 来指示为了使子句匹配，相同的 Gallina 术语必须出现在这两个位置中。在某种程度上，这限制了与“相同性”要求的可能匹配。这很方便，但如果还能够提出“不同”的要求，那就更方便了（原文如此）。有没有一种方法可以编写形式的匹配子句，其中我们要求和... ?x ... ?y ...所约束的术语是可区分的？?x?y

我所说的可区分并不一定意味着不相等，而只是不同（它们的名称[或表示]不一致）。例如，假设我有两个术语a,b:C。从我们可以证明命题 的意义上来说，这两个术语可能是相等的a = b，但这与我的目的无关。彼此的区别在于它们的名称a不同。b

?x那么，我可以通过提出两个元变量和?y必须绑定不同术语的要求来进行模式匹配吗？

为了将其置于某种上下文中，假设我们已经定义了对、投影和 letR是某种（适当类型的）二元关系。假设我以某种方式最终得到以下两个假设。

H  : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a

我希望能够在我的策略中编写一个仅匹配H而不匹配的匹配子句H'。有什么窍门吗？

如果没有办法只匹配H，那么也许我可以匹配两者，我绑定a到?x …