http://d.hatena.ne.jp/ehito/20111119/1321692292 のPVS版です． lem00:lemma FORALL (p: pred [nat]): (FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)) IMPLIES (FORALL (n: nat): p(n)) %|- lem00 : PROOF %|- (then (skeep*) (c…

http://d.hatena.ne.jp/ehito/20130816/1376622603 の続編です． 前回は n≦n*n を sub goal としましたが，今回は結論に含め，帰納法の仮定を強くしました． g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n * (&n - &1) …

http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext

http://logitext.mit.edu/logitext.fcgi/main https://github.com/ezyang/logitext/blob/master/doc/report.pdf

以前にも書いた排中律ネタですが，今回は連言から存在量化を纏める形のものです． g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;; e( REPEAT STRIP_TAC );; e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );; e…