task13re.v

Inductive pos : Set :=
  | S0 : pos
  | S : pos -> pos.
 
Fixpoint plus(n m:pos) : pos :=
  match n with
  | S0 => S 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.

task28.v

Require Import Reals.
Require Import Field.
Require Import Fourier.

Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
  assert( sum_f_R0 (tg_alt PI_tg) (21) <= PI / 4 )%R.
  apply (PI_ineq 10).
  assert( 61/80 < sum_f_R0 (tg_alt PI_tg) (21) )%R.
  simpl.
  unfold tg_alt.
  unfold PI_tg.
  simpl.
  field_simplify.
  apply (Rminus_lt (61/80) (436451980632680605963119750/563862029680583509947946875) ).
  field_simplify.
  replace (0/1)with(-0) by field.
  replace (-520574640098854370224820625 / 45108962374446680795835750000) with (-(520574640098854370224820625 / 45108962374446680795835750000)) by field.
  apply (Ropp_lt_contravar (520574640098854370224820625 / 45108962374446680795835750000) 0 ).
  apply (Rlt_mult_inv_pos 520574640098854370224820625 45108962374446680795835750000).
  prove_sup0.
  prove_sup0.
  assert ( 4 * sum_f_R0 (tg_alt PI_tg) 21 <= PI ) by fourier.
  assert ( 4 * 61 / 80 < 4 * sum_f_R0 (tg_alt PI_tg) 21 ) by fourier.
  assert ( 4 * 61 / 80 < PI ) by fourier.
  fourier.
Qed.

task31.v

Section Poslist.
  (* このセクションの中では、Aが共通の変数として使える。 *)
  Variable A : Type.
  (* 非空なリスト *)
  Inductive poslist : Type :=
    | nil : A -> poslist
    | cons : A -> poslist -> poslist.

  Section Fold.
    (* 二項演算 *)
    Variable g : A -> A -> A.

   (* gによって畳み込む。
    * 次のどちらかを定義すること。どちらでもよい。
    * 左畳み込み : リスト [a; b; c] に対して (a * b) * c を計算する。
    * 右畳み込み : リスト [a; b; c] に対して a * (b * c) を計算する。
    *)
    Fixpoint fold (l:poslist) : A :=
      match l with
      | nil a => a
      | cons a ll => g a (fold ll)
      end.
  End Fold.
End Poslist.
(* Poslistから抜けたことにより、poslistは変数Aについて量化された形になる。 *)

(* このリストに関するmap関数 *)
Section PoslistMap.
  Variable A B : Type.
  Variable f : A -> B.

  Fixpoint map (A :poslist A) : (poslist B) :=
    match A with
    | nil a => nil B (f a)
    | cons a ll => cons B (f a) (map ll)
  end.
End PoslistMap.

task32.v

Require Import Arith.

Module Type SemiGroup.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
End SemiGroup.

Module NatMult_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult (n m:nat) : nat := n*m.
  Theorem mult_assoc : forall x y z : nat , mult x (mult y z) = mult (mult x y) z.
  Proof.
    intros.
    unfold mult.
    apply (mult_assoc x y z).
  Qed.
End NatMult_SemiGroup.

Module NatMax_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult (n m:nat) : nat := min n m.
  Theorem mult_assoc : forall x y z : nat , min x (min y z) = min (min x y) z.
  Proof.
    intros.
    apply (Min.min_assoc x y z).
  Qed.
End NatMax_SemiGroup.

Module SemiGroup_Product (G0 G1:SemiGroup) <: SemiGroup.
  Inductive prod : Type :=
    pair : G0.G -> G1.G -> prod.
  Definition fst (p:prod) : G0.G :=
    match p with
    | pair a b => a
    end.
  Definition snd (p:prod) : G1.G :=
    match p with
    | pair a b => b
    end.
  Definition G := prod.
  Definition mult (a b:prod) : prod :=
    pair (G0.mult (fst a) (fst b)) (G1.mult (snd a) (snd b)).
  Theorem mult_assoc : forall x y z : prod , mult x (mult y z) = mult (mult x y) z.
  Proof.
    intros.
      unfold mult.
      replace (fst (pair (G0.mult (fst y) (fst z)) (G1.mult (snd y) (snd z)))) with (G0.mult (fst y) (fst z)) by auto.
      replace (snd (pair (G0.mult (fst y) (fst z)) (G1.mult (snd y) (snd z)))) with (G1.mult (snd y) (snd z)) by auto.
      replace (fst (pair (G0.mult (fst x) (fst y)) (G1.mult (snd x) (snd y)))) with (G0.mult (fst x) (fst y)) by auto.
      replace (snd (pair (G0.mult (fst x) (fst y)) (G1.mult (snd x) (snd y)))) with (G1.mult (snd x) (snd y)) by auto.
      rewrite G0.mult_assoc.
      rewrite G1.mult_assoc.
      reflexivity.
  Qed.
End SemiGroup_Product.