coq - 在 Coq 中用圆对称求解证明
问题描述
我正在使用结构同余进行证明,其定义与此示例非常相似:
Require Import Nat.
Require Import Omega.
Inductive expr :=
| Const : nat -> expr
| Add : expr -> expr -> expr.
Reserved Notation "e1 === e2" (at level 80).
Inductive expr_congruence : expr -> expr -> Prop :=
| Commutative : forall e1 e2, Add e1 e2 === Add e2 e1
| Associative : forall e1 e2 e3, Add (Add e1 e2) e3 === Add e1 (Add e2 e3)
| CongruenceReflexive : forall e, e === e
| CongruenceSymmetric : forall e1 e2, e1 === e2 -> e2 === e1
| CongruenceTransitive :
forall e1 e2 e3, e1 === e2 -> e2 === e3 -> e1 === e3
where "e1 === e2" := (expr_congruence e1 e2).
我在尝试定义某种形式时遇到了问题forall e1 e2, e1 === e2 -> P e1 -> P e2
:我总是以循环逻辑结束。举个例子:
Inductive is_zero : expr -> Prop :=
| ZConst : is_zero (Const 0)
| ZAdd : forall e1 e2, is_zero e1 -> is_zero e2 -> is_zero (Add e1 e2).
Hint Constructors is_zero expr_congruence.
Lemma is_zero_over_congruence :
forall e1 e2,
e1 === e2 ->
is_zero e1 ->
is_zero e2.
Proof.
induction 1; eauto; intros.
Show 3.
(**
1 subgoal
e1, e2 : expr
H : e1 === e2
IHexpr_congruence : is_zero e1 -> is_zero e2
H0 : is_zero e2
**)
e1
和这里之间的唯一联系e2
是它们是一致的。对它们进行反演或归纳最终会回到相同的情况,这不会提供额外的信息。
当使用以这种方式定义的对称结构时,处理归纳的正确方法是什么?
解决方案
至少在这个最小的例子中,你只需要证明一些更强大的东西:
Lemma is_zero_over_congruence :
forall e1 e2, e1 === e2 -> is_zero e1 <-> is_zero e2.
Proof.
induction 1.
- split; intros HI; inversion HI; eauto.
- split; intros HI; inversion HI; [inversion H1 | inversion H2]; eauto.
- reflexivity.
- symmetry. auto.
- rewrite IHexpr_congruence1, IHexpr_congruence2. reflexivity.
Qed.
以便is_zero e1 <-> is_zero e2
在需要证明时可以作为归纳假设is_zero e2 <-> is_zero e1
。
推荐阅读
- html - Ace Editor 未使用容器 div 调整大小
- java - 如何阻止我的迭代器跳过第一个输入值?
- spring-boot - 无法模拟 RestTemplate.exchange
- assembly - ARM中MSR和MRS指令的扩展是什么
- android - 如何在 ArCore Android 中隐藏 SFB 文件中的子网格
- regex - 如何在 perl 中将 XX1/XXSomething/XX1/Something 之类的模式更改为 XXSomething/XX1/Something
- vb.net - 如何在字符串列表中对字符串类型日期进行排序?
- javascript - 无法为我的反应应用禁用 LiveReloading webapck 开发服务器
- python - 如何获取外键对象以在 django rest 框架中显示完整对象
- activiti - Activiti:添加任务局部变量即席