|
Warning: this is an htmlized version!
The original is here, 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.
# An introduction to eev can be found here:
#
# (find-eev-quick-intro)
# http://angg.twu.net/eev-intros/find-eev-quick-intro.html
#
# 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-debs-2020» (to "coq-debs-2020")
# «.coq-from-git» (to "coq-from-git")
# «.coq-from-opam» (to "coq-from-opam")
# «.coqtop» (to "coqtop")
# «.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-old» (to "proofgeneral-old")
# «.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")
# «.Locate» (to "Locate")
# «.irc-channels» (to "irc-channels")
# «.HOTT» (to "HOTT")
# «.performant-CT» (to "performant-CT")
# «.CS1-through-TT» (to "CS1-through-TT")
# «.sub-universe» (to "sub-universe")
# «.primitive-recursion» (to "primitive-recursion")
# «.why-dependent-type-theory» (to "why-dependent-type-theory")
# «.ND-cheat-sheet» (to "ND-cheat-sheet")
# «.CIC» (to "CIC")
# «.theory-behind-coq» (to "theory-behind-coq")
# «.extensional-equality» (to "extensional-equality")
# «.proof-irrelevance» (to "proof-irrelevance")
# «.proof-general» (to "proof-general")
# «.prooftree» (to "prooftree")
# «.logical-foundations» (to "logical-foundations")
# «.ctpe» (to "ctpe")
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
# (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-debs-2020
# 2020oct11
#
#####
# «coq-debs-2020» (to ".coq-debs-2020")
# (find-zsh "installeddebs | sort | grep coq")
# (find-zsh "availabledebs | sort | grep coq")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
apti coq
# (find-status "coq")
# (find-vldifile "coq.list")
# (find-udfile "coq/")
#####
#
# Coq from Git
# 2020oct12
#
#####
# «coq-from-git» (to ".coq-from-git")
# https://github.com/coq/coq/releases/latest
# https://github.com/coq/coq
# https://coq.github.io/doc/master/api/
# https://coq.github.io/doc/master/stdlib/
# https://coq.github.io/doc/master/refman/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/coq/
cd ~/usrc/
git clone https://github.com/coq/coq
cd ~/usrc/coq/
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
# (find-fline "~/usrc/")
# (find-fline "~/usrc/coq/")
# (find-gitk "~/usrc/coq/")
# (code-c-d "coqsrc" "~/usrc/coq/")
# (find-coqsrcfile "")
# (find-coqsrcfile "doc/")
# (find-coqsrcfile "INSTALL.md")
# (find-coqsrcfile "INSTALL.md" "ZArith")
# (find-coqsrcfile "INSTALL.md" "eval $(opam env)")
# (find-coqsrcfile "README.md" "https://coq.zulipchat.com/")
# (find-coqsrcfile "Makefile")
apti libzarith-ocaml-dev libfindlib-ocaml-dev liblablgtk3-ocaml-dev
apti libgtksourceview-3.0-dev
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/coq/
./configure |& tee oc
make |& tee om
opam env
eval $(opam env)
nice opam init
nice opam install ocamlfind zarith lablgtk3-sourceview3
#####
#
# coq-from-opam
# 2020oct12
#
#####
# «coq-from-opam» (to ".coq-from-opam")
# (find-es "ocaml" "opam-init")
# (find-man "1 opam")
# (find-man "1 opam-init")
# (find-man "1 opam-switch")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/.opam/*
# opam switch create coq 4.11.1+flambda
cd
opam init -v -v -v -v -n
opam env
eval $(opam env)
opam -v install ocamlfind zarith lablgtk3-sourceview3
<><> Creating initial switch (ocaml-system>=4.02.3) <><><><><><><><><><><><><><>
+ /usr/bin/lsb_release "-s" "-r"
- 10
# (find-man "lsb_release")
# (find-sh "lsb_release -s -r")
-r, --release
Display the release number of the currently installed distribution.
-c, --codename
Display the code name of the currently installed distribution.
-a, --all
Display all of the above information.
-s, --short
Use the short output format for any information displayed. This format omits the
leading header(s).
#####
#
# coqtop
# 2020oct11
#
#####
# «coqtop» (to ".coqtop")
# (find-man "1 coqtop")
# (find-sh "coqtop --help")
# https://coq.inria.fr/refman/practical-tools/coq-commands.html
# (find-fline "~/LOGS/20201012.coq")
<pgiarrusso> edrx: coqtop -load-vernac-source Basics.v might help
(https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-command-line-options),
# (find-coqsrcfile "toplevel/")
# (find-coqsrcfile "toplevel/coqtop.ml")
#####
#
# 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-old» (to ".proofgeneral-old")
# (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 / 2020jan03
#
#####
# «mailing-list» (to ".mailing-list")
# https://sympa.inria.fr/sympa/arc/coq-club/
# https://sympa.inria.fr/sympa/arc/coq-club/2020-01/
# Old links:
# 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")
# (find-es "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://proofweb.cs.ru.nl/login.php
http://proofweb.cs.ru.nl/man.pdf
http://proofweb.cs.ru.nl/install.php
#####
#
# Locate
# 2013jan01
#
#####
# «Locate» (to ".Locate")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Locate "exists2".
# Search "exists2".
# Check "exists2".
# will describe what the notation means. It is defined in
# http://coq.inria.fr/V8.4/stdlib/Coq.Init.Logic.html and it should
# also hint you toward your second question.
#####
#
# IRC channels
# 2013jul12
#
#####
# «irc-channels» (to ".irc-channels")
Hello,
Just a quick note that there is now a channel on the freenode IRC
network for real time discussion of Homotopy Type Theory and related
topics.
The channel is ##hott (please note the double hash!) on
irc://chat.freenode.net and currently has around 20 users and growing.
For reference, the freenode IRC network has an active community of
type theory enthusiasts, functional programmers, and mathematicians in
various channels, including ##categorytheory, ##logic, #agda, #coq,
#epigram, #haskell, #idris, #ocaml, and others. Across these channels
there are now upwards of 1000 users.
One can find more information on the freenode IRC network, including
software or web-based IRC clients, at https://freenode.net
We are hoping the ##hott channel can be a useful resource for
interested parties. Please feel free to repost this information
elsewhere.
(find-freenode "##hott")
(find-freenode "##categorytheory")
(find-freenode "##logic")
(find-freenode "#agda")
(find-freenode "#coq")
(find-freenode "#epigram")
(find-freenode "#haskell")
(find-freenode "#idris")
(find-freenode "#ocaml")
#####
#
# HOTT
# 2013aug01
#
#####
# «HOTT» (to ".HOTT")
http://www.homotopytypetheory.org/book
http://homotopytypetheory.org/2013/06/20/the-hott-book/
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html
http://math.andrej.com/2013/06/20/the-hott-book/
https://github.com/HoTT/book/issues/292
http://ncatlab.org/nlab/show/homotopy+type+theory
https://groups.google.com/forum/#!forum/hott-amateurs
http://hottheory.files.wordpress.com/2013/03/hott-online-207-g21ac918.pdf
;; (find-fline "$S/http/hottheory.files.wordpress.com/2013/03/")
(code-xpdf "hottbook" "$S/http/hottheory.files.wordpress.com/2013/03/hott-online-207-g21ac918.pdf")
(code-pdf-text "hottbook" "$S/http/hottheory.files.wordpress.com/2013/03/hott-online-207-g21ac918.pdf")
;; (find-hottbookpage)
;; (find-hottbooktext)
#####
#
# Performant CT
# 2014jun16
#
#####
# «performant-CT» (to ".performant-CT")
In my experience using several definitions (e.g. for a group to have
the "group_carrier", "group_data", then "group_axioms" consisting of
"group_assoc", "group_unit", "group_inverse" all of these being
separate definitions, then "group" consisting of "group_data" and
"group_axioms") makes things much much faster since Coq does not
unfold the internal definitions unless necessary.
# https://mail.google.com/mail/ca/u/0/#inbox/1469ba68b7d2b9ac
# http://people.csail.mit.edu/jgross/#category-coq-experience
# http://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission-final.pdf
;; (find-fline "$S/http/people.csail.mit.edu/jgross/personal-website/papers/")
(code-xpdf "performantctcoq" "$S/http/people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission-final.pdf")
(code-pdf-text "performantctcoq" "$S/http/people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission-final.pdf")
;; (find-performantctcoqpage)
;; (find-performantctcoqtext)
http://users.cecs.anu.edu.au/~okeefe/work/fcat4cats04.pdf
#####
#
# CS1 Through Type Theory
# 2016nov06
#
#####
# «CS1-through-TT» (to ".CS1-through-TT")
# https://github.com/kevinsullivan/cs1113f16
# 2018fev19:
From: Gert Smolka
To: Kevin Sullivan
We cover intuitionistic / classical ND in an introductory class using Coq,
see lecture notes and Coq files at https://courses.ps.uni-saarland.de/icl_17/2/Resources.
This includes Glivenko's theorem.
There is also a Coq development of Gentzen's intuitionistic sequent calculus
showing that it is decidable and intereducible with intuitionistic ND, see
http://www.ps.uni-saarland.de/courses/cl-ss16/LectureNotes/html/toc.html.
https://courses.ps.uni-saarland.de/icl_17/2/Resources
http://www.ps.uni-saarland.de/courses/cl-ss16/LectureNotes/html/toc.html
#####
#
# sub-universe
# 2019apr06
#
#####
# «sub-universe» (to ".sub-universe")
From Vladimir Voevodsky, on Coq-club, 2010sep09:
Actually, as I have accidentally discovered recently there is a way to
control the universe assignment in Coq. For example, one can start
one's development with something like that:
Definition Type1:=Type.
Definition Type0:Type1:=Type.
Definition jj01:Type0 -> Type1:= fun T => T.
This fixes two universes Type0 and Type1 such that Type0:Type1 and
Type0 is a sub-universe of Type1. In further development you may use
Type0 or Type1 everywhere instead of Type. Some definitions may have
to be repeated twice once for Type0 and once for Type1.
#####
#
# primitive-recursion
# 2019apr06
#
#####
# «primitive-recursion» (to ".primitive-recursion")
# https://coq.inria.fr/tutorial/2-induction
# http://adam.chlipala.net/cpdt/html/GeneralRec.html
# https://cstheory.stackexchange.com/questions/20578/is-the-class-of-primitive-recursion-functionals-equivalent-to-the-class-of-funct
#####
#
# Why Dependent Type Theory? (Thread at Coq-Club)
# 2020mar04
#
#####
# «why-dependent-type-theory» (to ".why-dependent-type-theory")
# https://mail.google.com/mail/ca/u/0/#inbox/FMfcgxwHMGCPMstQGdzDJDjDZmWdqFdL
# https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00032.html
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00038.html "proving 2 + 2 = 4 requires on the order of 10^7 symbols"
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00018.html meaning (a la Martin-Lof)
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00016.html kubota
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00019.html eauto 7 min / 2 hours
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00025.html videos
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00030.html termination
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00034.html f91 in hol
https://sympa.inria.fr/sympa/arc/coq-club/2020-03/msg00035.html true , false} \cup {0,1,2,3}
#####
#
# ND-cheat-sheet
# 2020mar27
#
#####
# «ND-cheat-sheet» (to ".ND-cheat-sheet")
# https://www.cosc.brocku.ca/~mwinter/Courses/4P42/
# https://www.cosc.brocku.ca/~mwinter/Courses/4P42/CheatSheet.pdf
(code-pdf-page "ndcheatsheet" "$S/https/www.cosc.brocku.ca/~mwinter/Courses/4P42/CheatSheet.pdf")
(code-pdf-text "ndcheatsheet" "$S/https/www.cosc.brocku.ca/~mwinter/Courses/4P42/CheatSheet.pdf")
;; (find-ndcheatsheetpage)
;; (find-ndcheatsheettext)
#####
#
# The Calculus of Inductive Constructions
# 2020mar27
#
#####
# «CIC» (to ".CIC")
# https://coq.inria.fr/refman/language/cic.html
# (find-books "__logic/__logic.el" "paulin-mohring")
# (find-books "__comp/__comp.el" "dybjer")
#####
#
# theory-behind-coq
# 2020mar27
#
#####
# «theory-behind-coq» (to ".theory-behind-coq")
# https://github.com/coq/coq/wiki/TheoryBehindCoq
#####
#
# extensional-equality
# 2020apr05
#
#####
# «extensional-equality» (to ".extensional-equality")
# https://github.com/coq/coq/wiki/extensional_equality
# https://en.wikipedia.org/wiki/Extensionality
#####
#
# proof-irrelevance
# 2020apr12
#
#####
# «proof-irrelevance» (to ".proof-irrelevance")
# https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-is-proof-irrelevance
# https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-is-streichers-axiom-k
#####
#
# proof-general (from MELPA)
# 2020oct11
#
#####
# «proof-general» (to ".proof-general")
# (find-angg ".emacs" "proof-general")
# (find-epackage-links 'proof-general)
# (find-epackage 'proof-general)
# (code-c-d "proofgeneral" "~/.emacs.d/elpa/proof-general-20200911.3/" "ProofGeneral")
# (find-proofgeneralnode "")
# (find-proofgeneralfile "")
# (find-proofgeneralfile "coq/coq-mode.el")
# https://proofgeneral.github.io/
# (find-proofgeneralnode "Walkthrough example in Isabelle")
# (find-proofgeneralnode "Walkthrough example in Isabelle" "theorem my_theorem:")
# (find-proofgeneralnode "Coq Proof General")
#####
#
# prooftree
# 2020oct11
#
#####
# «prooftree» (to ".prooftree")
# http://askra.de/software/prooftree/
#####
#
# Logical Foundations (vol. 1 of Software Foundations)
# 2020oct11
#
#####
# «logical-foundations» (to ".logical-foundations")
# https://coq.inria.fr/documentation
# https://softwarefoundations.cis.upenn.edu/
# https://softwarefoundations.cis.upenn.edu/lf-current/index.html
# https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/coq-sf/lf/")
rm -Rv ~/usrc/coq-sf/lf/
mkdir -p ~/usrc/coq-sf/lf/
tar -C ~/usrc/coq-sf/ \
-xvzf $S/https/softwarefoundations.cis.upenn.edu/lf-current/lf.tgz
cd ~/usrc/coq-sf/lf/
# (code-c-d "coqlf" "~/usrc/coq-sf/lf/")
# (find-coqlffile "")
# (find-coqlffile "Basics.v")
# file:///home/edrx/usrc/coq-sf/lf/index.html
# file:///home/edrx/usrc/coq-sf/lf/toc.html
# file:///home/edrx/usrc/coq-sf/lf/Basics.html
#####
#
# Coq Tactics in Plain English
# 2024apr19
#
#####
# «ctpe» (to ".ctpe")
# https://charlesaverill.github.io/ctpe/
# https://charlesaverill.github.io/ctpe/?s=35 Coq Tactics in Plain English
# https://github.com/CharlesAverill/ctpe
# (code-c-d "ctpe" "~/usrc/ctpe/")
# (find-ctpefile "")
https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html
https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html
https://flint.cs.yale.edu/cs428/coq/doc/Reference-Manual012.html
https://le.qun.ch/en/blog/coq/ Coq Tricks for Beginners with Too Many Examples
https://julesjacobs.com/notes/coq-cheatsheet/coq-cheatsheet.pdf
https://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf
# https://github.com/coq/coq/wiki/Alternative-names
# https://geekfeminism.wikia.org/wiki/Zipper_incident
;; https://www.dc.fi.udc.es/staff/freire/coqdoc/pauillac.inria.fr/coq/doc/n125.htm
http://coq.inria.fr/cocorico/SquareRootTwo
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
http://www-sop.inria.fr/lemme/Laurent.Chicli/index.html
http://www-sop.inria.fr/lemme/personnel/Laurent.Chicli/FrCoq.html
http://www.xs4all.nl/~weegen/eelis/research/math-classes/
http://www.xs4all.nl/~weegen/eelis/research/math-classes/mscs.pdf
C-zar:
http://coq.inria.fr/V8.2pl1/refman/Reference-Manual014.html
http://askra.de/software/coq-tree/proof-tree.jpg
http://askra.de/software/prooftree/
https://github.com/pilki/cases
http://mws.cs.ru.nl/proviola/index.html
[1] Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk.
Proviola: a tool for proof re-animation. Intelligent Computer
Mathematics, volume LNAI 6167 of Lecture Notes in Artifical
Intelligence, pages 440 - 454. March 2010. Preprint available
through http://cs.ru.nl/~carst/files/proviola.pdf.
[2] Carst Tankink, Herman Geuvers, and James McKinna. Narrating
formal proof (work in progress). In User Interfaces for Theorem
Provers 2010. To appear in an issue of ENTCS. Available through
http://www.cs.ru.nl/~carst/files/narration.pdf
let me give you some references to "intrinsic typing", a technique of
ensuring welltypedness of terms by dependent types of the metalevel. All
of the references implement abstract syntax in Coq.
This one is a quite pedagogical, because very detailed, account of
intrinsic typing:
N Benton, C-K Hur, A Kennedy and C McBride. Strongly Typed Term
Representations in Coq.
http://research.microsoft.com/en-us/um/people/nick/jartypedsyntax.pdf
Intrinsic typing for the simply--typed syntax associated to a signature
is used in
V Capretta, A Felty. Higher-Order Abstract Syntax in Type Theory
http://www.site.uottawa.ca/~afelty/dist/lc06.pdf
http://www.site.uottawa.ca/~afelty/coq/HOUA.v
http://www.site.uottawa.ca/~afelty/coq/TLC.v
and
B Ahrens, J Zsido. Initial Semantics for higher-order typed syntax in Coq.
http://jfr.cib.unibo.it/article/view/2066
http://jfr.cib.unibo.it/article/view/1695
http://www.lix.polytechnique.fr/~barras/proofs/sets/index.html
http://people.debian.org/~schepler/coqtut.v.pdf
http://www.people.fas.harvard.edu/~gmalecha/
http://www.cs.st-andrews.ac.uk/~vk/doc/subfold.pdf
http://www.cs.ru.nl/~spitters/coqw_files/program.html
http://lacl.u-pec.fr/polonowski/Develop/Generic_Env/gen-env.html
http://richmodels.epfl.ch/
2012may10: [Coq-Club] Alternate proof that classic -> proof_irrelevance
http://www-sop.inria.fr/lemme/Frederique.Guilhot/
http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath
http://math-classes.org/
I've been looking and thinking about how you would introduce freshmen
to discrete math using Coq, and again looking at the Gries and
Schneider book "A Logical Approach to Discrete Math," I rather like
it...
http://iron.ouroborus.net/ Iron Lambda
http://www.lama.univ-savoie.fr/~david/ftp/experiment.ps
http://www.lama.univ-savoie.fr/~david/ftp/pate07.pdf
http://www.ps.uni-saarland.de/courses/cl-ss11/script/icl.pdf
http://math.unice.fr/~ah/div/bghp.pdf
http://www.lama.univ-savoie.fr/~raffalli/?page=cours&lang=fr
https://wiki.mq.edu.au/display/plrg/Resources
http://www.youtube.com/watch?v=l6zqLJQCnzo How to use Coq with Proof General
http://coq.inria.fr/cocorico/Other%20Coq%20Resources
http://fuscia.info/cours/coq/
http://www-sop.inria.fr/members/Yves.Bertot/coq-master1.html
http://www.inria.fr/sophia/members/Yves.Bertot/coqartF.pdf
http://www.labri.fr/Perso/%7Ecasteran/CoqArt/index.html
http://www.mpi-sws.org/~beta/Publications.html
Jeremy Avigad's message to FOM with links about formalized maths:
http://www.cs.nyu.edu/pipermail/fom/2014-October/018221.html
http://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory.html
http://www.wired.com/2015/05/will-computers-redefine-roots-math/ ***
http://217.67.21.78/doc/coq/coq-8.5-hack/index.html Show Tree
http://tlringer.github.io/pdf/analytics.pdf REPLica: REPL Instrumentation for Coq Analysis
https://deducteam.github.io/ Dedukti
http://logipedia.inria.fr/about/about.php
https://gist.github.com/codyroux/1ec2a59ef57cdebebef1b9c5993fd48e to Valeria de Paiva
Jordan normal form:
https://www-sop.inria.fr/marelle/Guillaume.Cano/these.pdf
https://www-sop.inria.fr/marelle/Guillaume.Cano/
https://gopiandcode.uk/logs/log-certified-synthesis.html
https://github.com/coq/coq/wiki/CoqTerminationDiscussion
https://www.reddit.com/r/programming/comments/1ap7kq7/coq_theorem_prover_will_be_renamed_into_rocq/
https://iris-project.org/
# Local Variables:
# coding: utf-8-unix
# End: