qnighy

Require Import Arith.
Require Import List.

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

Definition nn_to_nat(nn : nat * nat) : nat :=

qnighy

Require Import Relations.

Definition clos_refl_trans2(A : Type) (R : relation A) : relation A
  := fun x y =>
      forall R' : relation A,
        (forall x y, R x y -> R' x y) ->
        reflexive _ R' -> transitive _ R' -> R' x y.

Lemma clos_refl_trans2_iff :
  forall A (R : relation A) x y,

qnighy

Require Import Arith.
Require Import Lists.List.
Require Import Omega.

Theorem t1 : (forall P, P \/ ~P) -> (forall P, ~~P -> P).
Proof.
  intros LEM P; destruct (LEM P); tauto.
Qed.

Theorem t2 : forall (A:Type) (P:A->Prop), (~exists x:A, P x) -> (forall x:A, ~P x).

qnighy

#!/usr/bin/ruby
# -*- coding: utf-8 -*-

chopsticks = Array.new(5) {Mutex.new}

threads = Array.new(5) {|i|
  Thread.new {
    loop {
      chopsticks[i].synchronize {
        puts "take left #{i}"

qnighy

(* サブゴールは消滅するがQedに失敗する証明の試みの例 *)
(* これらはQedに失敗しているので証明とはいえない *)

Lemma f : True -> False.
Proof.
  fix 1.
  assumption.
Fail Qed.
Abort.

qnighy

Inductive T2 : Type :=
  | T2Empty : T2
  | T2Node : T2 -> T2 -> T2.

Inductive Tm : Type :=
  | TmNode : list Tm -> Tm.

Fixpoint f(t:T2) : Tm :=
  match t with
  | T2Empty => TmNode nil

qnighy

Definition True' : Prop := forall P : Prop, P -> P.
Definition False' : Prop := forall P : Prop, P.
Definition and'(A B : Prop) := forall P : Prop, (A -> B -> P) -> P.
Definition or'(A B : Prop) := forall P : Prop, (A -> P) -> (B -> P) -> P.


Lemma True'_iff : True <-> True'.
Proof.
  unfold True'.
  intuition auto.

qnighy

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
Require Import tuple finfun finset.
Require Import Coq.Vectors.Vector.

Lemma beheadE n T (x : T) (t : n.-tuple T) :
    behead_tuple [tuple of x :: t] = t.
Proof.
  by apply val_inj.
Qed.

qnighy

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.

qnighy

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

Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun P Q H0 H1 =>
    let (H2, H3) := H0 in
    H2 (H3 H1).

Definition Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q
  := fun P Q H0 H1 =>