Skip to content

Instantly share code, notes, and snippets.

RrIdPAVa+r1:IdAVb+r1:IdAiIsAp1RrLi?=Tr1iSa\ApVap::ApVbp::Op
Require Import SetoidClass.
Require Import Arith.
Record int := {
Ifst : nat;
Isnd : nat
}.
Program Instance ISetoid : Setoid int := {|
equiv x y := Ifst x + Isnd y = Ifst y + Isnd x
Require Import ZArith.
Section Principal_Ideal.
Variable a : Z.
Definition pi : Set := { x : Z | ( a | x )%Z }.
Program Definition plus(a b : pi) : pi := (a + b)%Z.
Next Obligation.
unfold proj1_sig.
Require Import Arith.
Module Type Monoid.
Parameter G : Type.
Parameter mult : G -> G -> G.
Parameter E : G.
Axiom mult_assoc :
forall x y z : G, mult x (mult y z) = mult (mult x y) z.
Axiom identity_element1 :
forall x : G, mult x E = mult E x.
Require Import Reals.
Require Import Fourier.
Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
assert (((sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R <= (PI / 4)%R <=
(sum_f_R0 (tg_alt PI_tg) (2 * 5))%R)%R).
apply PI_ineq.
simpl H.
destruct H.
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.
Print SemiGroup.
Module NatMult_SemiGroup <: SemiGroup.
(* Section の練習 *)
Section Poslist.
(* このセクションの中では、Aが共通の変数として使える。 *)
Variable A : Type.
(* 非空なリスト *)
Inductive poslist : Type :=
nil : A -> poslist | cons : A -> poslist -> poslist.
Require Import ZArith.
Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
intros.
assert (((z ^ 2 - 2)<>0)%Z -> (((z ^ 2 - 2)^2) > 0) % Z).
intro.
assert (forall p : Z, ((p<>0)%Z -> (p ^ 2 > 0) % Z)).
intro.
Require Import Arith.
Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
ring.
Qed.
(* 必要な公理を入れる*)
Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
intros.
tauto.
Qed.
(* 必要な公理を入れる *)