如何解决无法将变量绑定到已包装的打开公式
首先,对于通常的开放式公式,
Require Import Coq.Init.Nat.
Variable x : nat.
Lemma test1:
~ exists a : nat,let x := a in
x * x = 2.
Proof.
simpl. Admitted.
在a
之后,我看到x
绑定到simpl.
。
1 subgoal
______________________________________(1/1)
~ (exists a : nat,a * a = 2)
现在,我根据formula
编写包装好的开放式Prop
,
进行解包操作f2p
。
Require Import Coq.Init.Nat.
Require Import Lists.List.
Import ListNotations.
(* I: injection,A: and,T: then,S: square *)
Inductive formula := I (p : Prop) | A (f g : formula) | T (p : Prop) (f : formula) | S (f : formula).
(* unwrap formula to prop *)
Fixpoint f2p (f : formula) : Prop :=
match f with
| I p => p
| A f g => f2p(f) /\ f2p(g)
| T p f => p -> f2p(f)
| _ => True
end.
Definition andl (l : list Prop) : Prop :=
fold_left and l True.
Variable x : nat.
Lemma test2:
let l := [I (x*x = 2)] in
~ exists a : nat,let x := a in
andl (map f2p l).
Proof.
unfold andl. simpl.
Admitted.
但是在这种情况下,在a
之后,我看不到x
绑定到simpl.
。
1 subgoal
______________________________________(1/1)
~ (exists _ : nat,True /\ x * x = 2)
解决方法
您看不到它,因为它不会发生。 你有表情
let x := a in andl (map f2p l)
的确将x
定义为a
中的andl (map f2p l)
,但是正如您所见,该术语并未提及x
。它确实提到了另一个名为x
的变量:
Variable x : nat.
但是它们不一样!
在编写let x := a in exp
时,在表达式x := a
的上下文中有一个 local 定义exp
,因此您可以编写let x := a in x * x
,它将减少到a * a
。
您试图做的不是执行局部定义,而是实例化变量,方法是使用函数application。
let l := fun x => [I (x*x = 2)] in
~ exists a : nat,let x := a in
andl (map f2p (l x)).
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。