ランボー怒りのCoqで自然演繹

なにこれ

自然演繹（古典論理）の推論規則をCoqで導出したものです。関数適用などをなるべく避け、素のCICに近い形にしたつもりです。素人なので「つもり」レベルです。(* *)内はコメントで、Show Proofした際の出力、すなわち、証明に対応するCICの項をCoqからコピペして記載しています。カリーハワードの息遣いを感じてください。

参考にしたものは、software foundations vol.1のlogic foundationのlogic in coqの章です。

先頭でSet Printing All.しておくと、論理和/論理積などが/とかではなくorやandなどの代数的データ型で表示されます。CICの息吹をさらに感じたい人はどうそ。

この記事はまだ完成していません。否定周りの推論規則、forall, existsの推論規則がまだありません。そのうちなんとかする気持ちはあります。

Theorem intro_mp : forall A : Prop, A -> A.
Proof.
  intro A. intro PA. apply PA.
  Show Proof.
  (* (fun (A : Prop) (PA : A) => PA) *)
Qed.

Theorem eliminate_mp : forall A B : Prop, (A -> B) -> A -> B.
Proof.
  intros A B. intros H PA.
  apply H in PA. apply PA. 
  Show Proof.
  (* (fun (A B : Prop) (H : A -> B) (PA : A) => let PA0 : B := H PA in PA0) *)
Qed.

Theorem intro_disjunction_l : forall A  B : Prop, A -> A \/ B .
Proof.
  intros A B. intro PA. 
  apply or_introl. apply PA.
  Show Proof.
  (* (fun (A B : Prop) (PA : A) => or_introl PA) *)
Qed.


Theorem intro_disjunction_r : forall A  B : Prop, B -> A \/ B .
Proof.
  intros A B. intro PB. 
  apply or_intror. apply PB.
  Show Proof.
  (* (fun (A B : Prop) (PB : B) => or_intror PB) *)
Qed.

Theorem eliminate_disjunction  : forall  A : Prop, A \/ A  -> A.
Proof.
  intro A. intro HD. case HD.
  - intro  HA. apply HA.
  - intro  HB. apply HB.
  Show Proof.
  (*
     (fun (A : Prop) (HD : A \/ A) => match HD with
                                      | or_introl HA => HA
                                      | or_intror HB => HB
                                      end)
  *)
Qed.

Theorem intro_conjunction : forall A B : Prop, A -> B -> A /\ B.
Proof.
  intros A B. intros PA PB.
  apply conj.
    - apply PA.
    - apply PB.
  Show Proof.
  (* (fun (A B : Prop) (PA : A) (PB : B) => conj PA PB) *)
Qed.



Theorem eliminate_conjunction_left : forall A B : Prop, A /\ B -> A.
Proof.
  intros A B. intro HA. case HA. 
    - intros PA PB. apply PA.
  Show Proof.
  (*
     (fun (A B : Prop) (HA : A /\ B) => match HA with
                                        | conj PA _ => PA
                                        end)
  *)
Qed.

Theorem eliminate_conjunction_right : forall A B : Prop, A /\ B -> B.
Proof.
  intros A B. intro HA. case HA. 
    - intros PA PB. apply PB.
  Show Proof.
  (*
     (fun (A B : Prop) (HA : A /\ B) => match HA with
                                        | conj _ PB => PB
                                        end)
  *)
Qed.

Theorem ex_falso_quodlibet : forall P : Prop, False ->  P.
Proof.
  intros P contra.
  destruct contra.
  Show Proof.
  (*
     (fun (P : Prop) (contra : False) => match contra return P with
                                         end)
  *)
Qed. 

Theorem intro_negation : forall  P : Prop, P -> False -> False -> P.
Proof.
  intro P. intros HP HC1. intro HC2. apply HP.
  Show Proof.
  (* (fun (P : Prop) (HP : P) (_ _ : False) => HP) *)
Qed. 

Theorem intro_negation_1 : forall  P : Prop, P -> ~~ P.
Proof.
  intros P. unfold not. intro HP. intro H. apply H. apply HP.
  Show Proof.
Qed. 


Theorem intro_negation_2 : forall  P : Prop, (False -> P) -> False -> False -> P.
Proof.
  intro P. intros HP HC1 HC2. apply  HP in HC1. apply HC1.
  Show Proof.
  (* (fun (P : Prop) (HP : False -> P) (HC1 _ : False) => let HC3 : P := HP HC1 in HC3) *)
Qed. 


Theorem eliminate_double_negation : (forall P : Prop, P \/ ~P) -> (forall  P : Prop, ~~P -> P).
Proof.
  intros. specialize (H P). case H.
      + intro HP. apply HP. 
        (*      + exact (match H0 return P with end). *)
      + contradiction.
  Show Proof.
Qed.