(* An illustration of a "deep embedding" of propositional logic in CiC by Valery Trifonov *) Implicit Arguments On. (* the type of propositions is the sort Prop, the implication is the arrow type constructor (->) *) Definition o : Type := Prop. Definition imp : o -> o -> o := [A,B : o] (A -> B). (* [X : T] M is syntax for lambda X : T. M *) Infix RIGHTA 9 "=>" imp. (* so that A => B stands for (imp A B) *) Definition conj : o -> o -> o := [A,B : o] (C : o) ((A -> B -> C) -> C). (* (X : T) M is Pi X : T. M *) Infix 5 "^" conj. (* the Hilbert calculus (with conjunction) *) Inductive hil : o -> Prop := MP : (A,B : o) (hil (A => B)) -> (hil A) -> (hil B) | S : (A,B,C : o) (hil ((A => B => C) => (A => B) => (A => C))) | K : (A,B : o) (hil (A => B => A)) | P : (A,B : o) (hil (A => B => (A ^ B))) | Q : (A,B,C : o) (hil ((A => B => C) => (A ^ B) => C)). (* shorthands for use in those cases when Coq can infer the arguments *) Syntactic Definition S_ := (S ? ? ?). Syntactic Definition K_ := (K ? ?). Syntactic Definition P_ := (P ? ?). Syntactic Definition Q_ := (Q ? ? ?). (* examples (from Carsten's Twelf code) *) Definition p1 := [A,B,C] (MP (MP K_ (S A B C)) (S A B C)). (* Coq infers the types of A, B, C, and the arguments of K *) Check p1. (* show the inferred type of p1 *) Definition p2 := [A] (MP (MP S_ K_) (K A A)). Check p2. Definition I := p2. Definition p3 := [A] (MP (p2 ?) (p2 A)). (* Coq infers the argument ? *) Check p3. Definition p4 := [A,B,C] (MP (p2 ?) (p1 A B C)). Check p4. Definition first := [A,B] (MP Q_ (K A B)). Check first. Definition second := [A,B] (MP Q_ (MP (K ? A) (I B))). Check second. (* natural deduction *) Definition nd : o -> Prop := [A : o] A. Definition impE : (A,B : o) (nd (A => B)) -> (nd A) -> (nd B) := [A,B,D1,D2] (D1 D2). Definition impI : (A,B : o) ((nd A) -> (nd B)) -> (nd (A => B)) (* notice "negative occurrence" of nd in the type *) := [A,B,f,x] (f x). Definition andEL : (A,B : o) (nd (A^B)) -> (nd A) := [A,B,D] (D ? ([x,y] x)). Definition andER : (A,B : o) (nd (A^B)) -> (nd B) := [A,B,D] (D ? ([x,y] y)). Definition andI : (A,B : o) (nd A) -> (nd B) -> (nd (A^B)) := [A,B,D1,D2] [C; c : (A=>B=>C)] (c D1 D2). (* example *) Definition examplebb := [A,B : o] (impI [u : (nd A)] (impI [v : (nd B)] u)). Check examplebb. (* conversion of derivations in the Hilbert calculus to natural deduction (the converse is left for the reader :-) *) Fixpoint hil2nd [A; D : (hil A)] : (nd A) := (* using dependently-typed inductive elimination: *) <[A;_] (nd A)> Cases D of (MP _ _ D1 D2) => (impE (hil2nd D1) (hil2nd D2)) | (S _ _ _) => (impI [x] (impI [y] (impI [z] (impE (impE x z) (impE y z))))) | (K _ _) => (impI [x] (impI [_] x)) | (P _ _) => (impI [x] (impI [y] (andI x y))) | (Q _ _ _) => (impI [c] (impI [p] (impE (impE c (andEL p)) (andER p)))) end. Check hil2nd. (* show the type of the conversion function *) (* "Hilbert" with a single hypothesis: write (hilh H A) for H |- A *) Inductive hilh : o -> o -> Prop := Axh : (A : o) (hilh A A) | MPh : (H,A,B : o) (hilh H (A => B)) -> (hilh H A) -> (hilh H B) | Sh : (H,A,B,C : o) (hilh H ((A => B => C) => (A => B) => (A => C))) | Kh : (H,A,B : o) (hilh H (A => B => A)). (* "bracket abstraction" (one level only); notice it's a function from derivations in the system with a hypothesis to derivations in the original system *) Fixpoint bah [H,A; D : (hilh H A)] : (hil (H => A)) := <[H,A,D] (hil (H => A))> Cases D of (Axh A) => (MP (MP S_ K_) (K A A)) | (MPh _ _ _ D1 D2) => (MP (MP S_ (bah D1)) (bah D2)) | (Sh _ A B C) => (MP K_ (S A B C)) | (Kh _ A B) => (MP K_ (K A B)) end. Check bah. (* show the type of the bracket abstraction function *) (* notice that type correctness implies the function is total, i.e. defined (hence terminating) on all terms in its domain *)