如何解决从所有人那里获得功能是事实
我的目标是从形式∀x的事实中获得函数常数f。 y P x y使得∀x。 P x(f x)。这是我手动执行的操作:
theory Choose
imports
Main
begin
lemma
fixes P :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
shows True
proof -
(* Somehow obtained this fact *)
have I: "∀ n m :: nat . ∃ i j k . P n m i j k"
by sorry
(* Have to do the rest by hand *)
define F
where "F ≡ λ n m . SOME (i,j,k) . P n m i j k"
define i
where "i ≡ λ n m . fst (F n m)"
define j
where "j ≡ λ n m . fst (snd (F n m))"
define k
where "k ≡ λ n m . snd (snd (F n m))"
have "∀ n m . P n m (i n m) (j n m) (k n m)"
(* prove manually (luckily sledgehammer finds a proof)*)
(*...*)
qed
(* or alternatively: *)
lemma
fixes P :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
shows True
proof -
(* Somehow obtained this fact *)
have I: "∀ n m :: nat . ∃ i j k . P n m i j k"
by sorry
obtain i j k where "∀ n m . P n m (i n m) (j n m) (k n m)"
(* sledgehammer gives up (due to problem being too higher order?) *)
(* prove by hand :-( *)
(*...*)
qed
如何更符合人体工程学?伊莎贝尔有类似的东西吗 精益选择策略(https://leanprover-community.github.io/mathlib_docs/tactics.html#choose)? (Isabelles规范命令仅在顶层:-()上起作用。
(很抱歉,如果已经问过这个问题,我没有找到一个很好的流行词来搜索此问题)
解决方法
我认为没有什么可以使该用例自动化。您可以通过直接使用SOME
规则来避免摆弄choice
;它可以让您将“∀∃”变成“∃∀”。但是,您仍然必须将P
从具有5个参数的curried属性转换为带有两个参数的元组,然后再重新包装结果。我没有解决的办法。这就是我要做的:
let ?P' = "λ(n,m). λ(i,j,k). P n m i j k"
have I: "∀n m. ∃i j k. P n m i j k"
sorry
hence "∀nm. ∃ijk. ?P' nm ijk"
by blast
hence "∃f. ∀nm. ?P' nm (f nm)"
by (rule choice) (* "by metis" also works *)
then obtain f where f: "?P' (n,m) (f (n,m))" for n m
by auto
define i where "i = (λn m. case f (n,m) of (i,k) ⇒ i)"
define j where "j = (λn m. case f (n,k) ⇒ j)"
define k where "k = (λn m. case f (n,k) ⇒ k)"
have ijk: "P n m (i n m) (j n m) (k n m)" for n m
using f[of n m] by (auto simp: i_def j_def k_def split: prod.splits)
原则上,我相信这可以自动化。我认为specification
命令只适用于顶层,而不适用于本地环境,甚至不适用于Isar证明,没有任何理由,除了它已经过时而且没有人去做。就是说,这当然意味着相当多的实施工作,而我遇到这种情况的机会相对很少,并且上面手工进行选择的样板还不错。
但是为此实现自动化当然会很好!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。