[Coq] Coq Advent Calender : omega (6 of 25)

　Coq でよく使われる tactic の６つ目は omega です...ってanarchy proofは課題が数学寄りに偏っているから、順序が６つ目というのはあまり気にしないで下さい。

　omega タクティックはforallとかexistsとかを含まない形のPresburger算術 (Wikipedia)の式を自動証明してくれます。端的に言うと、

• 割り算無し


• 変数と変数の掛け算が入っているものはNG、変数と定数（2, 3などの具体的な整数）の掛け算はOK
  

みたいな感じの等式 or 不等式を証明します。
　Coqがよく使われる理由は、この手の数式関係の自動証明が便利に使えるからだと思います。整数の等式不等式に関する公理定理を組み合わせて証明するとか大変ですからね。

簡単な例はこんなのです。使い方は簡単で、Require Import Omega して、introsとかして、omega と入力するだけ。

Coq < Require Import Omega.

Coq < Lemma Sample_of_omega : forall x:nat, x > 1 -> 3 * x > x + 2.
1 subgoal
  
  ============================
   forall x : nat, x > 1 -> 3 * x > x + 2

Sample_of_omega < intros.
1 subgoal
  
  x : nat
  H : x > 1
  ============================
   3 * x > x + 2

Sample_of_omega < omega.
Proof completed.

　内部で実行された自動証明を見てみると、こんな感じらしい。

Sample_of_omega < Undo.
1 subgoal
  
  x : nat
  H : x > 1
  ============================
   3 * x > x + 2

