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

2006-01-19 VL 24

Weiter mit konstruktiver Logik und Coq:

BHK-Interpretation (Propositions-as-type) für Prädikatenlogik
=============================================================

Prädikate sind Aussageformen, d.h. Funktionen, die Individuen auf
Propositionen abbilden, z.B.

  even : N -> "Propositions"

Unter der BHK-Interpretation ordnet also ein Prädikat jedem Individuum
einen Typ zu.  Typ-wertige Funktionen heissen abhänginge Typen.

Bsp: Vec(n)  = Vektoren der Länge n
     upto(n) = [0..n-1]

Prop und Set
------------

In Coq wird das Universum derjenigen Typen, die Propositionen
entsprechen, mit Prop bezeichnet, und das Univ. der Typen, die
Individuen enthalten, mit Set bezeichnet. 

Sei  D : Set
     P : D -> Prop

Was ist ein Beweis für "Für alle d:D gilt P(d)"?  Eine Funktion
(Algorithmus, Verfahren), die jedem d aus D ein Element aus (einen
Beweis für) P(d) zuordnet, also eine "abhängige" Funktion.

[Abhängige Funktionen gibt es auch in PVS.]  Der Raum dieser
abhängigen Funktionen wird mit 

  Pi d:D. P(d)

bezeichnet.  Also wenn f : Pi d:D.P(d), dann gilt f(d):P(d) für alle
d:D.  Pi d:D.P(d) ist also der Typ der Beweise von FORALL (d:D):P(d).

Bsp: init : R -> Pi n:N. Vec(n)
     init 0.7 3 = (0.7, 0,7, 0,7)

In Coq: Pi d:D.P(d)  wird geschrieben als  "forall (d:D), P(d)"

Beispiel:

Section test.
Variable D:Set.
Variable P:D -> Prop.


Theorem inst: forall x:D, (forall y:D, P y) -> P x.
intros x H.
apply (H x).
Qed.
Print inst.


Was ist ein Beweis für EXISTS d:D. P(d)?  Antwort: So ein Beweis
beinhaltet ein Element (d:D), den Zeugen, und einen Beweis von P(d).

In der Typentheorie von Martin-Löf gibt es den Typen SIGMA x:D. P(x),
dessen Elemente Paare (d,p) mit d:D und p:P(d) sind.  Für SIGMA
x:D.P(x) gibt es sogar Projektionen

  pr1 : SIGMA x:D. P(x) -> D
  pr2 : PI p:(SIGMA x:D. P(x)). P (pr1 p)

Reduktionsregeln (definitionale Gleichheiten):

  pr1 (d,p) = d  (i)
  pr2 (d,p) = p  (ii)

(ii) ist in folgendem Sinne interessant.  Die Typen beider Seiten der
Gleichung (ii) sind:

  LHS: p : P(d)
  RHS: pr2(d,p) : P(pr1(d,p)) = P(d)  (wegen (i))

Man braucht also (i) um die Wohlgetyptheit von (ii) zu zeigen.

Bsp: Auswahlaxiom

(forall x:D, exists y:D, R x y) -> (exists f:D->D, forall x:D, R x (f x))

Beweis hat Typ

  (Pi x:D, Sigma y:D, R x y) -> (Sigma f:D->D, Pi x:D, R x (f x))

und ist

  fun H => (fun x => pr1 (H x), 
            fun x => pr2 (H x))

Eine weitere definitionale Gleichheit:

  (fun (x:A) => e) e' = e[e'/x]   (beta-Gleichheit)

Schliesslich: Hat man definiert

  f := e

Dann ist f = e. Definitionen werden automatisch expandiert.

In Coq: Falls P: D -> Prop, dann ist

  forall x:D, P x : Prop

egal was D ist.

Girard's Paradox: Anzunehmen, dass Sigma x:D.P(x) : Prop, egal was
D ist, ist inkonsistent.  Daraus ergibt sich folgende Bedingung von
EXISTS.  Man definiert:

  ex : forall (D:Set), (D -> Prop) -> Prop

wie folgt.

  ex D P = forall C:Prop, (forall x:D, P(x) -> C) -> C

Falls d:D und p:P(d) vorliegen, dann finden wir

  ex_intro d p : ex D P
               := fun (C:Prop) => fun (H:forall x:D, P(x) -> C) => H d p

Ebenso finden wir

  ex_elim : (forall x:D, P(x) -> C) -> ((ex D P) -> C)
          := fun (H  : forall x:D, P(x) -> C) => 
             fun (H1 : ex D P) -> H1 C H

Man umgeht mit dieser Eliminationsregel eine echte erste Projektion (pr1).