Rechnergestütztes Beweisen (Hofmann, WS 2005/06) 2006-01-26 VL 26 (Entwurf) Injektivität und Disjunktivität =============================== Axiome der Arithmetik: Injektivität. S n = S m => n = m Disjunktiviät (Unterscheidung). 0 <> S m Diese Gesetze gelten für alle induktiven Typen in Coq: 1. Sind zwei Bewohner eines induktiven Typs gleich, haben sie gleiche Konstruktoren und Unterterme. 2. Terme mit unterschiedlichem äußersten Konstruktor sind verschieden. Vgl: Kongruenzaxiom in Gleichungstheorie. In Coq werden diese Gesetze mit den Taktiken "injection" und "discriminate" verwendet. Induktive Familien ================== Vektoren -------- Gamma |- A : Set vector-I1 -------------------------- Gamma |- Vnil : vector A 0 Gamma |- n : nat Gamma |- a : A Gamma |- as : vector A n vector-I2 ----------------------------------------- Gamma |- Vcons a as : vector A (S n) Der Typ vector : Set -> nat -> Set hat zwei Parameter: Einen unveränderlichen, A:Set, und einen veränderlichen n:nat. Der unveränderliche wird wie bei Listen als "genereller Parameter" implementiert. Damit ist vector A : nat -> Set eine induktiv definierte Typ-wertige Funktion, oder induktive Familie. In Coq: Require Import Bvector. Inductive vector (A:Set) : nat -> Set := | Vnil : vector A 0 | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n). Induktiv definierte Propositionen und Prädikate =============================================== Kleiner-gleich auf natürlichen Zahlen. Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, le n m -> le n (S m). Infix "<=" := le : nat_scope. Die logischen Konnektive können selbst induktiv definiert werden (ausser Implikation und universelle Quantifikation). Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope. Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope. Inductive True : Prop := I : True. Inductive False : Prop :=. Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. Rekursion, Termination, und logische Konsistenz =============================================== In Haskell ist jeder Typ bewohnt: 1. Möglichkeit: Rekursion: a :: A a = a 2. Möglichkeit: Exception: a :: A a = error "undefined" Wären diese Definitionen in Coq akzeptierbar, so wäre vermöge des Curry-Howard-Isomorphismus jede Proposition bewohnt, d.h., hätte einen Beweis. Coq wäre als Beweissystem inkonsistent. Konsequenzen: - es gibt keine Exceptions "error", damit auch keine partiellen Funktionen - jeder Ausdruck muss terminieren Insbesondere ist Rekursion in Coq nur eingeschränkt verfügbar. 1. Mit vordefinierten Rekursionskombinatoren, die zu induktiven Definitionen erzeugt werden: nat_rec : forall P : nat -> Set, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n 2. In Form von struktureller Rekursion, z.B. Fixpoint add (n m : nat) {struct n } : nat := match n with | O => m | (S n') => S (add n' m) end Diese Def. ist akzeptierbar, da das erste Argument sich bei jedem rekursiven Aufruf verkleinert. Nicht jede Funktion ist direkt strukturell rekursiv, z.B., Division. Die folgende Funktion div x y berechnet x/(y+1), aufgerundet. div 0 y = 0 div (S x) y = S (div (x-y) y) Positivität =========== Negative ind. Def. erzeugen auch Nicht-Termination: Z.B. Repräsentation des ungetypten Lambda-Kalküls: Inductive D : Set := | abs : (D -> D) -> D. Definition app (t t': D) : D := match t with | abs f => f t' end. Nun ist der nicht-terminierende Term (\x. x x) (\x. x x) definierbar durch: app (abs (fn x => app x x)) (abs (fn x => app x x)) Gleichheit in der Typentheorie (BHK-Interpretation) =================================================== Für jedes A:Set, a1,a2:A brauchen wir einen Typ eq_A a1 a2 : Prop, der die Beweise, dass a1 = a2 ist, enthält. (Subskript _A an eq wird meist weggelassen.) Zwei Antworten: a) Leibniz-Gleichheit. eq_A a1 a2 := forall P:A->Prop, P a1 -> P a2. Variable A:Set. Definition refl_equal: forall a:A, eq a a := fun a:A => fun P:A->Prop => fun H:P a => H. Definition sym_equal: forall a1 a2:A, eq a1 a2 -> eq a2 a1 := fun a1 a2:A => fun p:eq a1 a2 => p (fun x:A => eq x a1) (refl_equal a1). Definition trans_equal: ... Leibniz-Gleichheit ist unbrauchbar bei abhängigen Datentypen wie z.B. Vec (= vector). Wenn z.B. x : nat, y : nat, p : eq x y a : Vec x Dann gibt es keine Möglichkeit, ein Element a' : Vec y zu konstruieren. Begründung: Vec : nat -> Set, nicht nat -> Prop. (Wenn eq a1 a2 als forall P:A->Set. P a1 -> P a2 definiert wäre, wäre p Vec a : Vec y möglich.) Zweiter Kritikpunkt (von Martin-Löf vorgetragen): eq ist impredikativ. b) Induktive Definition der Gleichheit nach Martin-Löf. Inductive eq (A:Set) : A -> A -> Prop := refl_equal : forall a:A, eq a a. Daraus folgendes Induktionsprinzip: C : forall a1 a2:A, eq a1 a2 -> Type H : forall a:A. C a a (refl_equal a) ----------------------------------------------------------- eq_elim C H : forall a1 a2:A, forall p: eq a1 a2, C a1 a2 p Informelle Erklärung: "Type" ist entweder Set oder Prop. Intuition zur Symmetrie: sym_equal a a (refl_equal a) = refl_equal a Definition sym_equal: forall a1 a2:A, eq a1 a2 -> eq a2 a1 := eq_elim (fun a1 a2:A => fun p: eq a1 a2 => eq a2 a1) (fun a:A => fun p: eq a a. p) Klausur 08.02.2006 12.00 Uhr Besprechung 09.02.2006 14.00 Uhr Übung 09.02.2006 10.00 Uhr fällt aus (bzw. Dulma holt nach) Stoff: Skript bis Sonntag 29.01. 23:59 "closed book" (ohne Material), dafür einfacher, orientiert sich an theoretischen Übungsaufgaben.