小编Mat*_*aty的帖子

我试图(经典地)证明

~ (forall t : U, phi) -> exists t: U, ~phi

在Coq.我想要做的是证明它是相反的:

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

我的问题是第(2)和(5)行.我无法弄清楚如何选择U的任意元素,证明它的一些东西,并得出一个结论.

任何建议(我不承诺使用对立面)？

我正在尝试使用Function来定义使用度量的递归定义,并且我收到错误:

Error: find_call_occs : Prod

我在底部发布了整个源代码,但我的功能是

Function kripke_sat (M : kripke) (s : U) (p : formula) {measure size p}: Prop :=
match p with
| Proposition p'  => L M (s)(p')
| Not p' => ~ kripke_sat M s p'
| And p' p''   => kripke_sat M s p' /\ kripke_sat M s p''
| Or p' p''  => kripke_sat M s p' \/ kripke_sat M s p''
| Implies p' p''  => ~kripke_sat M s p' \/  kripke_sat …