形式手法に興味がありCoqを勉強中。教科書として使っているのはこの本。
Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions
とりあえず4章の練習問題までやってみる。
Require Import Arith.
Require Import ZArith.
Require Import Bool.
Open Scope nat_scope.
Open Scope Z_scope.

(* Exercise 2.1 *)

Check (plus 3).
Check (Zmult (-5)).
(* Check Zabs_nat. 関数が無い？バージョン違いによるものか？ *)
(* Check (mult 3 (-45)%Z). *)

(* Exercise 2.2 *)
Check (fun a b c:Z => (b*b-4*a*c)%Z).

(* Exercise 2.3 *)
Check (fun (f g:nat -> nat)(n:nat) => g (f n)).

(* Exercise 2.4 *)
Check (fun n p: nat => 
  (let diff := n(*Var*)-p(*Var*)(*App*)
 in(*Let-in*)
   let square := diff(*Var*)*diff(*Var*)(*App*)
 in(*Let-in*)
   square(*Var*) * (square(*Var*)+n(*Var*)(*App*))(*App*))%nat)(*Lam*)(*Lam *).
(*Var 7回*)
(*App 4回*)
(*Lam 2回*)
(*Let-in 2回*)

(* Exercise 2.5 *)
Definition five_sum (a b c d e: Z) := a+b+c+d+e.

(* Exercise 2.6 *)
Section five_sum.
Variable a b c d e: Z.
Definition five_sum_result := a+b+c+d+e.
End five_sum.
Print five_sum_result.

(* Exercise 2.7 *)
Definition poly := (fun (x: Z) => (Zplus (Zplus (Zmult (Zmult 2 x) x) (Zmult 3 x)) 3)).
Eval compute in poly 2.
Eval compute in poly 3.
Eval compute in poly 4.

(* Exercise 3.1 *)
Hypothesis P Q R: Prop.
Check ((P(*Var*) ->(*Prod-Prop*) Q(*Var*)) ->(*Prod-Prop*) 
  (Q(*Var*) ->(*Prod-Prop*) R(*Var*)) ->(*Prod-Prop*) P(*Var*) ->(*Prod-Prop*) R(*Var*)).

(* Exercise 3.2 *)
Lemma id_P : P -> P.
intro P.
assumption.
Qed.

Lemma id_PP : (P -> P) -> (P -> P).
intro PtoP.
assumption.
Qed.

Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R.
intros PtoQ QtoR P.
apply (QtoR (PtoQ P)).
Qed.

Lemma imp_perm : (P -> Q -> R) -> (Q -> P -> R).
intros PtoQtoR Q P.
apply (PtoQtoR P Q).
Qed.

Lemma ignore_Q : (P -> R) -> P -> Q -> R.
intros PtoR P Q.
apply (PtoR P).
Qed.

Lemma delta_imp : (P -> P -> Q) -> P -> Q.
intros PtoPtoQ P.
apply (PtoPtoQ P P).
Qed.

Lemma delta_impR : (P -> Q) -> (P -> P -> Q).
intros PtoQ P1 P2.
apply (PtoQ P1).
Qed.

