Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-11-17 VL 10

Übungen in PVS: Monoide:

* 1 ist invertierbar
* x,y sind invertierbar => x*y ist invertierbar

Daraus folgt, dass die invertierbaren Elements eines Monoids eine
Gruppe bilden.

(auto-rewrite "Invertible")
(case "x * y * (y_inv * x_inv) = x * (y * y_inv) * x_inv")
  [Schnittregel]
(replace -1 1)
(grind)


Rekursive Funktionen in PVS:

In PVS gibt es Funktionsdefinitionen, z.B.:

  plusfuenf(x:nat):nat = x + 5

  Invertible(x:M):boolean = EXISTS(y:M):...

Rekursive Definitionen sind auch erlaubt, aber sie müssen
terminieren.  Problematisch sind nicht-terminierende Funktionen wie
z.B.

  f(x) = f(x)+1

Dann kann man zeigen 0=1:
  0 = f(0) - f(0) = f(0) + 1 - f(0) = 1

In PVS sind alle Funktionen total, alle Terme haben einen
wohldefinierten Wert.  Deshalb muss bei jeder rekursiven Definition
eine Abstiegsfunktion angegeben werden.  

Satz:  Seien A, B!=0 Mengen und F:[[A->B],A->B].  Sei ausserdem
m:[A->N], so dass für alle a in A und f1,f2:[A->B]

 wenn f1(x)=f2(x) für alle x in A mit m(x)<m(a),
 dann F(f1)(a) = F(f2)(a).

Dann existiert genau eine Funktion f:[A->B] mit F(f)=f.

Beweis: f(a) = F^(m(a))(\lambda x. b0)(a) für ein beliebiges b0.
Zeige F(f)(a)=f(a) durch Induktion über m(a).

  a : [nat->real]

  sum(n:nat) : RECURSIVE nat =
    IF n=0 THEN a(0) ELSE a(n) + sum(n-1) ENDIF
    MEASURE n
  % oder MEASURE 2*n  MEASURE n*n  ...

  sum(b:[nat->real],n:nat) : RECURSIVE nat =
    IF n=0 THEN b(0) ELSE b(n) + sum(b,n-1) ENDIF
    MEASURE n

  id(x:nat) = x

  gauss : PROPOSITION
    FORALL(n:nat): sum(id,n)=n*(n+1)/2

  gauss1 : PROPOSITION sum(id,3)=6

TCCs ("type checking conditions") sind Formeln, die sich aus der
Typüberprüfung ergeben.  Sie müssen auch separat bewiesen werden,
allerdings oft voll-automatisch.

Bsp:

  IF FORALL(n:nat): EXISTS(p,q:nat): prime(p) AND prime(q) AND p+q = n+4
     THEN 1 ELSE 0.5 
  ENDIF : nat

M-x show-tccs

M-x tcp 
  "type check proof"  Versuche alle tccs zu automatisch zu beweisen.

Insbesondere führen rekursive Definitionen zu TCCs, die aussagen, dass
die Abstiegsfunktion tatsächlich eine ist.

(expand "sum")

prelude.pvs enthält Definitionen, Axiome und Lemmas die automatisch
geladen werden.


(lemma "nat_induction")

(expand "sum" :if-simplifies T)

(inst -1 "LAMBDA(n:nat):sum(id,n)=n*(n+1)/2")

(induct "n")

(induct-and-simplify "n")