Sample_of_omega < info omega.
 == refine (Decidable.dec_not_not (3 * x > x + 2) (dec_gt (3 * x) (x + 2)) _);
       intro H0;
       refine ((_:3 * x <= x + 2 -> False) (not_gt (3 * x) (x + 2) H0));
       clear H0; intro H0;
       refine ((_:(Z_of_nat x > Z_of_nat 1)%Z -> False) (inj_gt x 1 H));
       change ((Z_of_nat x > 1)%Z -> False); clear H; 
    intro H;
       refine ((_:(Z_of_nat (3 * x) <= Z_of_nat (x + 2))%Z -> False)
                 (inj_le (3 * x) (x + 2) H0));
       refine ((fun (P : Z -> Prop) (H : P (Z_of_nat 3 * Z_of_nat x)%Z) =>
                eq_ind_r P H (inj_mult 3 x))
                 (fun x0 : Z => (x0 <= Z_of_nat (x + 2))%Z -> False) _);
       change ((3 * Z_of_nat x <= Z_of_nat (x + 2))%Z -> False);
       refine ((fun (P : Z -> Prop) (H : P (Z_of_nat x + Z_of_nat 2)%Z) =>
                eq_ind_r P H (inj_plus x 2))
                 (fun x0 : Z => (3 * Z_of_nat x <= x0)%Z -> False) _);
       change ((3 * Z_of_nat x <= Z_of_nat x + 2)%Z -> False); 
    clear H0; intro H0; refine (ex_ind _ (intro_Z x)); 
    intro Zvar2; intro Omega11; refine (and_ind _ Omega11); 
    clear Omega11; intro Omega8; intro Omega11;
       refine ((_:(0 <= Z_of_nat x + -1 + - (1))%Z -> False)
                 (Zgt_left (Z_of_nat x) 1 H)); clear H;
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x : Z => (0 <= x + -1 + - (1))%Z -> False) _);
       change ((0 <= Zvar2 + -1 + -1)%Z -> False);
       refine (fast_Zplus_assoc_reverse Zvar2 (-1) 
                 (-1) (fun x : Z => (0 <= x)%Z -> False) _);
       change ((0 <= Zvar2 + -2)%Z -> False);
       refine (fast_Zred_factor0 Zvar2
                 (fun x : Z => (0 <= x + -2)%Z -> False) _); 
    intro Omega10;
       refine ((_:(0 <= Z_of_nat x + 2 + - (3 * Z_of_nat x))%Z -> False)
                 (Zle_left (3 * Z_of_nat x) (Z_of_nat x + 2) H0)); 
    clear H0;
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x0 : Z => (0 <= x0 + 2 + - (3 * Z_of_nat x))%Z -> False)
                 _);
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x : Z => (0 <= Zvar2 + 2 + - (3 * x))%Z -> False) _);
       refine (fast_Zmult_comm 3 Zvar2
                 (fun x : Z => (0 <= Zvar2 + 2 + - x)%Z -> False) _);
       refine (fast_Zopp_mult_distr_r Zvar2 3
                 (fun x : Z => (0 <= Zvar2 + 2 + x)%Z -> False) _);
       change ((0 <= Zvar2 + 2 + Zvar2 * -3)%Z -> False);
       refine (fast_Zplus_comm (Zvar2 + 2) (Zvar2 * -3)
                 (fun x : Z => (0 <= x)%Z -> False) _);
       refine (fast_Zplus_assoc (Zvar2 * -3) Zvar2 2
                 (fun x : Z => (0 <= x)%Z -> False) _);
       refine (fast_Zred_factor3 Zvar2 (-3)
                 (fun x : Z => (0 <= x + 2)%Z -> False) _);
       change ((0 <= Zvar2 * Zneg (3 - 1) + 2)%Z -> False); 
    intro Omega9;
       cut ((Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z);[intro H|idtac].
    refine ((_:(Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z -> False) H);
       clear H; intro auxiliary;
       refine ((_:(0 <= (Zvar2 * -1 + 1) * 2 + 0)%Z -> False)
                 (OMEGA1 (Zvar2 * -2 + 2) ((Zvar2 * -1 + 1) * 2 + 0)
                    auxiliary Omega9)); clear auxiliary Omega9; 
    intro Omega9;
       cut (2 > 0)%Z;[intro H|idtac].
    refine ((_:(2 > 0)%Z -> False) H); clear H;
       cut (2 > 0)%Z;[intro H|idtac].
    refine ((_:(2 > 0)%Z -> (2 > 0)%Z -> False) H); 
    clear H; intro auxiliary_1; intro auxiliary_2;
       refine ((_:(0 <= Zvar2 * -1 + 1)%Z -> False)
                 (Zmult_le_approx 2 (Zvar2 * -1 + 1) 0 auxiliary_1
                    auxiliary_2 Omega9));
       clear auxiliary_1 auxiliary_2 Omega9; intro Omega9;
       refine ((_:(0 <= Zvar2 * 1 + -2 + (Zvar2 * -1 + 1))%Z -> False)
                 (OMEGA2 (Zvar2 * 1 + -2) (Zvar2 * -1 + 1) Omega10 Omega9));
       refine (fast_OMEGA13 Zvar2 (-2) 1 1 (fun x : Z => (0 <= x)%Z -> False)
                 _); change ((0 <= Zneg (2 - 1))%Z -> False);
       change ((0 ?= Zneg (2 - 1))%Z <> Gt -> False);
       change (Gt <> Gt -> False); intro H; refine (False_ind False _);
       cut (Gt = Gt);[intro H0|idtac].
    refine ((_:Gt = Gt -> False) H0); clear H0;
       cut (Gt <> Gt);[intro H0|idtac].
    refine ((_:Gt <> Gt -> Gt = Gt -> False) H0); clear H0; 
    intro H0; intro H1; exact (H0 H1).
    
    exact H.
    
    change (Gt = Gt); exact (refl_equal Gt).
    
    change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
       exact (refl_equal Gt).
    
    change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
       exact (refl_equal Gt).
    
    refine (fast_OMEGA11 Zvar2 (-1) 1 0 2
              (fun x : Z => (Zvar2 * -2 + 2)%Z = x) _);
       change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
       change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
       exact (refl_equal (Zvar2 * -2 + 2)%Z).
    
Proof completed.

Sample_of_omega <