Playing around with modeling logic in Coq

logic.v

Set Implicit Arguments.

Require Import List.

Inductive Vec A : nat -> Type :=
| nilV  : Vec A O
| consV : forall n, A -> Vec A n -> Vec A (S n).

Inductive T : nat -> Type :=
| Var    : T 1
| Lift   : forall n, T n -> T (S n).

Inductive P : nat -> Type :=
| And    : forall n, P n -> P n -> P n
| Or     : forall n, P n -> P n -> P n
| ForAll : forall n, P (S n) -> P n
| Exists : forall n, P (S n) -> P n
| Equal  : forall n, T n -> T n -> P n.

Definition interpT : forall n, Vec nat n -> T n -> nat.
 intros.
 generalize H ; clear H.
 induction H0 ; intros.

 (* Var *)
 remember 1 as m in H ; destruct H.
 discriminate Heqm.
 exact n0.

 (* Lift *)
 remember (S n) as m in H ; destruct H.
 discriminate Heqm.
 apply eq_add_S in Heqm.
 rewrite Heqm in H.
 exact (IHT H).
Defined.

Definition interp : forall n, Vec nat n -> P n -> Prop.
 intros.
 generalize H ; clear H.
 induction H0 ; intros.
 
 (* And *)
 exact (IHP1 H /\ IHP2 H).
 
 (* Or *)
 exact (IHP1 H \/ IHP2 H).

 (* ForAll *)
 exact (forall x:nat, IHP (consV x H)).

 (* Exists *)
 exact (exists x:nat, IHP (consV x H)).

 (* Equal *)
 exact (interpT H t = interpT H t0).
Defined.


Inductive Proof : forall n, list (P n) -> P n -> Type :=
| AndP : forall n l (p q : P n), Proof l p -> Proof l q -> Proof l (And p q)
| OrPL : forall n l (p q : P n), Proof l p -> Proof l (Or p q)
| OrPR : forall n l (p q : P n), Proof l q -> Proof l (Or p q).

Theorem soundness : forall n (p : P n) v, Proof nil p -> interp v p.
 intros.
 induction H.

 (* AndP *)
 simpl.
 split.
 exact (IHProof1 v).
 exact (IHProof2 v).

 (* OrPL *)
 simpl ; left.
 exact (IHProof v).

 (* OrPR *)
 simpl ; right.
 exact (IHProof v).
Qed.