|
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/>.
#
#######
(fooi "find-coqv81w3m \"tutorial.html" "find-coqtutw3m \"")
# «.coq-deb-src» (to "coq-deb-src")
# «.coq-8.2-deb-src» (to "coq-8.2-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")
# «.cis500» (to "cis500")
# «.bertot-casteran» (to "bertot-casteran")
# «.coq-art» (to "coq-art")
# «.local-variables» (to "local-variables")
# «.type_of» (to "type_of")
# «.scopes» (to "scopes")
# «.categories-in-coq» (to "categories-in-coq")
# «.record-types» (to "record-types")
# «.simple-proofs» (to "simple-proofs")
# «.intro-apply-assumption-0» (to "intro-apply-assumption-0")
# «.intro-apply-assumption» (to "intro-apply-assumption")
# «.composition» (to "composition")
# «.cut» (to "cut")
# «.email-about-7-uples» (to "email-about-7-uples")
# «.dependent-projections» (to "dependent-projections")
# «.ab=1-implies-a=1» (to "ab=1-implies-a=1")
# «.coq-mode» (to "coq-mode")
# «.mailing-list» (to "mailing-list")
# «.print-string» (to "print-string")
# «.search» (to "search")
# «.conjunction» (to "conjunction")
# «.sections» (to "sections")
# «.agda» (to "agda")
# «.oficina» (to "oficina")
# «.cpdt» (to "cpdt")
# «.coq-in-a-hurry» (to "coq-in-a-hurry")
# «.monoid» (to "monoid")
# «.proofweb» (to "proofweb")
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
apti coq coq-doc-html coq-doc-pdf
# (find-available "ledit")
# (find-available "cle")
# (find-available "cle" "Wrap any command-line driven tool with readline")
# 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 8.2 (from the debian sources - INCOMPLETE SCRIPT)
# 2009jul30
#
#####
# «coq-8.2-deb-src» (to ".coq-8.2-deb-src")
# http://ftp.debian.org/debian/pool/main/c/coq/
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.2-1+dfsg-1.dsc
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.2-1+dfsg-1.diff.gz
# http://ftp.debian.org/debian/pool/main/c/coq/coq_8.2-1+dfsg.orig.tar.gz
# dpkg-checkbuilddeps: Unmet build dependencies:
# dh-ocaml (>= 0.4.1)
# ocaml-nox (>= 3.11.0-5)
# camlp5 (>= 5.10-3)
# liblablgtk2-ocaml-dev (>= 2.12.0-2)
# hevea (>= 1.10-7)
# http://backports.org/debian/pool/main/d/dh-ocaml/
# http://backports.org/debian/pool/main/d/dh-ocaml/dh-ocaml_0.4.1~bpo50+1.dsc
# http://backports.org/debian/pool/main/d/dh-ocaml/dh-ocaml_0.4.1~bpo50+1.tar.gz
# http://ftp.de.debian.org/debian/pool/main/d/dh-ocaml/
# http://ftp.de.debian.org/debian/pool/main/d/dh-ocaml/dh-ocaml_0.5.0.dsc
# http://ftp.de.debian.org/debian/pool/main/d/dh-ocaml/dh-ocaml_0.5.0.tar.gz
# http://ftp.debian.org/debian/pool/main/o/ocaml/
# http://ftp.debian.org/debian/pool/main/o/ocaml/ocaml_3.11.1-2.dsc
# http://ftp.debian.org/debian/pool/main/o/ocaml/ocaml_3.11.1-2.diff.gz
# http://ftp.debian.org/debian/pool/main/o/ocaml/ocaml_3.11.1.orig.tar.gz
# http://ftp.de.debian.org/debian/pool/main/c/camlp5/
# http://ftp.de.debian.org/debian/pool/main/c/camlp5/camlp5_5.10-3.dsc
# http://ftp.de.debian.org/debian/pool/main/c/camlp5/camlp5_5.10-3.diff.gz
# http://ftp.de.debian.org/debian/pool/main/c/camlp5/camlp5_5.10.orig.tar.gz
# http://ftp.de.debian.org/debian/pool/main/l/lablgtk2/
# http://ftp.de.debian.org/debian/pool/main/l/lablgtk2/lablgtk2_2.12.0-2.dsc
# http://ftp.de.debian.org/debian/pool/main/l/lablgtk2/lablgtk2_2.12.0-2.diff.gz
# http://ftp.de.debian.org/debian/pool/main/l/lablgtk2/lablgtk2_2.12.0.orig.tar.gz
# http://ftp.de.debian.org/debian/pool/main/h/hevea/
# http://ftp.de.debian.org/debian/pool/main/h/hevea/hevea_1.10-7.dsc
# http://ftp.de.debian.org/debian/pool/main/h/hevea/hevea_1.10-7.diff.gz
# http://ftp.de.debian.org/debian/pool/main/h/hevea/hevea_1.10.orig.tar.gz
sudo apt-get build-dep ocaml-nox
sudo apt-get build-dep camlp5
sudo apt-get build-dep liblablgtk2-ocaml-dev
sudo apt-get build-dep hevea
apti docbook-xsl
#*
rm -Rv ~/usrc/dh-ocaml/
mkdir ~/usrc/dh-ocaml/
cd $S/http/ftp.de.debian.org/debian/pool/main/d/dh-ocaml/
cp -v dh-ocaml_0.5.0* ~/usrc/dh-ocaml/
cd ~/usrc/dh-ocaml/
dpkg-source -sn -x dh-ocaml_0.5.0.dsc
cd ~/usrc/dh-ocaml/dh-ocaml-0.5.0/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/dh-ocaml/")
* (eepitch-shell)
cd ~/usrc/dh-ocaml/
sudo dpkg -i *.deb
#*
rm -Rfv ~/usrc/ocaml/
mkdir ~/usrc/ocaml/
cd $S/http/ftp.debian.org/debian/pool/main/o/ocaml/
cp -v ocaml_3.11.1* ~/usrc/ocaml/
cd ~/usrc/ocaml/
dpkg-source -sn -x ocaml_3.11.1-2.dsc
cd ~/usrc/ocaml/ocaml-3.11.1/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
# (find-fline "~/usrc/ocaml/ocaml-3.11.1/")
# (find-fline "~/usrc/ocaml/ocaml-3.11.1/odb" "*** [camlp4opt] Error 2")
#*
# (find-fline "~/usrc/ocaml/")
* (eepitch-shell)
cd ~/usrc/ocaml/
sudo dpkg -i *.deb
#*
rm -Rv ~/usrc/camlp5/
mkdir ~/usrc/camlp5/
cd $S/http/ftp.de.debian.org/debian/pool/main/c/camlp5/
cp -v camlp5_5.10* ~/usrc/camlp5/
cd ~/usrc/camlp5/
dpkg-source -sn -x camlp5_5.10-3.dsc
cd ~/usrc/camlp5/camlp5-5.10/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
# (find-fline "~/usrc/camlp5/camlp5-5.10/odb")
# Sorry: the compatibility with ocaml version "3.11.1"
# is not yet implemented. Please report.
#
# Configuration failed.
# make: *** [debian/configure-stamp] Error 2
# dpkg-buildpackage: failure: debian/rules build gave error exit status 2
#*
# (find-fline "~/usrc/camlp5/")
* (eepitch-shell)
cd ~/usrc/camlp5/
sudo dpkg -i *.deb
#*
#*
#*
rm -Rv ~/usrc/hevea/
mkdir ~/usrc/hevea/
cd $S/http/ftp.de.debian.org/debian/pool/main/h/hevea/
cp -v hevea_1.10* ~/usrc/hevea/
cd ~/usrc/hevea/
dpkg-source -sn -x hevea_1.10-7.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
#*
#*
rm -Rv ~/usrc/lablgtk2/
mkdir ~/usrc/lablgtk2/
cd $S/http/ftp.de.debian.org/debian/pool/main/l/lablgtk2/
cp -v lablgtk2_2.12.0* ~/usrc/lablgtk2/
cd ~/usrc/lablgtk2/
dpkg-source -sn -x lablgtk2_2.12.0-2.dsc
cd ~/usrc/lablgtk2/lablgtk2-2.12.0/
dpkg-buildpackage -us -uc -b -rfakeroot |& tee odb
#*
# (find-fline "~/usrc/lablgtk2/")
* (eepitch-shell)
cd ~/usrc/lablgtk2/
sudo dpkg -i *.deb
#*
# (code-c-d "camlp5" "~/usrc/camlp5/camlp5-5.10/")
# (find-camlp5file "")
#*
rm -Rv ~/usrc/coq/
mkdir ~/usrc/coq/
cd $S/http/ftp.debian.org/debian/pool/main/c/coq/
cp -v coq_8.2* ~/usrc/coq/
cd ~/usrc/coq/
dpkg-source -sn -x coq_8.2-1+dfsg-1.dsc
cd ~/usrc/coq/coq-8.2-1+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.2-1+dfsg/")
# (find-coqfile "")
#####
#
# 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-LATEX "# (find-vldifile \"coq-doc-html.list\")")
# (find-LATEXdvi "# (find-vldifile \"coq-doc-html.list\")")
# (find-udfile "coq-doc-html/")
# (code-c-d "coqdochtml" "/usr/share/doc/coq-doc-html/")
# (find-coqdocfile "")
# (find-coqdochtmlfile "")
# (find-coqdochtmlw3m "FAQ.v.html")
# (find-coqdochtmlw3m "RecTutorial.v.html")
# (find-coqdochtmlw3m "Tutorial.v.html")
# (find-coqrefw3m "menu.html")
# (find-coqrefw3m "toc.html")
# (find-coqrefw3m "biblio.html")
# (find-coqrefw3m "general-index.html")
# (find-coqrefw3m "tactic-index.html")
# (find-coqrefw3m "command-index.html")
# (find-coqrefw3m "error-index.html")
# (code-c-d "coqhtmlref" "/usr/share/doc/coq-doc-html/refman/")
# (find-coqreffile "")
# (find-coqrefw3m "toc.html")
# (find-coqrefw3m "Reference-Manual013.html" "Syntax extensions")
# (find-coqdochtmlw3m "Tutorial.v.html#htoc3")
# (find-coqhtmlrefw3m "refman/Reference-Manual015.html")
# (find-coqhtmlrefw3m "refman/Reference-Manual016.html" "coq-tex")
# (find-coqdochtmlw3m "Tutorial.v.html")
/usr/share/doc/coq-doc-pdf/Tutorial.v.pdf
/usr/share/doc/coq-doc-pdf/Reference-Manual.pdf
/usr/share/doc/coq-doc-pdf/FAQ.v.pdf
/usr/share/doc/coq-doc-pdf/RecTutorial.v.pdf
/usr/share/doc/coq-doc-pdf/Tutorial.v.pdf
(code-xpdf "coqref" "/usr/share/doc/coq-doc-pdf/Reference-Manual.pdf")
(code-pdftotext "coqref" "/usr/share/doc/coq-doc-pdf/Reference-Manual.pdf")
;; (find-coqrefpage 13 "Contents")
;; (find-coqrefpage 333 "Global Index")
;; (find-coqreftext)
/usr/share/doc/coq-doc-pdf/FAQ.v.pdf
/usr/share/doc/coq-doc-pdf/RecTutorial.v.pdf
#####
#
# The Coq Tutorial
# 2008aug09
#
#####
# «coq-tutorial» (to ".coq-tutorial")
*;; (find-coqtutw3m "#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-coqtutw3m "#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-coqtutw3m "#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-coqtutw3m "#htoc8" "Disjunction")
Lemma or_commutative : A \/ B -> B \/ A.
intro H; elim H.
intro HA.
clear H.
right.
trivial.
auto.
*;; (find-coqtutw3m "#htoc9" "Tauto")
Restart.
tauto.
Qed.
Print or_commutative.
Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).
tauto.
Qed.
*;; (find-coqtutw3m "#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-coqtutw3m "#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-coqrefw3m "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")
#####
#
# Benjamin C. Pierce's course on Prog Lang Foundations using Coq
# 2009jan25
#
#####
# «cis500» (to ".cis500")
# Using a Proof Assistant to Teach Programming Language Foundations
# (or: Lambda, the Ultimate TA)
# http://lists.seas.upenn.edu/pipermail/types-list/2009/001324.html
# http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf
# http://www.seas.upenn.edu/~cis500/cis500-s09/index.html
# http://www.seas.upenn.edu/~cis500/cis500-f07/index.html
# http://www.seas.upenn.edu/~cis500/cis500-s09/lectures/Basics.pdf
# http://www.seas.upenn.edu/~cis500/cis500-s09/lectures/Lists.pdf
#####
#
# Bertot/Castéran: Coq'Art
# 2009jun14
#
#####
# «bertot-casteran» (to ".bertot-casteran")
# «coq-art» (to ".coq-art")
# (find-LATEX "catsem.bib" "bib-Coq")
# (find-books "__comp/__comp.el" "coq")
# http://www.labri.fr/perso/casteran/CoqArt/index.html
# http://www.labri.fr/perso/casteran/CoqArt/coqart81.tar.gz
# http://www.labri.fr/perso/casteran/CoqArt/contents.html
#*
rm -Rv ~/usrc/CoqArtExos81/
tar -C ~/usrc/ -xvzf \
$S/http/www.labri.fr/perso/casteran/CoqArt/coqart81.tar.gz
cd ~/usrc/CoqArtExos81/
#*
# (code-c-d "coqart" "~/usrc/CoqArtExos81/")
# (find-coqartfile "")
# (find-coqartw3m "contents.html")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
# (find-coqartpage 17 "Contents")
# (find-coqartpage (+ 26 1) "1. A brief overview")
# (find-coqartfile "horizon/SRC/")
# (find-coqartpage (+ 26 13) "2. Types and expressions")
# (find-coqartfile "specprog/SRC/")
# (find-coqartfile "specprog/SRC/chap2.v")
# (find-coqartpage (+ 26 43) "3. Propositions and proofs")
# (find-coqartpage (+ 26 47) "Definition 8 (Goal).")
# (find-coqartpage (+ 26 47) "Definition 9 (Tactics).")
# (find-coqartfile "propproof/SRC/")
# (find-coqartfile "propproof/SRC/chap3.v")
# (find-coqartpage (+ 26 73) "4. Dependent products or Pandora's box")
# (find-coqartfile "depprod/SRC/")
# (find-coqartfile "depprod/SRC/chap4.v")
# (find-coqartpage (+ 26 105) "5. Everyday logic")
# (find-coqartfile "everyday/SRC/")
# (find-coqartfile "everyday/SRC/chap5.v")
# (find-coqartpage (+ 26 137) "6. Inductive data types")
# (find-coqartfile "structinduct/SRC/")
# (find-coqartfile "structinduct/SRC/chap6.v")
# (find-coqartpage (+ 26 187) "7. Tactics and automation")
# (find-coqartfile "autotac/SRC/")
# (find-coqartfile "autotac/SRC/chap7.v")
# (find-coqartpage (+ 26 211) "8. Inductive predicates")
# (find-coqartfile "inductive-prop-chap/SRC/")
# (find-coqartfile "inductive-prop-chap/SRC/chap8.v")
# (find-coqartpage (+ 26 251) "9. Functions and their specifications")
# (find-coqartfile "progav/SRC/")
# (find-coqartfile "progav/SRC/chap9.v")
# (find-coqartpage (+ 26 285) "10. Extraction and imperative programming")
# (find-coqartfile "extraction/SRC/")
# (find-coqartfile "extraction/SRC/chap10.v")
# (find-coqartpage (+ 26 309) "11. A case study")
# (find-coqartfile "searchtrees/SRC/")
# (find-coqartpage (+ 26 325) "12. The module system")
# (find-coqartfile "modules/SRC/")
# (find-coqartpage (+ 26 347) "13. Infinite objects and proofs")
# (find-coqartfile "co-inductifs/SRC/")
# (find-coqartpage (+ 26 377) "14. Foundations of inductive types")
# (find-coqartfile "induc-fond/SRC/")
# (find-coqartfile "induc-fond/SRC/chap14.v")
# (find-coqartpage 17 "Contents")
# (find-coqartpage (+ 26 407) "15. General recursion")
# (find-coqartfile "gen-rec/SRC/")
# (find-coqartfile "gen-rec/SRC/chap15.v")
# (find-coqartpage (+ 26 433) "16. Proof by reflection")
# (find-coqartfile "reflection/SRC/")
# (find-coqartfile "reflection/SRC/chap16.v")
# (find-coqartpage (+ 26 459) "Index")
#####
#
# local variables
# 2009jul30
#
#####
# «local-variables» (to ".local-variables")
# (find-coqartpage (+ 26 13) "2. A brief overview")
# (find-coqartpage (+ 26 30) "2.3.2. Sections and local variables")
# (find-coqartfile "specprog/SRC/")
# (find-coqartfile "specprog/SRC/chap2.v")
# (find-coqartfile "specprog/SRC/chap2.v" "Section binomial_def.")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
Open Scope Z_scope.
Section binomial_def.
Variables a b:Z.
Definition binomial z:Z := a*z + b.
Section trinomial_def.
Variable c : Z.
Definition trinomial z:Z := (binomial z)*z + c.
End trinomial_def.
End binomial_def.
Print binomial.
Print trinomial.
#####
#
# type_of (with thanks to rocketman/soupdragon)
# 2009jul30
#
#####
# «type_of» (to ".type_of")
# (find-fline "~/LOGS/2009jul29.coq")
# (find-coqartpage (+ 26 73) "4. Dependent products or Pandora's box")
# (find-coqartpage (+ 26 88) "4.2.3.2. Implicit arguments")
# (find-coqartfile "depprod/SRC/")
# (find-coqartfile "depprod/SRC/chap4.v")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
Definition type_of_ (T : Type) (t : T) := T.
Definition type_of (T : Type) (t : T) := T.
Implicit Arguments type_of [T].
Print type_of_.
Print type_of.
Check type_of_.
Check type_of_ _ 2.
Check type_of.
Check type_of 2.
Reset type_of_.
Set Implicit Arguments.
Definition type_of (T : Type) (t : T) := T.
Print type_of.
Definition two := 2.
Check two.
Parameter a : type_of two.
Check a.
#####
#
# Interpretation scopes
# 2009jul30
#
#####
# «scopes» (to ".scopes")
# (find-coqrefw3m "general-index.html" "Interpretation scopes")
# (find-coqartpage (+ 26 14) "2.1.2. Interpretation scopes")
# (find-coqartfile "specprog/SRC/chap2.v")
# (find-coqrefw3m "Reference-Manual013.html#scopes")
# (find-coqrefw3m "Reference-Manual015.html#scopes")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
Check ((2%Z),(3%nat)).
Check (((2%Z),(3%nat)))%nat.
#####
#
# categories in Coq
# 2009jul29
#
#####
# «categories-in-coq» (to ".categories-in-coq")
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
# (find-status "coq-libs")
# (find-vldifile "coq-libs.list")
# (find-udfile "coq-libs/")
# http://en.wikipedia.org/wiki/Coq
# http://www.lix.polytechnique.fr/cocorico/
# http://www.labri.fr/perso/casteran/CoqArt/coqart81.tar.gz
# (find-coqartpage 17 "Contents")
# (find-coqartpage (+ 26 1) "1. A Brief Overview")
# (find-coqartpage (+ 26 460) "Index")
# (find-coqarttext)
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
Definition type_of (T : Type) (t : T) := T.
Implicit Arguments type_of [T].
Section Category_C.
Variable C_0 : Type.
Variable Hom_C : C_0 -> C_0 -> Set.
Variable id_C : forall (A : C_0), Hom_C A A.
Variable o_C : forall (A B C : C_0) (g : Hom_C B C) (f : Hom_C A B), Hom_C A C.
Implicit Arguments o_C [A B C].
Variable idL_C : forall (A B : C_0) (f : Hom_C A B), (o_C (id_C _) f = f).
Implicit Arguments idL_C [A B].
Variable idR_C : forall (A B : C_0) (f : Hom_C A B), (o_C f (id_C _) = f).
Implicit Arguments idR_C [A B].
Variable assoc_C : forall (A B C D : C_0)
(f : Hom_C A B) (g : Hom_C B C) (h : Hom_C C D),
(o_C h (o_C g f) = o_C (o_C h g) f).
Implicit Arguments assoc_C [A B C D].
Definition C := (C_0, Hom_C, id_C, o_C, idL_C, idR_C, assoc_C).
Definition C_minus := (C_0, Hom_C, id_C, o_C).
Definition Category := type_of C.
Definition Protocategory := type_of C_minus.
Check assoc_C.
Print assoc_C.
Check C.
Check Category.
Print Category.
Variable D : Category.
Definition (D_0, Hom_D, id_D, o_D, idL_D, idR_D, assoc_D) := D.
(* ... *)
Check D.
(* ^
Syntax error: [Prim.identref] expected after [def_token] (in [vernac:gallina])
*)
#####
#
# Record types
# 2009jul30
#
#####
# «record-types» (to ".record-types")
# (find-coqrefw3m "general-index.html" "Record,")
# (find-coqrefpage 47 "\n2.1 Record types")
# (find-coqreftext "\n2.1 Record types")
# (find-coqfile "")
# (find-coqsh "find | sort")
# (find-coqfile "contrib/" "setoid_ring")
# (find-coqfile "theories/Arith/Mult.v")
# (find-coqfile "theories/Arith/")
# (find-coqfile "toplevel/record.ml")
# (find-coqfile "toplevel/record.mli")
# (find-coqfile "parsing/g_vernac.ml4" "record_token:")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
Record Rat:Set := mkRat {
sign : bool;
top : nat;
bottom : nat;
Rat_bottom_cond : 0 <> bottom
}.
Print Rat.
Print mkRat.
Definition half := mkRat true 1 2 (O_S 1).
Check half.
Eval compute in half.(top).
Eval compute in half.(bottom).
Eval compute in half.(Rat_bottom_cond).
(* The rest of this block is garbage *)
Reset Initial.
Check 2%Z.
# (find-coqartpage (+ 26 85) "Definition of polymorphic functions")
Definition twice : forall A:Set, (A->A)->A->A
:= fun A f a => f (f a).
Check forall (A B : Set)(a:A)(b:B),A*B.
Check (2,3).
Check 2.
Check Z.
Check Set.
#####
#
# Proving some simple theorems
# 2009jul31
#
#####
# «simple-proofs» (to ".simple-proofs")
# (find-coqartpage (+ 26 43) "3. Propositions and proofs")
# (find-coqartpage (+ 26 48) "apply")
# (find-coqartpage (+ 26 58) "Exercise 3.2")
# (find-coqartfile "propproof/SRC/")
# (find-coqartfile "propproof/SRC/chap3.v")
# (find-coqartfile "propproof/SRC/simple_proofs.v")
# (find-coqartfile "propproof/SRC/simple_proofs.v" "weak_peirce")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "(((P->Q)->P)->P)->Q ((P->Q)->P)->P (P->Q)->P (P->Q)->P' P->Q P")
Section simple_proofs.
Variables P Q R S : Prop.
Lemma weak_peirce : ((((P -> Q) -> P) -> P) -> Q) -> Q.
Proof.
intro (((P->Q)->P)->P)->Q.
apply (((P->Q)->P)->P)->Q.
intro (P->Q)->P.
apply (P->Q)->P.
intro P.
apply (((P->Q)->P)->P)->Q.
intro (P->Q)->P'.
assumption.
Show Tree.
Qed.
End simple_proofs.
Reset simple_proofs.
#####
#
# The simplest tactics: intro, apply and assumption
# 2009oct27
#
#####
# «intro-apply-assumption-0» (to ".intro-apply-assumption-0")
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
\def\vdashq{\begin{picture}(0,0)\put(5,4.5){\tiny?}\end{picture}\vdash}
\def\tactic#1#2{\text{\textsf{#1}: $#2$}}
%:*|-?*\vdashq *
%:*&*\land *
%:
%: -----------------\tactic{assumption}{Ð{p}':=Ð{p}}
%: Ð{p\_q}:P->Q,Ð{q\_r}:Q->R,Ð{p}:P|-?Ð{p}':P
%: -----------------\tactic{apply}{Ð{q}:=Ð{p\_q}\;Ð{p}'}
%: Ð{p\_q}:P->Q,Ð{q\_r}:Q->R,Ð{p}:P|-?Ð{q}:Q
%: -----------------\tactic{apply}{Ð{r}:=Ð{q\_r}\;Ð{q}}
%: Ð{p\_q}:P->Q,Ð{q\_r}:Q->R,Ð{p}:P|-?Ð{r}:R
%: -------------------\tactic{intro}{Ð{p\_r}:=ðÐ{p}¨P.Ð{r}}
%: Ð{p\_q}:P->Q,Ð{q\_r}:Q->R|-?Ð{p\_r}:P->R
%: -----------------------\tactic{intro}{Ð{q\_r\_\_p\_r}:=ðÐ{q\_r}¨(Q->R).Ð{p\_r}}
%: Ð{p\_q}:P->Q|-?Ð{q\_r\_\_p\_r}:(Q->R)->P->R
%: ---------------------\tactic{intro}{Ð{imp\_trans}:=ðÐ{p\_q}¨(P->Q).Ð{q\_r\_\_p\_r}}
%: |-?Ð{imp\_trans}:(P->Q)->(Q->R)->P->R
%:
%: ^imp_trans_1
%:
\noindent
$\ded{imp_trans_1}$
\msk
{\myttchars
% \footnotesize
% * (eepitch-coqtop)
% * (eepitch-kill)
% * (eepitch-coqtop)
\begin{verbatim}
Parameter P Q R : Prop.
Theorem imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intros p_q q_r.
intro p.
apply q_r.
apply p_q.
assumption.
Qed.
Print imp_trans.
\end{verbatim}
}
\bsk
%:
%: ----\tactic{exact}{Ð{p}:=Ð{proj1}\;Ð{pq}} ---\tactic{exact}{Ð{q}:=Ð{proj2}\;Ð{pq}}
%: Ð{pq}:P&Q|-?Ð{p}:P Ð{pq}:P&Q|-?Ð{q}:Q
%: ----------------------\tactic{split}{Ð{qp}:=Ð{conj}\;Ð{p}\;Ð{q}}
%: Ð{pq}:P&Q|-?Ð{qp}:Q&P
%: ------------------------------\tactic{intro}{Ð{and\_commutes}:=ðÐ{pq}¨(P&Q).Ð{qp}}
%: |-?Ð{and\_commutes}:P&Q->Q&P
%:
%: ^and_commutes_1
%:
\noindent
$\ded{and_commutes_1}$
\msk
{\myttchars
% \footnotesize
\begin{verbatim}
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intro pq.
split.
exact (proj2 pq).
exact (proj1 pq).
Qed.
Print and_commutes.
\end{verbatim}
}
%*
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Parameters P Q R T : Prop.
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intro pq.
split.
exact (proj2 pq).
exact (proj1 pq).
Qed.
Print and_commutes.
# (find-coqartpage (+ 26 52) "Lemma")
# (find-coqartfile "propproof/SRC/chap3.v" "Lemma apply_example")
# (find-coqartpage (+ 26 53) "exact")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "p|->p|->q p")
Parameter P Q R T : Prop.
Theorem delta : (P->P->Q)->P->Q.
Proof (fun p|->p|->q p => p|->p|->q p p).
* (dnc-strings "q|->r|->t p|->q")
Lemma apply_example : (Q->R->T)->(P->Q)->P->R->T.
Proof.
intros q|->r|->t p|->q p r.
apply q|->r|->t.
exact (p|->q p).
assumption.
Qed.
#####
#
# The simplest tactics: intro, apply and assumption
# 2009aug01
#
#####
# «intro-apply-assumption» (to ".intro-apply-assumption")
# (find-coqartpage (+ 26 48) "imp_trans : (P->Q)->(Q->R)->P->R")
# (find-coqartfile "propproof/SRC/chap3.v" "imp_trans : (P->Q)->(Q->R)->P->R")
# (find-coqartfile "propproof/SRC/chap3.v" "imp_trans : (P->Q)->(Q->R)->P->R")
# (find-coqfile "")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "(p|->q)|->(q|->r)|->p|->r p|->q q|->r p")
Parameter P Q R T : Prop.
Theorem imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intros p|->q q|->r.
intro p.
apply q|->r.
apply p|->q.
assumption.
Qed.
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
\def\vdashq{\begin{picture}(0,0)\put(5,4.5){\tiny?}\end{picture}\vdash}
%:*|-?*\vdashq *
%:
%: -----------------Ð{assumption}
%: p|->q,q|->r,p|-?p
%: -----------------Ð{apply}
%: p|->q,q|->r,p|-?q
%: -----------------Ð{apply}
%: p|->q,q|->r,p|-?r
%: -------------------Ð{intro}
%: p|->q,q|->r|-?p|->r
%: -----------------------Ð{intro}
%: p|->q|-?(q|->r)|->p|->r
%: ----------------------------Ð{intro}
%: |-?(p|->q)|->(q|->r)|->p|->r
%:
%: ^imp_trans_1
%:
$$\ded{imp_trans_1}$$
intro-apply-assumption
{\myttchars
\footnotesize
\begin{verbatim}
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "(p|->q)|->(q|->r)|->p|->r p|->q q|->r p")
Parameter P Q R T : Prop.
Theorem imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intros p|->q q|->r.
intro p.
apply q|->r.
apply p|->q.
assumption.
Qed.
\end{verbatim}
}
%*
#####
#
# Composition of tactics
# 2009aug09
#
#####
# «composition» (to ".composition")
# (find-coqartpage (+ 26 62) "Simple composition")
# (find-coqartfile "propproof/SRC/chap3.v" "Lemma compose_example")
# (find-coqrefpage 181 "\nSequence")
# (find-coqreftext "\nSequence")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "p->q->r")
Parameter P Q R T : Prop.
Theorem then_example_0 : P->Q->(P->Q->R)->R.
Proof.
intros p q p->q->r.
apply p->q->r.
exact p.
exact q.
Qed.
Theorem then_example_1 : P->Q->(P->Q->R)->R.
Proof.
intros p q p->q->r.
apply p->q->r; [exact p | exact q].
Qed.
Theorem then_example_2 : P->Q->(P->Q->R)->R.
Proof.
intros p q p->q->r.
apply p->q->r; [assumption | assumption].
Qed.
Theorem then_example : P->Q->(P->Q->R)->R.
Proof.
intros p q p->q->r.
apply p->q->r; assumption.
Qed.
# (find-coqartpage (+ 26 63) "compose")
# (find-coqartfile "propproof/SRC/chap3.v" "Lemma compose_example")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "p->q->r p->q")
Parameter P Q R T : Prop.
Lemma compose_example : (P->Q->R)->(P->Q)->(P->R).
Proof.
intros p->q->r p->q p.
apply p->q->r; [assumption | apply p->q; assumption].
Qed.
#####
#
# The "cut" tactic
# 2009aug09
#
#####
# «cut» (to ".cut")
# (find-coqartpage (+ 26 68) "cut")
# (find-coqartfile "propproof/SRC/chap3.v" "Section section_for_cut_example.")
# (find-coqrefpage 141 "3. cut form")
# (find-coqrefpage 139 "8.3.6 apply term")
# (find-coqreftext "8.3.6 apply term")
# (find-coqrefpage 141 "8.3.8 assert")
# (find-coqreftext "8.3.8 assert")
# (find-coqreftext "3. cut form")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "_ p->q q->r (p->r)->t->q (p->r)->t p->r")
Parameter P Q R T : Prop.
Section section_for_cut_example.
Hypotheses (p->q : P->Q)
(q->r : Q->R)
((p->r)->t->q : (P->R)->T->Q)
((p->r)->t : (P->R)->T).
Lemma cut_example_0 : Q.
Proof.
cut (P->R).
intro p->r.
apply (p->r)->t->q.
exact p->r.
apply (p->r)->t.
exact p->r.
intro p.
apply q->r.
apply p->q.
exact p.
Qed.
Lemma cut_example_1 : Q.
Proof.
cut (P->R).
intro p->r.
apply (p->r)->t->q; [exact p->r | apply (p->r)->t; exact p->r].
intro p; apply q->r; apply p->q; exact p.
Qed.
Lemma cut_example_e : Q.
Proof (let p->r :=
fun (p:P) => q->r (p->q p) in
(p->r)->t->q p->r ((p->r)->t p->r)).
Print cut_example_0.
Print cut_example_1.
Print cut_example_e.
End section_for_cut_example.
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
%:
%: [P]^6 [P->Q]^1 [P->R]^5 [(P->R)->T]^4
%: --------------- --------------------
%: Q [Q->R]^2 [P->R]^5 T [(P->R)->T->Q]^3
%: ----------------- ------------------------------------------------
%: R Q
%: ----6 ---------5
%: P->R (P->R)->Q
%: -----------------------
%: Q
%: ---------------------------------------------1,2,3,4
%: (P->Q)->(Q->R)->((P->R)->T->Q)->((P->R)->T)->Q
%:
%: ^foo
%:
$$\footnotesize \ded{foo}$$
%*
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "_ ((p->q)->q)->q p->q")
Parameter P Q R T : Prop.
Lemma triple_impl2 : (((P->Q)->Q)->Q)->P->Q.
Proof.
auto.
Qed.
Print triple_impl2.
Lemma triple_imple : (((P->Q)->Q)->Q)->P->Q.
Proof (fun (H : ((P->Q)->Q)->Q) (H0 : P) =>
H (fun H1 : P->Q =>
H (fun _ : P->Q =>
H (fun _ : P->Q =>
H1 H0))))
: (((P->Q)->Q)->Q)->P->Q .
Print triple_imple.
Lemma triple_impld : (((P->Q)->Q)->Q)->P->Q.
Proof (fun (((p->q)->q)->q:((P->Q)->Q)->Q) (p:P) =>
((p->q)->q)->q (fun p->q:P->Q =>
((p->q)->q)->q (fun _:P->Q =>
((p->q)->q)->q (fun _:P->Q =>
p->q p))))
: (((P->Q)->Q)->Q)->P->Q .
Print triple_impld.
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
%: [P]^2 [P->Q]^4
%: ---------------
%: Q
%: ---------5
%: (P->Q)->Q [((P->Q)->Q)->Q]^1
%: --------------------------
%: Q
%: ---------4
%: (P->Q)->Q [((P->Q)->Q)->Q]^1
%: ---------------------------
%: Q
%: ---------3
%: (P->Q)->Q [((P->Q)->Q)->Q]^1
%: ---------------------------
%: Q
%: ----2
%: P->Q
%: ----------------------1
%: (((P->Q)->Q)->Q)->P->Q
%:
%: ^triple_impl_auto
%:
$$\footnotesize
\ded{triple_impl_auto}
$$
%*
#####
#
# E-mail about 7-uples to the Coq-Club mailing list
# 2009aug01
#
#####
# «email-about-7-uples» (to ".email-about-7-uples")
# http://pauillac.inria.fr/pipermail/coq-club/2009/005078.html
Hello list,
this is probably a basic question (I'm a newbie) but anyway, here it
goes... If abcdefg is a 7-uple - with a complex dependent type - is
there a way to extract all its components at once? Something like this
would be ideal,
Definition (a, b, c, d, e, f, g) := abcdefg.
but this is not accepted...
Let me explain how I arrived at this problem. I am trying to use Coq
to formalize a certain notation that I have been using for years for
doing constructions and proofs in Category Theory, and I tried to do
this:
(* ------ snip, snip ------ *)
Definition type_of (T : Type) (t : T) := T.
Implicit Arguments type_of [T].
Section Categories.
Variable C_0 : Type.
Variable Hom_C : C_0 -> C_0 -> Set.
Variable id_C : forall (A : C_0), Hom_C A A.
Variable o_C : forall (A B C : C_0) (g : Hom_C B C) (f : Hom_C A B),
Hom_C A C.
Implicit Arguments o_C [A B C].
Variable idL_C : forall (A B : C_0) (f : Hom_C A B),
(o_C (id_C _) f = f).
Implicit Arguments idL_C [A B].
Variable idR_C : forall (A B : C_0) (f : Hom_C A B),
(o_C f (id_C _) = f).
Implicit Arguments idR_C [A B].
Variable assoc_C : forall (A B C D : C_0)
(f : Hom_C A B) (g : Hom_C B C) (h : Hom_C C D),
(o_C h (o_C g f) = o_C (o_C h g) f).
Implicit Arguments assoc_C [A B C D].
Definition C := (C_0, Hom_C, id_C, o_C, idL_C, idR_C, assoc_C).
Definition C_minus := (C_0, Hom_C, id_C, o_C).
Definition Category := type_of C.
Definition Protocategory := type_of C_minus.
Variable D : Category.
Definition (D_0, Hom_D, id_D, o_D, idL_D, idR_D, assoc_D) := D. (* <- *)
Definition D_minus := (C_0, Hom_C, id_C, o_C).
(* etc... *)
end Categories.
(* ------ snip, snip ------ *)
It would be fantastic if the "(* <- *)" line above would be accepted,
but it isn't... Any hints, suggestions, pointers, workarounds (using
records, maybe)?...
Thanks in advance,
Eduardo Ochs
eduardoochs@gmail.com
http://angg.twu.net/
#####
#
# Dependent projections (an attempt to solve the problem above)
# 2009aug01
#
#####
# «dependent-projections» (to ".dependent-projections")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section foo.
Variable A : Set.
Variable a : A.
Variable B : forall (a:A), Set.
Variable b : B a.
Variable C : forall (a:A) (b:B a), Set.
Variable c : C a b.
Variable D : forall (a:A) (b:B a) (c:C a b), Set.
Variable d : D a b c.
Check d.
Check (a,b,c,d).
End foo.
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section foo.
Variable A : Set.
Variable B : forall (a:A), Set.
Variable C : forall (a:A) (b:B a), Set.
Variable D : forall (a:A) (b:B a) (c:C a b), Set.
Section abcd.
Variable a : A.
Variable b : B a.
Variable c : C a b.
Variable d : D a b c.
Check d.
Check (a,b,c,d).
Record ABCD' : Set := mkabcd' {
a' : A; b' : B a'; c' : C a' b'; d' : D a' b' c'
}.
Check a'.
Check d'.
End abcd.
Record ABCD : Set := mkabcd {
a : A; b : B a; c : C a b; d : D a b c
}.
Check a.
Check d.
End foo.
# (find-coqrefw3m "Reference-Manual004.html#Letin")
Coq < Record Rat : Set := mkRat
Coq < {sign : bool;
Coq < top : nat;
Coq < bottom : nat;
Coq < Rat_bottom_cond : 0 <> bottom;
Coq < Rat_irred_cond :
Coq < forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
Rat is defined
Rat_rect is defined
Rat_ind is defined
Rat_rec is defined
sign is defined
top is defined
bottom is defined
Rat_bottom_cond is defined
Rat_irred_cond is defined
#####
#
# Proving that ab=1 -> a=1 (in Nat; just the beginning)
# 2009jul30
#
#####
# «ab=1-implies-a=1» (to ".ab=1-implies-a=1")
# (find-coqrefpage 47 "\n2.1 Record types")
# (find-coqreftext "\n2.1 Record types")
# (find-coqfile "")
# (find-coqfile "theories/Arith/")
# (find-coqfile "theories/Arith/Mult.v" "mult_lt_compat_r")
# (find-coqfile "theories/Arith/Compare.v")
# (find-angg "COQ/dnc-0.el")
# (load "~/COQ/dnc-0.el")
;;
;; [a>1]^2 [b>0]^1 [b>0]^1
;; ---------------- -------
;; [a<1]^2 [b=0]^1 ab>b b>=1
;; ------- ------- ------------------
;; a=0 ab=0 ab>1
;; ---- -------- ----- -----
;; a~=1 ab=0 b=0\/b>0 ab~=1 ab~=1
;; ------- ----- -----------------------------------
;; a<1\/a>1 ab~=1 ab~=1
;; -------------------------------------
;; ab~=1
;;
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export ZArith.
Require Export Arith.
Require Export Bool.
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Require Export Omega.
Open Scope nat_scope.
Theorem foo : forall a b : nat, b > 1 -> a <= a * b.
intros. omega.
#####
#
# Coq mode for Emacs
# 2009jul29
#
#####
# «coq-mode» (to ".coq-mode")
# (find-fline "/etc/emacs/site-start.d/50coq.el")
# (find-fline "/usr/share/emacs/site-lisp/coq/coq.el")
# (find-fline "/usr/share/emacs/22.2/lisp/obsolete/hilit19.el.gz")
# (load "/usr/share/emacs/22.2/lisp/obsolete/hilit19.el.gz")
# (find-coqfile "theories/Init/Notations.v")
# No font-locking on emacs23... 8-\
# http://web.math.unifi.it/~maggesi/mechanized/emacs/coq.el
# http://web.math.unifi.it/~maggesi/mechanized/emacs/inferior-coq.el
# http://web.math.unifi.it/users/maggesi/mechanized/emacs/coq.el
#####
#
# Mailing list and links
# 2009aug01
#
#####
# «mailing-list» (to ".mailing-list")
# http://pauillac.inria.fr/mailman/listinfo/coq-club
# http://pauillac.inria.fr/pipermail/coq-club/
# http://www.reddit.com/r/dependent_types
# http://www.reddit.com/r/dependent_types/comments/95efw/has_anyone_studied_this_type_theory/
# http://www.reddit.com/r/Coq
# http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/bertot_coq.pdf
# http://www.seas.upenn.edu/~cis500/cis500-f07/schedule.html
#####
#
# Print string
# 2009aug05
#
#####
# «print-string» (to ".print-string")
# http://pauillac.inria.fr/pipermail/coq-club/2009/005090.html
#####
#
# Search
# 2009aug09
#
#####
# «search» (to ".search")
# (find-coqrefw3m "general-index.html" "Search")
# (find-coqrefw3m "general-index.html" "SearchAbout")
# (find-coqrefw3m "general-index.html" "SearchPattern")
# (find-coqtut3w3m "#htoc30")
# (find-coqhurrypage 1)
# (find-coqhurrytext)
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
SearchAbout and.
SearchAbout (_ /\ _ -> _).
SearchPattern (_ /\ _ -> _).
SearchPattern (_ /\ _ -> _).
(* User error: the pattern is not simple enough *)
SearchPattern (_ = _).
#####
#
# Conjunction
# 2009aug09
#
#####
# «conjunction» (to ".conjunction")
# (find-coqrefw3m "general-index.html")
# (find-coqrefw3m "toc.html")
# (find-coqrefw3m "tactic-index.html" "intuition")
# (find-coqrefw3m "Reference-Manual010.html#intuition")
# (find-coqrefw3m "Reference-Manual011.html#intuition")
# (find-coqreftext "8.12.4 intuition tactic")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "_ p&q q&p")
Parameters P Q R T : Prop.
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intuition.
Qed.
Print and_commutes.
# (find-coqrefpage 333)
# (find-coqrefpage 341)
# (find-coqrefpage 149 "elim")
# (find-coqrefpage 146)
# (find-coqrefpage 148 "3. split")
# (find-coqreftext "3. split")
# (find-coqtut1w3m "#htoc7" "Conjunction")
# (find-coqtuttext "1.3.1 Conjunction")
# (find-coqtut1w3m "#htoc7" "apply conj")
# (find-coqtuttext "apply conj")
# (find-coqartpage (+ 26 121) "5.2.4 Conjunction and disjunction")
# (find-coqartfile "everyday/SRC/chap5.v")
# (find-coqartfile "everyday/SRC/chap5.v" "Lemma and_commutes")
# (find-coqlibdocw3m "Coq.Init.Logic.html")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Parameters P Q R T : Prop.
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intro pq.
split.
exact (proj2 pq).
exact (proj1 pq).
Qed.
Print and_commutes.
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "_ p&q q&p")
Parameters P Q R T : Prop.
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intro p&q.
split.
exact (proj2 p&q).
exact (proj1 p&q).
Qed.
Print and_commutes.
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
* (load "~/COQ/dnc-0.el")
* (dnc-strings "_ p->q p->r q&r")
Parameter P Q R T : Prop.
Theorem conj_foo : P -> (P -> Q) -> (P -> R) -> Q /\ R.
Proof.
intros p p->q p->r.
split.
exact (p->q p).
exact (p->r p).
Qed.
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-coqtutw3m "#htoc8" "Disjunction")
Lemma or_commutative : A \/ B -> B \/ A.
intro H; elim H.
intro HA.
clear H.
right.
trivial.
auto.
#####
#
# Sections
# 2009aug09
#
#####
# «sections» (to ".sections")
# (find-coqrefpage 337 "let")
# (find-coqrefpage 48 "let")
# (find-coqrefpage 49 "dot notation")
# (find-coqrefpage 50 "let ... in ...")
# (find-coqreftext 337 "let")
# Two kinds of sanity checks:
# typeof ab = AB
# AB = record bleh
# (find-coqrefpage 55 "Sections")
# (find-coqreftext)
# (find-coqreftext "2.4 Section mechanism")
# (find-coqreftext "\n2.4 Section mechanism")
# (find-coqreftext 337 "let")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Section s1.
Variables x y : nat.
Let y' := y.
Definition x' := S x.
Definition x'' := x' + y'.
Print x'.
End s1.
Print x'.
Print x''.
#####
#
# Agda
# 2009sep23
#
#####
# «agda» (to ".agda")
# http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html
# http://wiki.portal.chalmers.se/agda/agda.php
# http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html
# http://ftp.de.debian.org/debian/pool/main/a/agda/
# http://ftp.de.debian.org/debian/pool/main/a/agda/agda_2.2.4+dfsg-1.dsc
# http://ftp.de.debian.org/debian/pool/main/a/agda/agda_2.2.4+dfsg-1.diff.gz
# http://ftp.de.debian.org/debian/pool/main/a/agda/agda_2.2.4+dfsg.orig.tar.gz
# http://ftp.de.debian.org/debian/pool/main/a/agda-bin/
# http://ftp.de.debian.org/debian/pool/main/a/agda-bin/agda-bin_2.2.4-1.dsc
# http://ftp.de.debian.org/debian/pool/main/a/agda-bin/agda-bin_2.2.4-1.diff.gz
# http://ftp.de.debian.org/debian/pool/main/a/agda-bin/agda-bin_2.2.4.orig.tar.gz
# http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download
# http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.InstallationOfAgdaFromSourceForNonprogrammers
# http://www.cs.swan.ac.uk/~csetzer/othersoftware/agda2/agda2installation.html
# (find-es "eev" "apt-ftparchive")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/ag/
mkdir /tmp/ag/
cd /tmp/ag/
cp -v $S/http/ftp.de.debian.org/debian/pool/main/a/agda-bin/* .
cp -v $S/http/ftp.de.debian.org/debian/pool/main/a/agda/* .
mkdir -p dists/./main/source/
laf
apt-ftparchive sources .
apt-ftparchive sources . \
| gzip -c9 > dists/./main/source/Sources.gz
# (find-fline "/etc/apt/sources.list")
# deb-src file:///tmp/ag . main
sudo apt-get install
sudo apt-get build-dep agda
# Featherweight Java:
# http://pauillac.inria.fr/pipermail/coq-club/2009/005115.html
# (find-fline "~/tmp/featherj.zip")
# http://users.dimi.uniud.it/~marino.miculan/data/downloads/TYPES02.pdf
# (find-fline "~/LOGS/2009aug09.coq")
Ltac abstr_proofs :=
match goal with
| |- context [?e] =>
match type of e with
| ?T =>
match type of T with
| Prop =>
let H := fresh "prf" in
set (H := e) in |- *; generalize H; clear H
end
end
end
http://packages.debian.org/source/sid/ssreflect
http://homepages.inf.ed.ac.uk/ratkey/parametricity/
#####
#
# Notas para a oficina de assistentes de provas
# 2009oct23
#
#####
# «oficina» (to ".oficina")
# (find-efunction 'eev-oficina-settings)
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Parameter P Q R : Prop.
Theorem imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intros p_q q_r.
intro p.
apply q_r.
apply p_q.
assumption.
Qed.
Print imp_trans.
Lemma and_commutes : P /\ Q -> Q /\ P.
Proof.
intro pq.
split.
exact (proj2 pq).
exact (proj1 pq).
Qed.
Print and_commutes.
#####
#
# Adam Chlipala's "Certified Programming with Dependent Types" book
# 2010jan13
#
#####
# «cpdt» (to ".cpdt")
# http://adam.chlipala.net/
# http://adam.chlipala.net/cpdt/
# http://adam.chlipala.net/cpdt/html/toc.html
# http://adam.chlipala.net/cpdt/html/Intro.html
# http://adam.chlipala.net/cpdt/html/StackMachine.html
#####
#
# Coq in a hurry
# 2010feb25
#
#####
# «coq-in-a-hurry» (to ".coq-in-a-hurry")
# http://cel.archives-ouvertes.fr/inria-00001173/
# http://cel.archives-ouvertes.fr/docs/00/45/91/39/PDF/coq-hurry.pdf
(code-xpdf "coqinahurry" "$S/http/cel.archives-ouvertes.fr/docs/00/45/91/39/PDF/coq-hurry.pdf")
(code-pdftotext "coqinahurry" "$S/http/cel.archives-ouvertes.fr/docs/00/45/91/39/PDF/coq-hurry.pdf")
;; (find-coqinahurrypage 1 "Contents")
;; (find-coqinahurrypage (+ 1 1) "Index")
;; (find-coqinahurrytext "")
#####
#
# Monoid (ideas - that I don't understand - from the Coq-club list)
# 2010apr14
#
#####
# «monoid» (to ".monoid")
# http://article.gmane.org/gmane.science.mathematics.logic.coq.club/4796
# http://article.gmane.org/gmane.science.mathematics.logic.coq.club/4797
# http://article.gmane.org/gmane.science.mathematics.logic.coq.club/4799
Class Monoid (Carrier:Set)(mult:Carrier->Carrier->Carrier) :=
{ neutral : Carrier
; identL : forall a, (mult a neutral) = a
; identR : forall a, (mult neutral a) = a
; assoc : forall a b c, (mult a (mult b c)) = (mult (mult a b) c)
}.
Class SemiGroupOp A := sg_op: A -> A -> A.
Infix "&" := sg_op (at level 50, left associativity).
[
It would be nicer to write:
Class SemiGroupOp A := (&) : A -> A -> A.
Like in haskell.
]
and then:
Context A {e: Equiv A}.
Class Setoid: Prop := setoid_eq:> Equivalence (@equiv A e).
Class SemiGroup {op: SemiGroupOp A}: Prop :=
{ sg_setoid:> Setoid
; sg_ass:> Associative sg_op
; sg_mor:> Proper (e ==> e ==> e)%signature sg_op }.
Class Monoid {op: SemiGroupOp A} {unit: MonoidUnit A}: Prop :=
{ monoid_semigroup:> SemiGroup
; monoid_left_id:> LeftIdentity sg_op mon_unit
; monoid_right_id:> RightIdentity sg_op mon_unit }.
Class Group {op: SemiGroupOp A} {unit: MonoidUnit A} {inv: GroupInv
A}: Prop :=
{ group_monoid:> Monoid
; inv_proper:> Proper (e ==> e) inv
; ginv_l: `(- x & x = mon_unit)
; ginv_r: `(x & - x = mon_unit) }.
#####
#
# ProofWeb
# 2010jun26
#
#####
# «proofweb» (to ".proofweb")
# (find-angg ".emacs.papers" "proofweb")
http://r6research.livejournal.com/
http://perso.ens-lyon.fr/aurelien.pardon/coq/index.html
http://www.lri.fr/~lescuyer/software.en.html
http://cs.ru.nl/~Adam.Koprowski/teaching/Coq/assignments07.pdf
http://www.alumnos.unican.es/ccc66/coq.htm
http://www.alumnos.unican.es/ccc66/coq/usingensembles.v
# Local Variables:
# coding: raw-text-unix
# ee-delimiter-hash: "\n#*\n"
# ee-delimiter-percent: "\n%*\n"
# ee-anchor-format: "«%s»"
# End: