(* 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
 *)