Quick
index
main
eev
maths
blogme
dednat4
littlelangs
PURO
emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
debian-rj
w32/AIX
politics
personal
heroes
irc
contact
☿

2009oct23: Workshop about Proof Assistants

In 2009oct23 I gave a workshop about proof assistants at the PURO.

Well, no. Let me restart.

I volunteered to give a workshop at the "Semana Acadêmica" about proof assistants. My plan was megalomaniac to say the least: I would install Emacs, eev and Coq at the machines of the computer lab, and I would prepare a file with e-scripted examples for Coq, and I would teach the students how to start emacs-eev, how to run the demos with eepitch, and I would explain to them proofs-as-types, BHK, Curry-Howard, sequents, goals, and tactics.

The day of the workshop came and didn't even have all the scripts to install all the packages in the machines of the lab... They couldn't be fetched from the outside each time, because our bandwidth with the outside world during the day is usually around 2KB/s. To make things even harder, I run Debian Lenny at my machines, and they use Ubuntu Jaunty at the lab...

cpne
  copies $1 to $2, but only if $2 does not exist
sources.list
dmissingu
ubuntu pkg search

openssh-server
install-sshd-sudo.sh

apt-ftparchive
U-and-HU

Introductory comments:
  (find-angg ".emacs.papers" "automath")
    Hard problem
    Hard language
  (find-angg ".emacs.papers" "yanofsky")
    Turing's Halting Problem
    Gödel's First Incompleteness Theorem
      (What really matters to us there is that proofs are numbers)
  Searching for proofs
  Checking proofs

Thanks to:
  FNaufel
  Vinícius
  Oberdan
  Welton
  Gustavo
  Rodrigo/Roberto

lc0216
  apt-get install
/var/cache/apt/archives/
 \-> /home/edrx/ubuntu-puro/debs/      debs
     \-> apt-ftparchive -> /dists/     dists
            |                            ^
            v                            |
/home/edrx/debs.tgz   ---> thttpd ---> debs.tgz
  /tmp/pen/debs.tgz

Emacs:
  It may be possible to teach people how to run the examples
    in Emacs by only teaching them F8 and a few related keys,
    and by having a script like:
      (find-eevfile "debian/emacs-eev")
    called `emacs-eev-coq', that starts up with the examples
    page.
  TODO: fix this (remove the "oficina" stuff), reduce 99 to 90,
      (find-eevfile "debian/")
      (find-eevfile "debian/99eev.el")
    create an `emacs-eev-coq' package.

The Debian side
The eev side
The mathematical side:
  (find-anggfile "IMAGES/and_commutes_shrink4.png")
  (find-anggfile "IMAGES/and_commutes_shrink6.png")
  (find-anggfile "IMAGES/imp_trans_shrink4.png")
  (find-anggfile "IMAGES/imp_trans_shrink6.png")
The Coq side:
  (find-es "coq" "intro-apply-assumption-0")

* (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.

Diagrams:
  Reductions for f(g(10))
  when g = \x:R.x+x
       f = \y:R.2x+3

The goal-based proof for imp_trans
  (add the `:='s)

The colored logs for the proofs in Coq

Missing:
  The goal-based proof for P&Q->Q&P
  splitting in the context
  cut & lemma

Missing:
an http-able repo
  --print-uris
python-apt
  -> uris