从所有人那里获得功能是事实

问题描述

我的目标是从形式∀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证明，没有任何理由，除了它已经过时而且没有人去做。就是说，这当然意味着相当多的实施工作，而我遇到这种情况的机会相对很少，并且上面手工进行选择的样板还不错。

但是为此实现自动化当然会很好！