qnighy

#!/usr/bin/make -f

EXECS = a b

CC = gcc
CFLAGS = -std=c99 -O2 -Wall -Wextra -ggdb

all: $(EXECS)

clean:

qnighy

Require Import Coq.Relations.Relations.
Require Import Coq.Sets.Constructive_sets.
Parameter X : Set.
Parameter Xle : relation X.
Axiom Xle_refl : reflexive _ Xle.
Axiom Xle_trans : transitive _ Xle.
Axiom Xle_antisym : antisymmetric _ Xle.

Notation "x =<= y" := (Xle x y) (at level 70, no associativity).

qnighy

(* *
 * * Vernacular Commands
 * *)


(*
 * Chapter 1 The Gallina specification language
 *)

(* 1.3.1 Assumptions *)

qnighy

CoInductive cnat : Set :=
  | O : cnat | S : cnat -> cnat.

CoFixpoint cplus n m :=
  match n with
  | O => m
  | S p => S (cplus p m)
  end.

(* mm1 means m - 1 *)

qnighy

Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
intros.
destruct H.
- destruct H0.
  apply H.
- apply H.
Qed.

qnighy

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros P Q HP HPQ; apply HPQ, HP.
Qed.

Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  intros P Q [HnQ HPQ] HP; apply HnQ, HPQ, HP.
Qed.

qnighy

Coq.Logic.ClassicalEpsilon.constructive_indefinite_description
Coq.Logic.ClassicalUniqueChoice.dependent_unique_choice
Coq.Logic.Classical_Prop.classic
Coq.Logic.Description.constructive_definite_description
Coq.Logic.Epsilon.epsilon_statement
Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
Coq.Logic.IndefiniteDescription.constructive_indefinite_description
Coq.Logic.JMeq.JMeq_eq
Coq.Logic.ProofIrrelevance.proof_irrelevance

qnighy

Require Import Eqdep.

Set Implicit Arguments.

Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
  JMeq_refl : JMeq x x.

Lemma JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Proof.
  intros A x y H.

qnighy

Require Import Arith.

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

Goal forall P Q : nat -> Prop, P 0 -> (forall x, P x -> Q x) -> Q 0.
Proof.
  intros P Q H0 H; apply H, H0.

qnighy

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