joisino

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros.
  apply H0.
  apply H.
Qed.

Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  intros.

joisino

Require Import Arith.

Goal forall x y, x < y -> x + 10 < y + 10.
Proof.
  intros.
  apply plus_lt_compat_r.
  apply H.
Qed.

joisino

Require Import Arith.

Fixpoint sum_odd(n:nat) : nat :=
  match n with
  | O => O
  | S m => 1 + m + m + sum_odd m
  end.

Goal forall n, sum_odd n = n * n.
Proof.

joisino

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.

joisino

Require Import Arith.
 
Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).
 
Definition NatPlus(n m : Nat) : Nat :=
  fun (A:Type)(f:A->A)(x:A) => ((n A) f)(((m A) f) x).
 
Definition nat2Nat : nat -> Nat := nat_iter.
 

joisino

Require Import Omega.

Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  omega.
Qed.

joisino

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.
 

joisino

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.
    apply (Z.divide_add_r a (proj1_sig a0) (proj1_sig b)).

joisino

Ltac split_all := repeat try split.

(* 以下は動作確認用 *)

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.

joisino

int fib( int n ){
  if( n <= 1 ){
    return n;
  }
  return fib( n - 1 ) + fib( n - 2 );
}
int main(){
  return fib( 10 );
}