Library syntax

Syntactic elements

A module defining the natural-deduction-style typing system for shift and reset, and a version thereof stratified into a normal-form level and a neutral-form level.
Require Export List.
Require Export Bool.


Parameter atoms : Set.

The syntax of formulas including a a distinguished atomic type Bot that reset can be set on
Inductive formula :=
| Func : formula -> formula -> formula
| Sum : formula -> formula -> formula
| Nat : formula
.

Definition context := list formula.
Hint Unfold context.

Church-style proof terms (typing system)
Inductive proof : context -> bool -> formula -> Set :=
| Inl : forall Gamma annot A B,
            proof Gamma annot A ->
            proof Gamma annot (Sum A B)
                  
| Inr : forall Gamma annot A B,
            proof Gamma annot B ->
            proof Gamma annot (Sum A B)

| Lam : forall Gamma annot A B,
            proof (A::Gamma) annot B ->
            proof Gamma annot (Func A B)

| Hyp : forall Gamma annot A,
            proof (A::Gamma) annot A

| Wkn : forall Gamma annot A B,
            proof Gamma annot A ->
            proof (B::Gamma) annot A

| Case : forall Gamma annot A B C,
            proof Gamma annot (Sum A B) ->
            proof (A::Gamma) annot C ->
            proof (B::Gamma) annot C ->
            proof Gamma annot C
                  
| App : forall Gamma annot A B,
            proof Gamma annot (Func A B) ->
            proof Gamma annot A ->
            proof Gamma annot B

| Reset : forall Gamma annot,
            proof Gamma true Nat ->
            proof Gamma annot Nat

| Shift : forall Gamma A,
            proof ((Func A Nat)::Gamma) true Nat ->
            proof Gamma true A

| Zero : forall Gamma annot,
            proof Gamma annot Nat

| Succ : forall Gamma annot,
            proof Gamma annot Nat ->
            proof Gamma annot Nat

| Rec : forall Gamma annot C,
            proof Gamma annot Nat ->
            proof Gamma annot C ->
            proof Gamma annot (Func Nat (Func C C)) ->
            proof Gamma annot C
.

The proof terms stratified into normal-form-terms (which cannot compute further) and neutral-terms (which could compute if the open variable(s) they countain would be substituted by a normal-non-neutral term)
Note that reset is only needed at the border of true/false annotations
Inductive proof_nf : context -> bool -> formula -> Set :=
| nf_Inl : forall Gamma annot A B,
               proof_nf Gamma annot A ->
               proof_nf Gamma annot (Sum A B)
                        
| nf_Inr : forall Gamma annot A B,
               proof_nf Gamma annot B ->
               proof_nf Gamma annot (Sum A B)
                        
| nf_Lam : forall Gamma annot A B,
               proof_nf (A::Gamma) annot B ->
               proof_nf Gamma annot (Func A B)
                        
| nf_ne : forall Gamma annot A,
               proof_ne Gamma annot A ->
               proof_nf Gamma annot A

| nf_Zero : forall Gamma annot,
               proof_nf Gamma annot Nat
                        
| nf_Succ : forall Gamma annot,
               proof_nf Gamma annot Nat ->
               proof_nf Gamma annot Nat

with proof_ne : context -> bool -> formula -> Set :=
| ne_Hyp : forall Gamma annot A,
               proof_ne (A::Gamma) annot A

| ne_Case : forall Gamma annot A B C,
               proof_ne Gamma annot (Sum A B) ->
               proof_nf (A::Gamma) annot C ->
               proof_nf (B::Gamma) annot C ->
               proof_ne Gamma annot C

| ne_App : forall Gamma annot A B,
               proof_ne Gamma annot (Func A B) ->
               proof_nf Gamma annot A ->
               proof_ne Gamma annot B


| ne_Wkn : forall Gamma annot A B,
               proof_nf Gamma annot A ->
               proof_ne (B::Gamma) annot A

| ne_Reset : forall Gamma,
               proof_ne Gamma true Nat ->
               proof_ne Gamma false Nat
                                               
| ne_Shift : forall Gamma A,
               proof_ne ((Func A Nat)::Gamma) true Nat ->
               proof_ne Gamma true A

| ne_Rec : forall Gamma annot C,
               proof_ne Gamma annot Nat ->
               proof_nf Gamma annot C ->
               proof_nf Gamma annot (Func Nat (Func C C)) ->
               proof_ne Gamma annot C
.

leb is the less-than-or-equal order on booleans
Lemma leb_refl : forall a, leb a a.

Lemma leb_trans : forall a b c, leb a b -> leb b c -> leb a c.

prefix is the prefix relation on two lists
Inductive prefix : context -> context -> Set :=
  prefix_refl w : prefix w w
| prefix_cons w w' : forall A, prefix w w' -> prefix w (A::w').

Lemma prefix_trans : forall w w' w'', prefix w w' -> prefix w' w'' -> prefix w w''.

Monotonicity of proof_nf and proof_ne with respect to the order on contexts and the order on booleans

Lemma proof_ne_mon : (forall Gamma Gamma', prefix Gamma Gamma' -> forall A annot, proof_ne Gamma annot A -> proof_ne Gamma' annot A).

Lemma proof_nf_mon : forall Gamma Gamma', prefix Gamma Gamma' -> forall A annot, proof_nf Gamma annot A -> proof_nf Gamma' annot A.

Lemma proof_nf_mon2 : (forall A Gamma annot, proof_nf Gamma annot A -> forall annot', leb annot annot' -> proof_nf Gamma annot' A)
with proof_ne_mon2 : (forall A Gamma annot, proof_ne Gamma annot A -> forall annot', leb annot annot' -> proof_ne Gamma annot' A).

forget_nf forgets the structure NF/NE

Theorem forget_nf (Gamma:context)(annot:bool)(A:formula)(r:proof_nf Gamma annot A) : proof Gamma annot A
with forget_ne (Gamma:context)(annot:bool)(A:formula)(e:proof_ne Gamma annot A) : proof Gamma annot A.

For testing purposes we define bare terms
Inductive bare : Set :=
| I1 : bare -> bare
| I2 : bare -> bare
| L : bare -> bare
| H : bare
| W : bare -> bare
| C : bare -> bare -> bare -> bare
| A : bare -> bare -> bare
| RESET : bare -> bare
| SHIFT : bare -> bare
| O : bare
| Sc : bare -> bare
| Rc : bare -> bare -> bare -> bare
.

forget_proof produces a bare structure of a proof term
Theorem forget_proof (Gamma:context)(annot:bool)(A:formula)(r:proof Gamma annot A) : bare.


This page has been generated by coqdoc