Rechnergestütztes Beweisen (Hofmann, WS 2005/06) 2006-01-25 VL 25 (Entwurf) Erweiterung des Kalküls für natürliches Schliessen ================================================== Universelle Quantifikation und Pi-Typ ------------------------------------- Gamma, x:A |- t : B forall-I ------------------------------- Gamma |- \x:A.t : forall(x:A),B Gamma |- r : forall(x:A),B Gamma |- s : A forall-E ------------------------------------------- Gamma |- r s : B(x:=s) Herleitungsreduktion (Beweisreduktion) wie bei Implikation. (beta) (\x:A.t) s --> t(x:=s) Existentielle Quantifikation und Sigma-Typ ------------------------------------------ Gamma |- s : A Gamma |- t : B(x:=s) exists-I ------------------------------------ Gamma |- (s,t) : exists(x:A),B Gamma |- r : exists(x:A),B Gamma, x:A, y:B |- t : C exists-E ----------------------------------------------------- Gamma |- ex_elim (\x:A.\y:B.t) r : C Reduktion. (iota) ex_elim (\x:A.\y:B.t) (r,s) --> t(x:=r,y:=s) Natürliche Zahlen ----------------- Gamma |- n : nat nat-I0 ---------------- nat-IS ------------------ Gamma |- O : nat Gamma |- S n : nat Gamma |- n : nat Gamma |- P : nat -> Prop Gamma |- tO : P O Gamma, n' : nat, ih : P n' |- tS : P (S n') nat-E ---------------------------------------------------- Gamma |- nat_ind P tO (\n':nat.\ih:P(n').tS) n : P n Schreibweise. 0 = O, 1 = S O, 2 = S (S O), ... Reduktion. (iota) nat_ind P t0 tS 0 --> t0 nat_ind P t0 tS (S n) --> tS n (nat_ind P t0 tS n) Listen ------ Gamma |- A : Set list-Inil --------------------- Gamma |- nil : list A Gamma |- a : A Gamma |- as : list A list-Icons ------------------------------------- Gamma |- cons a as : list A Gamma |- l : list A Gamma |- P : list A -> Prop Gamma |- tn : P nil Gamma, a:A, as:list A, ih:P as |- tc : P (cons a as) list-E ---------------------------------------------------- Gamma |- list_ind A P tn (\a\as\ih.tc) l : P l Schreibweise. a :: as = cons a as Reduktion. (iota) list_ind A P tn tc nil --> tn list_ind A P tn tc (cons a as) --> tc a as (list_ind A P tn tc as) Schema: Induktive Typen in Coq ------------------------------ Natürliche Zahlen: Inductive nat : Set := | O : nat | S : nat -> nat. O, S heissen Konstruktoren. Coq erzeugt Induktionsaxiom: nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n Listen: Require Import List. Inductive list (A : Set) : Set := | nil : list A | cons : A -> list A -> list A. Listen haben einen generellen Parameter, A:Set. Dieser wird in den definierten Konstrukten abstrahiert: list : forall (A:Set), Set (= Set -> Set) nil : forall (A:Set), list A cons : forall (A:Set), A -> list A -> list A In Coq ist das Typargument A zu nil und cons implizit. Check nil. Error: Cannot infer an instance for the implicit parameter A of nil Check (nil (A:=A)). nil : list A Induktionsschema: list_ind : forall (A : Set) (P : list A -> Prop), P nil -> (forall (a : A) (l : list A), P l -> P (a :: l)) -> forall l : list A, P l