Hypothesis T: Prop.
Lemma diamond : (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T.
intros PtoQ PtoR QtoRtoT P.
apply (QtoRtoT (PtoQ P) (PtoR P)).
Qed.

Lemma weak_peirce : ((((P -> Q) -> P) -> P) -> Q) -> Q.
intros.
apply H.
intros.
apply H0.
intro.
apply H.
intros.
assumption.
Qed.

(* Exercise 3.3 *)
Lemma id_P' : P -> P.
intro P; assumption.
Qed.

Lemma id_PP' : (P -> P) -> (P -> P).
intro PtoP; assumption.
Qed.

Lemma imp_trans' : (P -> Q) -> (Q -> R) -> P -> R.
intros PtoQ QtoR P; apply (QtoR (PtoQ P)).
Qed.

Lemma imp_perm' : (P -> Q -> R) -> (Q -> P -> R).
intros PtoQtoR Q P; apply PtoQtoR; [assumption | assumption].
Qed.

Lemma ignore_Q' : (P -> R) -> P -> Q -> R.
intros PtoR P Q; apply PtoR; assumption.
Qed.

Lemma delta_imp' : (P -> P -> Q) -> P -> Q.
intros PtoPtoQ P; apply (PtoPtoQ P P).
Qed.

Lemma delta_impR' : (P -> Q) -> (P -> P -> Q).
intros PtoQ P1 P2; apply (PtoQ P1).
Qed.

Lemma diamond' : (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T.
intros PtoQ PtoR QtoRtoT P; apply (QtoRtoT (PtoQ P) (PtoR P)).
Qed.

Lemma weak_peirce' : ((((P -> Q) -> P) -> P) -> Q) -> Q.
intros; apply H; intros; apply H0; intro; apply H; intros; assumption.
Qed.

(* Exercise 3.4 *)
(* skip *)


(* Exercise 3.5 *)
Section section_for_cut_example.
  Hypothesis (H: P -> Q) (H0 : Q -> R) (H1 : (P -> R) -> T -> Q) (H2 : (P -> R) -> T).
  Theorem cut_example : Q.
  cut (P -> R).
  intro H3.
  apply H1; [assumption | apply H2; assumption].
  intro; apply H0; apply H; assumption.
  Qed.
End section_for_cut_example.

Section section_example_without_cut.
  Hypothesis (H: P -> Q) (H0 : Q -> R) (H1 : (P -> R) -> T -> Q) (H2 : (P -> R) -> T).
  Theorem without_cut_example : Q.
  apply H1.
  intro.
  apply H0; apply H; assumption.
  apply H2.
  intro.
  apply H0; apply H; assumption.
  Qed.
End section_example_without_cut.

Print cut_example.
Print without_cut_example.


(* Exercise 3.6 *)
Theorem auto_depth6: (((((((((P -> Q) -> Q) -> Q) -> Q) -> Q) -> Q) -> Q) -> Q) -> Q) -> P -> Q.
auto 6.
Qed.

(* Exercise 4.1 *)
Open Scope nat_scope.
Definition ex4_1: (nat -> nat) -> Prop := fun f => f 0 > 0.
Definition ex4_2: (nat -> nat) -> (nat -> nat) -> Prop := fun f1 f2 => f1 (f2 0) > 0.
Parameter some_relation : nat -> nat -> Set.
Definition ex4_3: nat -> nat -> Set := some_relation.

(* Exercise 4.2 *)
Definition compose {A B C:Set} (f:A->B)(g:B->C)(a:A) := g (f a).
Definition thrice {A: Set} (f: A->A) := compose f (compose f f).

Check (thrice S).


(* Exercise 4.3 *)
Section A_declared.
  Variables (A:Set)(P Q:A->Prop)(R:A->A->Prop).
  Theorem all_perm : (forall a b:A, R a b)-> forall a b:A, R b a.
  intros.
  apply (H b a).
  Qed.

  Theorem all_imp_dit : (forall a:A, P a -> Q a) -> (forall a:A, P a) -> forall a: A, Q a.
  intros.
  apply H.
  exact (H0 a).
  Qed.

  Theorem all_delta : (forall a b:A, R a b) -> forall a:A, R a a.
  intros.
  apply (H a a).
  Qed.
End A_declared.


(* Exercise 4.4 *)
Definition id: forall A:Set, A -> A := fun A (a: A) => a.
Definition diag: forall A B:Set, (A->A->B)->A->B := fun A B f a => f a a.
Definition permute: forall A B C:Set, (A->B->C)->B->A->C := fun A B C f b a => f a b.
Definition f_nat_Z: forall A:Set, (nat -> A) -> Z -> A := fun A f z => f 0.

(* Exercise 4.5 *)
Theorem all_perm': forall (A: Type) (P:A -> A -> Prop), (forall x y:A, P x y) -> forall x y:A, P y x.
intros.
exact (H y x).
Qed.
Print all_perm'.

Theorem resolution: forall (A: Type) (P Q R S:A->Prop), (forall a:A, Q a->R a->S a)->(forall b:A, P b->Q b)->(forall c:A, P c->R c->S c).
intros.
apply (H c).
apply (H0 c).
assumption.
assumption.
Qed.
Print resolution.
この辺りまではまだ標準的な命題論理や述語論理という感じであまり面白味はない…。Inductive Typeが出てくる辺りから面白くなりそう。