####### # # 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 # or at . # See also , # , # , # , # and . # ####### (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") # (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")  (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 "") 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 # Local Variables: # coding: raw-text-unix # ee-delimiter-hash: "\n#\n" # ee-delimiter-percent: "\n%\n" # ee-anchor-format: "«%s»" # End: