述語論理版パースの法則 in Coq

peirce.v

Lemma col: forall P Q:nat->Prop, (forall x:nat,P x -> False) -> (forall x:nat, (forall z:nat, (P z->Q z)) -> P x) -> forall x:nat, P x .
Proof.
intros.
apply (H0 x).
intros.
apply (H z) in H1.
tauto.
Qed.

test4.v

Require Import Arith.
Require Import Nat.

(* ClassicalFacts.em の代わりに、直接排中律を公理として宣言 *)
Axiom excluded_middle_axiom : forall (X : Prop), ~X \/ X.

Axiom A : nat -> Prop. (* 完全と拡張は同じ行先 *)
Axiom B : nat -> Prop. (* x はコラッツで 1 に辿り着く *)

(* P x の定義: ~A x \/ ~B x *)
Definition P (x : nat) : Prop := ~A x \/ ~B x.
(* ３.４. *)
Axiom axiom_descent_case_A:
  forall x : nat, 0 < x         -> ~A (pred x) -> exists y : nat, y < x /\ P y.
(* １. *)
Axiom axiom_descent_case_A2:
  forall x : nat, 0 < x -> ~A x ->  A (pred x) -> exists y : nat, y < x /\ P y.
(* ２. *)
Axiom axiom_descent_case_B:
  forall x : nat, 0 < x -> ~B x ->  A (pred x) -> exists y : nat, y < x /\ P y.
Axiom P_0_is_false : ~ P 0.

(* --- 無限降下法 --- *)
Lemma hoge2_corrected : forall x : nat, P x -> exists y : nat, y < x /\ P y.
Proof.
  intros x H_Px. (* H_Px は ~A x \/ ~B x *)

  (* x = 0 の場合と x > 0 の場合で分岐します *)
  destruct x as [| x'].
  - exfalso. (* 矛盾を導入 *)
    apply P_0_is_false. (* P_0_is_false は ~P 0 なので P 0 が与えられると矛盾 *)
    exact H_Px. (* H_Px は P 0 (P x が P 0 になっている) *)

  - destruct (excluded_middle_axiom (A x')) as [H_not_A_x2 | H_A_x2].
    * apply (axiom_descent_case_A (S x')).
      -- apply Nat.lt_0_succ.
      -- rewrite (Nat.pred_succ x').
         exact H_not_A_x2.
    * destruct H_Px as [H_not_A_x | H_not_B_x].
      + apply (axiom_descent_case_A2 (S x')).
        -- apply Nat.lt_0_succ.
        -- exact H_not_A_x.
        -- rewrite (Nat.pred_succ x').
           exact H_A_x2.
      + apply (axiom_descent_case_B (S x')).
        -- apply Nat.lt_0_succ.
        -- exact H_not_B_x.
        -- rewrite (Nat.pred_succ x').
           exact H_A_x2.
Qed.



(* ClassicalFacts.em の代わりに、直接排中律を公理として宣言
Axiom excluded_middle_axiom : forall (P : Prop), P \/ ~P.

Axiom A : nat -> Prop.
Axiom B : nat -> Prop.

(* --- 降下を保証するための新しい公理群 --- *)

(* P x の定義: ~A x \/ ~B x *)
Definition P (x : nat) : Prop := ~A x \/ ~B x.

(* 公理 1: A x かつ ~B x の場合、より小さい y で P y となるものが見つかる *)
(* これは、特定の「反例の形」からの降下を保証します *)
Axiom axiom_descent_case_B:
  forall x : nat, 0 < x -> A x -> ~B x -> exists y : nat, y < x /\ P y.

(* 公理 2: ~A x の場合、より小さい y で P y となるものが見つかる *)
(* これは、もう一つの「反例の形」からの降下を保証します
   例えば、A x が偽なら、x-1 も A が偽である、といったような性質を想定します。
   0 < x の前提は、x が 0 の場合を除くためです。*)
Axiom axiom_descent_case_A:
  forall x : nat, 0 < x -> ~A x -> exists y : nat, y < x /\ P y.

(* --- 補足的な公理 (もし P 0 が真の場合に矛盾を導くため) --- *)
(* 無限降下法では、0 が反例にならないことを示す必要があります。
   もし P 0 が真であれば、矛盾を導く公理が必要です。
   例として、P 0 は決して成り立たない、という公理を置きます。
   これは、あなたが証明したい「最終的な定理」から導かれるべきですが、
   ここでは説明のために公理とします。
*)
Axiom P_0_is_false : ~ P 0.

(* --- あなたの目標 Lemma hoge1 の修正版 --- *)
Lemma hoge1_corrected : forall x : nat, P x -> exists y : nat, y < x /\ P y.
Proof.
  intros x H_Px. (* H_Px は ~A x \/ ~B x *)

  (* x = 0 の場合と x > 0 の場合で分岐します *)
  destruct x as [| x_pred].
  - (* x = 0 の場合 *)
    (* Goal: P 0 -> exists y : nat, y < 0 /\ P y.
       しかし、y < 0 を満たす自然数は存在しないため、
       exists y, y < 0 /\ P y は常に偽です。
       したがって、P 0 -> (偽) が真であるためには、P 0 が偽でなければなりません。
       これは、P_0_is_false 公理と矛盾します。
    *)
    exfalso. (* 矛盾を導入 *)
    apply P_0_is_false. (* P_0_is_false は ~P 0 なので P 0 が与えられると矛盾 *)
    exact H_Px. (* H_Px は P 0 (P x が P 0 になっている) *)

  - (* x = S x_pred (つまり x > 0) の場合 *)
    (* Goal: P (S x_pred) -> exists y : nat, y < (S x_pred) /\ P y.
       H_Px は P (S x_pred) です。
    *)
    destruct H_Px as [H_not_A_x | H_not_B_x].
    + (* ケース 1: H_not_A_x が真 (~A (S x_pred)) の場合 *)
      (* ここで axiom_descent_case_A を使います。
         前提: 0 < (S x_pred) と ~A (S x_pred).
         0 < (S x_pred) は Nat.lt_0_succ で証明できます。
         ~A (S x_pred) は H_not_A_x です。 *)
      apply (axiom_descent_case_A (S x_pred)).
      * (* サブゴール 1: 0 < S x_pred を示す *)
        apply Nat.lt_0_succ.
      * (* サブゴール 2: ~A (S x_pred) を示す *)
        exact H_not_A_x.
    + (* ケース 2: H_not_B_x が真 (~B (S x_pred)) の場合 *)
      (* このケースでは、A (S x_pred) であるか否かで分岐する必要があります。
         axiom_descent_case_B は A x を前提とするからです。 *)
      destruct (excluded_middle_axiom (A (S x_pred))) as [H_A_x | H_not_A_x'].
      * (* サブケース 2.1: A (S x_pred) が真の場合 *)
        (* axiom_descent_case_B を使います。
           前提: 0 < (S x_pred), A (S x_pred), ~B (S x_pred).
        *)
        apply (axiom_descent_case_B (S x_pred)).
        -- (* サブゴール 1: 0 < S x_pred を示す *)
           apply Nat.lt_0_succ.
        -- (* サブゴール 2: A (S x_pred) を示す *)
           exact H_A_x.
        -- (* サブゴール 3: ~B (S x_pred) を示す *)
           exact H_not_B_x.
      * (* サブケース 2.2: ~A (S x_pred) が真の場合 *)
        (* これはケース 1 と同じロジックになります (~A x の場合)。
           axiom_descent_case_A を使います。
        *)
        apply (axiom_descent_case_A (S x_pred)).
        -- (* サブゴール 1: 0 < S x_pred を示す *)
           apply Nat.lt_0_succ.
        -- (* サブゴール 2: ~A (S x_pred) を示す *)
           exact H_not_A_x'.
Qed. *)



(*
x>0 の完全割数列と拡張完全割数列は異なる行先 \/ x>0 はコラッツで 1 に辿り着かない
という最小反例を考える。
x に 拡張star変換 を施して y<x を得る。
y に 排中律 を施して y の完全と拡張は同じ行先 \/ y の完全と拡張は異なる行先 を得る。
4つ の場合分けをおこなう。
　１. x の完全と拡張は異なる行先      /\ y の完全と拡張は同じ行先
　　　　→ 2段階の拡張star を一回の 拡張star と見なすと、y の完全と拡張は異なる行先 になるので、より小さい反例が得られる
　２. x はコラッツで 1 に辿り着かない /\ y の完全と拡張は同じ行先
　　　　→ y もコラッツで 1 に辿り着かない 事になるので、より小さい反例が得られる
　３. x の完全と拡張は異なる行先      /\ y の完全と拡張は異なる行先　→より小さい反例
　４. x はコラッツで 1 に辿り着かない /\ y の完全と拡張は異なる行先　→より小さい反例
いずれも、より小さい反例が得られる。  □
*)

１. における拡張star変換の"すりかえ"