|
Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |
#######
#
# E-scripts on coq.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/coq.e>
# or at <http://angg.twu.net/e/coq.e.html>.
# See also <http://angg.twu.net/emacs.html>,
# <http://angg.twu.net/.emacs[.html]>,
# <http://angg.twu.net/.zshrc[.html]>,
# <http://angg.twu.net/escripts.html>,
# and <http://angg.twu.net/>.
#
#######
# «.coq-deb-src» (to "coq-deb-src")
# «.coq-doc-deb-src» (to "coq-doc-deb-src")
# «.coq-doc» (to "coq-doc")
# «.coq-tutorial» (to "coq-tutorial")
# «.hevea-deb-src» (to "hevea-deb-src")
# «.proofgeneral-deb-src» (to "proofgeneral-deb-src")
# «.proofgeneral» (to "proofgeneral")
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
apti coq-doc-html coq-doc-pdf
# The Archive of Formal Proofs
# http://afp.sourceforge.net/
# http://afp.sourceforge.net/entries/FOL-Fitting.shtml
# http://afp.sourceforge.net/entries/Category.shtml
#####
#
# coq (from the debian sources)
# 2008aug03
#
#####
# «coq-deb-src» (to ".coq-deb-src")
# http://ftp.debian.org/debian/pool/main/c/coq/
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.1.pl3+dfsg-1.dsc
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.1.pl3+dfsg-1.diff.gz
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.1.pl3+dfsg.orig.tar.gz
#*
sudo apt-get build-dep coq
#*
rm -Rv ~/usrc/coq/
mkdir ~/usrc/coq/
cd $S/http/ftp.debian.org/debian/pool/main/c/coq/
cp -v coq_8.1.pl3+dfsg* ~/usrc/coq/
cd ~/usrc/coq/
dpkg-source -sn -x coq_8.1.pl3+dfsg-1.dsc
cd ~/usrc/coq/coq-8.1.pl3+dfsg/
# dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
dpkg-buildpackage -d -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/coq/")
* (eepitch-shell)
cd ~/usrc/coq/
sudo dpkg -i *.deb
#*
# (code-c-d "coq" "~/usrc/coq/coq-8.1.pl3+dfsg/")
# (find-coqfile "")
# (find-coqsh "find")
# (find-coqfile "theories/")
# (find-coqfile "theories/Init/")
# (find-coqfile "theories/Init/Prelude.v")
# (find-coqfile "theories/Init/Notations.v")
# (find-coqfile "theories/Init/Logic.v")
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
# (find-status "coqide")
# (find-vldifile "coqide.list")
# (find-udfile "coqide/")
# (find-status "coq-libs")
# (find-vldifile "coq-libs.list")
# (find-udfile "coq-libs/")
# (find-udfile "coq-libs/html/")
# (find-udw3m "coq-libs/html/index.html")
# (find-udw3m "coq-libs/html/Coq.Init.Prelude.html")
# (find-man "1 coqide.byte")
# (find-man "1 coqide")
# (find-man "1 coqide.opt")
# (find-man "1 coqc")
# (find-man "1 coq_makefile")
# (find-man "1 coqmktop")
# (find-man "1 coqtop")
# (find-man "1 coq-tex")
# (find-man "1 coqdep")
# (find-man "1 coqdoc")
# (find-man "1 coqtop.byte")
# (find-man "1 coqtop.opt")
# (find-man "1 coqwc")
# (find-man "1 gallina")
# (find-man "1 coq-interface.opt")
# (find-man "1 coq-interface")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
coqtop
Require Import Notations.
Require Import Datatypes.
Require Import Logic.
Unset Boxed Definitions.
Open Scope nat_scope.
#####
#
# coq-doc (from the debian sources)
# 2008aug04
#
#####
# «coq-doc-deb-src» (to ".coq-doc-deb-src")
# http://ftp.debian.org/debian/pool/non-free/c/coq-doc/
# http://ftp.debian.org/debian/pool/non-free/c/coq-doc/coq-doc_8.1-3.dsc
# http://ftp.debian.org/debian/pool/non-free/c/coq-doc/coq-doc_8.1-3.diff.gz
# http://ftp.debian.org/debian/pool/non-free/c/coq-doc/coq-doc_8.1.orig.tar.gz
#*
apti texlive texlive-base texlive-latex-extra texlive-math-extra texlive-lang-french texlive-humanities hevea coq
apti texlive texlive-base texlive-latex-extra texlive-math-extra texlive-lang-french hevea coq
#*
rm -Rv ~/usrc/coq-doc/
mkdir ~/usrc/coq-doc/
cd $S/http/ftp.debian.org/debian/pool/non-free/c/coq-doc/
cp -v coq-doc_8.1* ~/usrc/coq-doc/
cd ~/usrc/coq-doc/
dpkg-source -sn -x coq-doc_8.1-3.dsc
cd ~/usrc/coq-doc/coq-doc-8.1/
# dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
dpkg-buildpackage -d -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/coq-doc/")
* (eepitch-shell)
cd ~/usrc/coq-doc/
sudo dpkg -i *.deb
#*
# (code-c-d "coq-doc" "~/usrc/coq-doc/coq-doc-8.1/")
# (find-coq-docfile "")
#####
#
# coq-doc
# 2008aug04
#
#####
# «coq-doc» (to ".coq-doc")
# (find-status "coq-doc")
# (find-vldifile "coq-doc.list")
# (find-udfile "coq-doc/")
# (find-status "coq-doc-pdf")
# (find-vldifile "coq-doc-pdf.list")
# (find-udfile "coq-doc-pdf/")
# (find-status "coq-doc-html")
# (find-vldifile "coq-doc-html.list")
# (find-udfile "coq-doc-html/")
# (code-c-d "coqdochtml" "/usr/share/doc/coq-doc-html/")
# (find-coqdochtmlfile "")
# (find-coqdochtmlw3m "FAQ.v.html")
# (find-coqdochtmlw3m "RecTutorial.v.html")
# (find-coqdochtmlw3m "Tutorial.v.html")
# (find-coqdochtmlw3m "refman/menu.html")
# (find-coqdochtmlw3m "refman/toc.html")
# (find-coqdochtmlw3m "refman/biblio.html")
# (find-coqdochtmlw3m "refman/general-index.html")
# (find-coqdochtmlw3m "refman/tactic-index.html")
# (find-coqdochtmlw3m "refman/command-index.html")
# (find-coqdochtmlw3m "refman/error-index.html")
# (find-coqdochtmlw3m "Tutorial.v.html#htoc3")
# (find-coqdochtmlw3m "refman/Reference-Manual015.html")
# (find-coqdochtmlw3m "refman/Reference-Manual016.html" "coq-tex")
# (find-coqdochtmlw3m "Tutorial.v.html")
#####
#
# The Coq Tutorial
# 2008aug09
#
#####
# «coq-tutorial» (to ".coq-tutorial")
*;; (find-coqv81w3m "tutorial.html#htoc3" "Declarations")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Check O.
Section Declaration.
Variable n : nat.
Hypothesis Pos_n : (gt n 0).
Check gt.
Check (nat -> Prop).
Check gt n O.
Definition one := (S O).
Definition two : nat := S one.
Definition three : nat := S two.
Definition double (m:nat) := plus m m.
Definition add_n (m:nat) := plus m n.
Check (forall m:nat, gt m 0).
Reset Declaration.
*;; (find-coqv81w3m "tutorial.html#htoc5" "Minimal Logic")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section Minimal_Logic.
Variables A B C : Prop.
Check (A -> B).
Goal (A -> B -> C) -> (A -> B) -> A -> C.
intro H.
intros H' HA.
apply H.
exact HA.
apply H'.
assumption.
Save trivial_lemma.
Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
intros.
apply H; [ assumption | apply H0; assumption ].
Save.
Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
auto.
Abort.
Inspect 3.
*;; (find-coqv81w3m "tutorial.html#htoc7" "Conjunction")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section Foo_Conjunction.
Variables A B C : Prop.
Lemma and_commutative : A /\ B -> B /\ A.
intro.
elim H.
split.
Restart.
intro H; elim H; auto.
Qed.
Check conj.
*;; (find-coqv81w3m "tutorial.html#htoc8" "Disjunction")
Lemma or_commutative : A \/ B -> B \/ A.
intro H; elim H.
intro HA.
clear H.
right.
trivial.
auto.
*;; (find-coqv81w3m "tutorial.html#htoc9" "Tauto")
Restart.
tauto.
Qed.
Print or_commutative.
Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).
tauto.
Qed.
*;; (find-coqv81w3m "tutorial.html#htoc10" "Classical reasoning")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section Foo_Classical.
Variables A B C : Prop.
Lemma Peirce : ((A -> B) -> A) -> A.
try tauto.
Abort.
Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
tauto.
Qed.
Require Import Classical.
Check NNPP.
Lemma Peirce : ((A -> B) -> A) -> A.
apply NNPP; tauto.
Qed.
*;; (find-coqv81w3m "tutorial.html#htoc10" "Scottish")
Section club.
Variables Scottish RedSocks WearKilt Married GoOutSunday : Prop.
Hypothesis rule1 : ~ Scottish -> RedSocks.
Hypothesis rule2 : WearKilt \/ ~ RedSocks.
Hypothesis rule3 : Married -> ~ GoOutSunday.
Hypothesis rule4 : GoOutSunday <-> Scottish.
Hypothesis rule5 : WearKilt -> Scottish /\ Married.
Hypothesis rule6 : Scottish -> WearKilt.
Lemma NoMember : False.
tauto.
Qed.
End club.
Check NoMember.
*;; (find-coqv81w3m "tutorial.html#htoc12" "Sections and signatures")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Reset Initial.
Section Predicate_calculus.
Variable D : Set.
Variable R : D -> D -> Prop.
Section R_sym_trans.
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
Check ex.
intros x x_Rlinked.
intro y.
elim x_Rlinked.
intros y Rxy.
apply R_transitive with y.
assumption.
apply R_symmetric; assumption.
Qed.
End R_sym_trans.
#####
#
# hevea (from the debian sources)
# 2008aug04
#
#####
# «hevea-deb-src» (to ".hevea-deb-src")
# http://ftp.debian.org/debian/pool/main/h/hevea/
# http://ftp.debian.org/debian/pool/main/h/hevea/hevea_1.10-5.dsc
# http://ftp.debian.org/debian/pool/main/h/hevea/hevea_1.10-5.diff.gz
# http://ftp.debian.org/debian/pool/main/h/hevea/hevea_1.10.orig.tar.gz
#*
rm -Rv ~/usrc/hevea/
mkdir ~/usrc/hevea/
cd $S/http/ftp.debian.org/debian/pool/main/h/hevea/
cp -v hevea_1.10* ~/usrc/hevea/
cd ~/usrc/hevea/
dpkg-source -sn -x hevea_1.10-5.dsc
cd ~/usrc/hevea/hevea-1.10/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/hevea/")
* (eepitch-shell)
cd ~/usrc/hevea/
sudo dpkg -i *.deb
#*
# (code-c-d "hevea" "~/usrc/hevea/hevea-1.10/")
# (find-heveafile "")
#####
#
# proofgeneral (from the debian sources)
# 2008aug04
#
#####
# «proofgeneral-deb-src» (to ".proofgeneral-deb-src")
# http://ftp.debian.org/debian/pool/main/p/proofgeneral/
# http://ftp.debian.org/debian/pool/main/p/proofgeneral/proofgeneral_3.7-3.dsc
# http://ftp.debian.org/debian/pool/main/p/proofgeneral/proofgeneral_3.7-3.diff.gz
# http://ftp.debian.org/debian/pool/main/p/proofgeneral/proofgeneral_3.7.orig.tar.gz
#*
rm -Rv ~/usrc/proofgeneral/
mkdir ~/usrc/proofgeneral/
cd $S/http/ftp.debian.org/debian/pool/main/p/proofgeneral/
cp -v proofgeneral_3.7* ~/usrc/proofgeneral/
cd ~/usrc/proofgeneral/
dpkg-source -sn -x proofgeneral_3.7-3.dsc
cd ~/usrc/proofgeneral/proofgeneral-3.7/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/proofgeneral/")
* (eepitch-shell)
cd ~/usrc/proofgeneral/
# sudo dpkg -i *.deb
sudo dpkg -i {proofgeneral,proofgeneral-coq,proofgeneral-doc}_*.deb
#*
# (code-c-d "proofgeneral" "~/usrc/proofgeneral/proofgeneral-3.7/")
# (find-proofgeneralfile "debian/control")
# (find-proofgeneralfile "")
#####
#
# proofgeneral
# 2008aug04
#
#####
# «proofgeneral» (to ".proofgeneral")
# (find-status "proofgeneral")
# (find-vldifile "proofgeneral.list")
# (find-udfile "proofgeneral/")
# (find-status "proofgeneral-coq")
# (find-vldifile "proofgeneral-coq.list")
# (find-udfile "proofgeneral-coq/")
# (find-status "proofgeneral-doc")
# (find-vldifile "proofgeneral-doc.list")
# (find-udfile "proofgeneral-doc/")
# (find-node "(PG-adapting)Top")
# (find-node "(ProofGeneral)Top")
# (find-node "(ProofGeneral)Quick start guide")
# (find-node "(ProofGeneral)Walkthrough example in Isabelle")
# (find-node "(ProofGeneral)Walkthrough example in Isabelle" "undo")
# (find-node "(ProofGeneral)Coq Proof General")
# (find-fline "/etc/emacs/site-start.d/50proofgeneral.el")
# (find-sitelispfile "proofgeneral/generic/proof-site.el")
# (find-sitelispfile "proofgeneral/generic/")
# (find-sitelispfile "proofgeneral/coq/")
# (find-sitelispfile "proofgeneral/coq/coq.el")
# http://proofgeneral.inf.ed.ac.uk/images/pg-coq-screenshot.png
(proofgeneral)
(find-file "/tmp/foo.v")
#####
#
# coq
# 2000may27
#
#####
# (find-status "coq")
# (find-status "ocaml")
# (find-status "camlp4")
# (find-vldifile "coq.list")
# (find-vldifile "ocaml.list")
# (find-vldifile "camlp4.list")
# (find-fline "/usr/doc/coq/")
# (find-fline "/usr/doc/ocaml/")
# (find-fline "/usr/doc/camlp4/")
# (find-status "libncurses5-dev")
# (find-vldifile "libncurses5-dev.list")
# (find-fline "/usr/doc/libncurses5-dev/")
# (find-status "libncurses4-dev")
# (find-vldifile "libncurses4-dev.list")
# (find-fline "/usr/doc/libncurses4-dev/")
#####
#
# coq-doc
# 2000may27
#
#####
# (find-status "coq-doc")
# (find-vldifile "coq-doc.list")
# (find-fline "/usr/doc/coq-doc/")
# (find-fline "/usr/doc/coq-doc/README")
# (code-c-d "coqhtml" "/usr/doc/coq-doc/coq-docs-html/")
# (find-coqhtmlw3 "toc.html")
# (find-coqhtmlw3 "node.3.4.0.html")
zcat /usr/doc/coq-doc/Tutorial.ps.gz \
| pstotext \
> ~/tmp/coq-tutor.ps.txt
# (find-fline "~/tmp/coq-tutor.ps.txt")
gv /usr/doc/coq-doc/Tutorial.ps.gz
gv /usr/doc/coq-doc/Changes.ps.gz
gv /usr/doc/coq-doc/Library.ps.gz
gv /usr/doc/coq-doc/Reference-Manual-base.ps.gz
gv /usr/doc/coq-doc/Reference-Manual-addendum.ps.gz
#gv /usr/doc/coq-doc/Reference-Manual-all.ps.gz
# (w3-open-local "/usr/doc/coq-doc/coq-docs-html/")
# (w3-open-local "/usr/doc/coq-doc/coq-docs-html/toc.html")
lynx /usr/doc/coq-doc/coq-docs-html/toc.html
links /usr/doc/coq-doc/coq-docs-html/toc.html
edrxnetscape /usr/doc/coq-doc/coq-docs-html/toc.html &
# What's the difference between the two ref.manuals?
zcat /usr/doc/coq-doc/Reference-Manual-base.ps.gz | pstotext > /tmp/base.txt
zcat /usr/doc/coq-doc/Reference-Manual-all.ps.gz | pstotext > /tmp/all.txt
#
# Aha: a diff shows that "all" is "base" plus "addendum". Note that
# "base" doesn't have the pages numbered 218--302 (the "addendum"); it
# jumps from 217 to 303.
http://ftp.debian.org/debian/pool/main/p/proofgeneral/proofgeneral_3.7-3.dsc
# Local Variables:
# coding: raw-text-unix
# ee-delimiter-hash: "\n#*\n"
# ee-delimiter-percent: "\n%*\n"
# ee-anchor-format: "«%s»"
# End: