有会Coq的大神吗？？【数学吧】

数学吧关注：879,114贴子：8,701,318

弱渣求助。

要调整蓝色部分，已有加法交换律
Theorem r2 :
forall (a b:nature),Plus a b = Plus b a.
用什么命令？？

送TA礼物

1楼2014-03-21 21:00回复

表沉啊

2楼2014-03-21 21:13

2024-11-02 07:35广告

再不济也能直接套个replace...with...吧..
好几年没玩这种把人虐成狗的东西了都忘光了....

IP属地:广东

3楼2014-03-21 21:27

收起回复

我来说说正确推荐做法..
试试rewrite (r2 (Mult x y) (Plus z (Mult x z))).

IP属地:广东

4楼2014-03-21 23:35

收起回复

下载贴吧APP
看高清直播、视频！

贴吧热议榜

发表回复

内容:

使用签名档查看全部

发表

保存至快速回贴