[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[SETFAVICON IMAGES/forthsun.png]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2009workshop"))
;;    http://angg.twu.net/2009workshop.html
;; file:///home/edrx/TH/L/2009workshop.html
#]
[lua: LR = R ]
[htmlize [J 2009oct23: Workshop about Proof Assistants]

[_TARGETS
  eev       -> (find-TH "emacs" "short-emacs-tutorial")
  emacs-eev -> (find-eevfile "debian/README.Debian")

]


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

[P Well, no. Let me restart.]

[P 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.]

[P 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...]

[BE'
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
]

[BE'
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
]

[BE'
Thanks to:
  FNaufel
  Vinícius
  Oberdan
  Welton
  Gustavo
  Rodrigo/Roberto
]

[BE'
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
]

[BE'
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.
]

[BE'
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.
]

[BE'
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
]

[BE'
Missing:
an http-able repo
  --print-uris
python-apt
  -> uris
]







]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]