task10.v

Parameter G : Set.
Parameter mult : G -> G -> G.
Notation "x * y" := (mult x y).
Parameter one : G.
Notation "1" := one.
Parameter inv : G -> G.
Notation "/ x" := (inv x).
(* Notation "x / y" := (mult x (inv y)). *) (* 使ってもよい *)

Axiom mult_assoc : forall x y z, x * (y * z) = (x * y) * z.
Axiom one_unit_l : forall x, 1 * x = x.
Axiom inv_l : forall x, /x * x = 1.

Theorem left_law1 : forall x y z : G , x = y -> z * x = z * y.
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

Theorem left_law2 : forall x y z : G , z * x = z * y -> x = y.
Proof.
 intros.
 rewrite <- (one_unit_l x).
 rewrite <- (one_unit_l y).
 rewrite <- (inv_l z ).
 rewrite <- (mult_assoc (/z) z x).
 rewrite H.
 rewrite (mult_assoc (/z) z y).
 reflexivity.
Qed.

Lemma one_unit_r : forall x, x * 1 = x.
Proof.
  intros.
  apply (left_law2 (x*1) x (/x)).
  rewrite (mult_assoc (/x) x 1 ).
  rewrite inv_l.
  rewrite one_unit_l.
  reflexivity.
Qed.


Lemma inv_r : forall x, x * / x = 1.
Proof.
  intros.
  rewrite (left_law2 (x*(/x)) 1 (/x)).
  reflexivity.
  rewrite (mult_assoc (/x) x (/x) ).
  rewrite inv_l.
  rewrite one_unit_r.
  rewrite one_unit_l.
  reflexivity.
Qed.

task13.v

Inductive pos : Set :=
  | S0 : pos
  | S : pos -> pos.

Fixpoint plus(n m:pos) : pos :=
  match n with
  | S0 => m
  | S p => S( plus p m )
  end.

Infix "+" := plus.

Theorem plus_assoc : forall n m p, n + (m + p) = (n + m) + p.
Proof.
  intros.
  induction n.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

task14.v

Require Import Arith.

Theorem FF: ~exists f, forall n, f (f n) = S n.
Proof.
  unfold not.
  intros.
  decompose [ex] H.
  assert (exists x0 : nat , (x 0) = x0).
  exists (x 0).
  reflexivity.
  decompose [ex] H1.
  assert (x(x 0) = 1).
  apply H0.
  assert (x(x0) = 1 ).
  rewrite <- H2.
  apply H3.
  assert ( forall a : nat , x a = x0 + a ).
  induction a.
  rewrite H2.
  apply (plus_n_O x0).
  assert  (x (x0 + a) = S a).
  rewrite <- IHa.
  apply H0.
  assert (x (x (x0 + a)) = x( S a ) ).
  rewrite H5.
  reflexivity.
  rewrite (H0 (x0 + a)) in H6.
  rewrite (plus_n_Sm x0 a) in H6.
  rewrite H6.
  reflexivity.
  assert ( x x0 = x0 + x0 ).
  apply H5.
  assert( x0 + x0 = 1 ).
  rewrite <- H6.
  rewrite H4.
  reflexivity.
  apply (odd_even_lem 0 x0 ).
  simpl.
  rewrite( plus_assoc x0 x0 0).
  symmetry.
  rewrite H7.
  reflexivity.
Qed.

task16.v

Definition tautology : forall P : Prop, P -> P
  := fun (P : Prop) (H : P) => H.

Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun (P Q : Prop) (H : ~Q /\ (P -> Q)) (H0 : P) =>
       match H with
         | conj H1 H2 => H1 (H2 H0)
       end.

Definition Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q
  := fun (P Q : Prop) (H : P \/ Q) (H0 : ~ P) =>
       match H with
         | or_introl H1 => False_ind Q (H0 H1)
         | or_intror H1 => H1
       end.

Definition tautology_on_Set : forall A : Set, A -> A
  := fun (A : Set) (H : A) => H.

Definition Modus_tollens_on_Set : forall A B : Set, (B -> Empty_set) * (A -> B) -> (A -> Empty_set)
  := fun (A B : Set) (H : (B -> Empty_set) * (A -> B)) (H0 : A) =>
       let (e, b) := H in e (b H0).

Definition Disjunctive_syllogism_on_Set : forall A B : Set, (A + B) -> (A -> Empty_set) -> B
  := fun (A B : Set) (H : A + B) (H0 : A -> Empty_set) =>
       match H with
         | inl a => Empty_set_rec (fun _ : Empty_set => B) (H0 a)
         | inr b => b
       end.

task17.v

Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  (* 例 : 最初の1行は refine (fun P Q R => _). に置き換えられる *)
  refine (fun P Q R => _).
  refine (fun H => _ ).
  refine (match H with or_introl HP => _ | or_intror HnQR => _ end).
  - refine (conj _ _).
    + refine (or_introl _).
      refine (HP).
    + refine (or_introl _).
      refine (HP).
  - refine (conj _ _).
    + refine (or_intror _).
      refine (fun HQ => _).
      refine (HnQR _).
      refine (or_introl _).
      refine (HQ).
    + refine (or_intror _).
      refine (fun HR => _).
      refine (HnQR _ ).
      refine (or_intror _).
      refine (HR).
Qed.

task18.v

Require Import Arith.

Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).

Definition NatPlus(n m : Nat) : Nat :=
  fun _ f x => (n _ f)((m _ f) x).

Definition nat2Nat : nat -> Nat := nat_iter.

Definition Nat2nat(n : Nat) : nat := n _ S O.

Lemma NatPlus_plus :
  forall n m, Nat2nat (NatPlus (nat2Nat n) (nat2Nat m)) = n + m.
Proof.
  intros.
  unfold nat2Nat.
  unfold NatPlus.
  unfold Nat2nat.
  assert (nat_iter m S 0 = m).
  induction m.
  simpl.
  reflexivity.
  simpl.
  rewrite IHm.
  reflexivity.
  rewrite H.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.