如何解决Z_3:左反转引理
我被困住了。我想证明Z_3的左反转引理
(* aux lemma)
Lemma Z_3_inv_lemma (k: nat) : ((3 + k) <? 3 = true) -> False.
Proof.
intro. induction k as [| k' IH].
- simpl in H. inversion H.
- rewrite Nat.add_succ_r in H. auto.
Qed.
(* main theorem *)
Proposition Z3_left_inv : forall x: Z_3,Z3_op (Z_3_inv x) x = z3_0.
Proof.
intro. unfold Z3_op. destruct x as [vx prf]. unfold z3_0. apply Z3_eq. destruct vx as [| vx'].
- simpl. reflexivity.
- destruct vx'.
+ simpl. reflexivity.
+ destruct vx'.
* simpl. reflexivity.
* revert prf. rewrite <- Nat.add_1_l. rewrite <- (Nat.add_1_l (S vx')). rewrite <- (Nat.add_1_l vx'). repeat rewrite Nat.add_assoc. change (1+1+1) with 3. intro.
结果:
1 subgoal (ID 153)
vx' : nat
prf : (3 + vx' <? 3) = true
============================
(Z_3_inv {| n := 3 + vx'; proof := prf |} +
{| n := 3 + vx'; proof := prf |}) mod 3 = 0
我想通过使用Z_3_inv_lemma来完成证明并在上下文中得到False。但是当我执行apply Z_3_inv_lemma in prf.
时,会出现错误:
Error: Cannot change prf,it is used in conclusion.
解决方法
我相信您可以尝试pose proof (Z_3_inv_lemma vx' prf)
,这应该使您可以使用False
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。