2 isabelle
我在这里提出的问题是我前一个问题的切线.
对于这些问题,我使用了一个非常简单的引理,尽管我的第二个问题是相当复杂的.
错误"本地语句无法优化任何待定目标"是一个更令人沮丧的错误,当使用show或thus当我的所有逻辑看起来都正确时,所以我试图更好地理解下面发生的错误消息lemma fix_2.
我知道它的修复,这是我的lemma fix_1,但我知道的越多,我在与另一个人交往时就越好"未能完善任何待定的目标".
任何有兴趣的人都可以通过阅读问题来回答Q1和Q2,然后再看两个引理.
我在下面提供了很多信息.我格式化下面的注释,就像我能够比较命令后的方式this和goal更改.这样做,我能够更好地了解什么是与使用的发生的let,def以及fix/assume,其主要目的是尝试在理解错误show的命令lemma fix_2.
我不知道如何提出这样简单的问题.
在这里,我提出了两个问题.你需要跳过来看看lemma let_1和lemma fix_2.我尝试使用HTML锚点在此页面中创建链接,但它不起作用.
Q1:下面lemma let_1,我在使用print_commands.我查看了这些命令,试图找到能够提供有关如何实例化原理图变量的信息的命令.我发现print_binds,这表明我使用了原理图变量?w.是否还有其他命令可以提供有关校样中原理图变量发生情况的信息？
Q2:我说得好吗？
show "card {} = 0"in lemma fix_2,this事实及其隐含假设时card w = 0 [w == {}],用于创建类似于{...}块导入之后lemma fix_1导出的规则,其中导出的规则存在(?w2 == {}) ==> card ?w2 = 0.show "card {} = 0",其中原理图变量被实例化{},但是某些东西不匹配,并且发生错误.def和fix/assume描述这个问题的主要背景是L.Noschinski 关于IsaUserList的声明:
当您使用"fix"或"def"来定义变量时,它们要么只是一般化(即转换为原理图)(修复),要么在块关闭/执行显示时由其右侧(定义)替换.
我部分重申它以显示我对show命令的理解,我所说的也是基于下面的方式def_1和fix_1行为,它们都使用一个{...}块:
如果语句def x == "P"和fix y assume "y == P"被一个之前使用show的命令,如def_2和fix_2下方,在使用的show命令时,将发生以下情况:
def x,事实x中的任何使用都this将被替换P.fix y,将使用this事实及其隐含假设创建规则,例如{...}在fix_1下面的内容之后.在此规则中,y将由原理图变量替换.this,goal,have和show声明
我使用show_question_marks是因为我需要在使用时看到引入逻辑示意图变量的时间fix/assume.
使用show_hyps在方括号中显示了证明事实的隐含假设.使用时,这些隐式条件将在导出的规则fix/assume中使用.
declare[[show_question_marks=true, show_hyps=true]]
declare[[show_sorts=false, show_types=false, show_brackets=false]]
一个基本引理,以及5个没有使用证明事实的变体
基本的引理显示了实际被证明的内容.然后我有以下内容:
let_1看看如何使用let影响this.def_1,使用def和{...}块,看看如何导出def行为和如何this导出.def_2使用之前无法{...}阻挡,能够查看.thisshowfix_1并且fix_2,它们同样是def_1和def_2,但是使用fix/assume.没有证明事实的引理
下面所有的引理都是下一个引理,并且证明是相同的.其他人所拥有的是一个不需要的证明事实,并且不被show命令使用.
证明事实的目的是帮助我了解如何def以及在证明时fix改变this事实have,并看看它们this在块{...}关闭后如何导出.
lemma "card {} = (0::nat)"
proof-
show "card {} = 0"
by(simp)
qed
let_1
lemma let_1: "card {} = (0::nat)"
proof-
let ?w = "{}::'a set" (*No `this` fact: ?w is instantiated as {}.*)
print_commands
print_binds (*term bindings: w? == bot *)
have "card ?w = (0::nat)" (*goal: card {} = 0 *)
by(simp) (*this: card {} = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
def_1,{...}
lemma def_1: "card {} = (0::nat)"
proof-
{def w == "{}::'a set" (*this: w == {} [w == {}] [name "local.w_def"] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
} (*this: card {} = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
def_2,没有阻止
lemma def_2: "card {} = (0::nat)"
proof-
def w == "{}::'a set" (*this: w == {} [w == {}] [name "local.w_def"] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
fix_1,{...}
lemma fix_1: "card {} = (0::nat)"
proof-
{fix w assume "w == {}::'a set" (*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
} (*this: (?w2 == {}) ==> card ?w2 = 0 *)
show "card {} = 0" (*goal: card {} = 0 *)
by(simp)
qed
fix_2,没有阻止
lemma fix_2: "card {} = (0::nat)"
proof-
fix w assume "w == {}::'a set"(*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(?w3 == {}) ==> card {} = 0 *)
oops
140119:
Q2的答案以及错误发生的原因fix_2由L.Paulson说,
证明
fix_2,你有"fix w".这扩展了上下文w.上下文不再匹配目标的原始上下文......
在isar-ref.pdf中搜索了"本地上下文" 之后,我会根据我的理解来完成gofer工作以填写一些细节.
我的Q2的明确答案是,不,我不对,我引用isar-ref.pdf来解释为什么公式(?w3 == {}) ==> card {} = 0在错误信息中.
另一个简短的答案isar-ref.pdf是presume代替assume意志"削弱当地背景"并摆脱错误,因为显然w,正如L.Paulson所描述的那样,背景不再延伸.
为什么我的例子的复杂性 fix_2
我对这个问题的设置是学术,仿佛一位教授说,"在fix_2,修改引理最小的方式来摆脱错误的,而仍然使用fix,尤其不要使用def,obtain或let以消除错误.我使用{...},如同fix_1,是一个可接受的解决方案,但我想进一步了解是什么产生错误信息中的公式fix_2,以帮助我将来.
我对fix/assumein的使用fix_2特定于我在顶部链接的上一个问题.在这里,我介绍了一个证明事实,以确保错误,就像我到达那里,但在这里,我不使用证明事实,简化事情,所以我不必使用from this或thus,但只需要使用show.
在我对前一个问题的回答中,对于手头的引理,我无法理解为什么def什么时候fix/assume没有产生错误.在输出面板的信息几乎是相同那里def和fix/assume,并isar-ref.pdf描述了def作为用于缩写fix/assume,117页,其中,所述关键词是"基本上":
基本上,
def x == t缩写fix x "assume x == t"......
在当地环境中,它就像,并非不重要,这就是说巨大的
在我的脑海里有一个模糊的概念,答案中的某个地方是当地背景的问题,因为我在文档中看到了很多"背景"这个词.知道这就是为什么我在{...}阅读L.Noschinski的提示之后用于解决问题的原因,以及为什么我在L.Paulson的答案之后搜索"本地语境".
(?w3 == {}) ==> card {} = 0我想,为什么在错误信息中
解释见2.2.2结构化陈述中isar-ref.pdf的第34页:
一个简单的陈述由命名命题组成.完整形式允许本地上下文元素后跟实际结论,例如
fixes x assumes "A x" shows "B x".在解除背景后,最终结果成为纯粹的规则:!!x. A x ==> B x.
我在这里假设fixe/assume一个证据的工作类似于fixes/assumes一个引理声明.
我的第一个猜测,而不是我的第二季,正在走上正轨.通过L.Noschinski,我知道w在调用assume "w == {}"时会更改为逻辑示意图变量show,因此错误公式的左侧与公式(?w3 == {}) ==> card {} = 0匹配assume "w == {}",右侧与公式匹配的show "card {} = 0".
我改变了我的猜测上骑自行车,像一个规则fix_1的出口this被创造了,(?w2 == {}) ==> card ?w2 = 0和这?w2与实例化{}.这与之不太匹配(?w3 == {}) ==> card {} = 0,但无论如何都是猜测.
关于当地背景的另外两个引用
由于我的使用fix/assume,在给出了L.Paulson的答案之后,我fix/assume的下一篇引文使我走上正轨,我扩展了背景.
pg.32 in 2.2 Isar证明语言:
剩下的元素
fix并assume构建一个本地上下文(参见§2.2.1),同时show通过嵌套子证明产生的规则细化一个待定的子目标(见§2.2.3).
我在这里的追求主要是试图了解show使用时引擎盖下发生了什么.我仍然在寻求命令给我一些反馈show,通常不会在输出面板中显示:
第6.2.4节目标:
show a: alpha就像have a: alpha加上第二阶段一样,为每一个完成的结果改进一些待定的子目标......
用来presume代替assume
最后,我展示了我的学术练习的另一种解决方案.如果没有L.Paulson的回答fix_2,我在下面引用的内容对我来说没有任何意义,我正在扩展上下文.
第6.3.2页初始和终端证明步骤:
调试这样的情况可能会涉及临时改变
show成have,或通过替换的出现削弱了当地的情况assume通过presume.
lemma fix_3: "card {} = (0::nat)"
proof-
fix w presume "w == {}::'a set"(*this: w == {} [w == {}] *)
from this
have "card w = (0::nat)" (*goal: card w = 0 *)
by(simp) (*this: card w = 0 [w == {}] *)
show "card {} = 0" (*goal: card {} = 0 *)
print_binds (*term bindings:
?this == card w = 0
... == 0
?thesis == card bot = 0 *)
by(simp)
小智 5
你正在制作一些简单而复杂的东西.
在证明中fix_2,你有fix w.这扩展了上下文w.上下文不再与目标的原始上下文匹配,因此show会card {} = 0生成您提到的错误消息.
在这个证明中你真正需要的引理可能是!!w. card w = 0.在证明这个引理时,你将插入fix w一个本地块,它将全部工作.