- (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
- { al_eqv : @ND_Relation Judg Rule
- where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
-
- (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
- * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
- * to generate the rest *)
- ; al_reflexive_seq : forall t, Rule [] [t|=t]
-
- (* these can all be absorbed into a separate "sequent calculus" presentation *)
- ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d]
- ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d]
- ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b]
- ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b]
- ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b]
- ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b]
- ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))]
- ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)]
- ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ]
- ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ]
- ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ]
- ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ]
-
- ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
- ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
-
- (* these are essentially one way of formalizing
- * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
- ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#]
- ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
- ; al_horiz_expand_right_then_cancel : forall a,
- ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
-
- ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ]
- ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ]
- ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ]
- ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x]
- ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
- f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g
- ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
- f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g
- ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
- f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g
- ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
- f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g
- ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left x (nd_id [a|=b]) === nd_id [x,,a|=b]
- ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right x (nd_id [a|=b]) === nd_id [a,,x|=b]
- ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left x (nd_id [a|=b]) === nd_id [a|=x,,b]
- ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right x (nd_id [a|=b]) === nd_id [a|=b,,x]
- ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
- (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
- ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
- (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
- ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
- (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
- ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
- (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
-
- ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
- ; al_subst_associativity : forall {a b c d},
- ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
- (al_subst a c d)
- ===
- nd_assoc ;;
- ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
- (al_subst a b d))
- ; al_subst_associativity' : forall {a b c d},
- nd_cossa ;;
- ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
- (al_subst a c d)
- ===
- ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
- (al_subst a b d))
-
- ; al_subst_left_identity : forall a b, (( [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell
- ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#] );; al_subst b _ _) === nd_cancelr
- ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
- [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
- === al_subst a b c;; [#al_horiz_expand_left d#]
- ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
- [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
- === al_subst a b c;; [#al_horiz_expand_right d#]
- ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
- (((nd_rlecnac;;
- ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
- (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
- (nd_id [t1 |= t0]) **
- ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
- (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));;
- al_subst t1 t0 t2)
- ===
- ((([#al_reflexive_seq (t1,, [])#];;
- (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
- al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));;
- (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
- }.
-
- Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
- Open Scope temporary_scope3.
-
- Lemma al_subst_respects {PL:ProgrammingLanguage} :
- forall {a b c},
- forall
- (f : [] /⋯⋯/ [a |= b])
- (f' : [] /⋯⋯/ [a |= b])
- (g : [] /⋯⋯/ [b |= c])
- (g' : [] /⋯⋯/ [b |= c]),
- (f === f') ->
- (g === g') ->
- (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
- intros.
- setoid_rewrite H.
- setoid_rewrite H0.
- reflexivity.
- Defined.
-
- (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
- Class ProgrammingLanguageWithUnrestrictedSubstructuralRules :=
- { alwusr_al :> ProgrammingLanguage
- ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b]
- ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c]
- ; al_weak : forall a b, Rule [[] |= b ] [ a |= b]
- }.
- Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
-
- (* languages with a fixpoint operator *)
- Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) :=
- { alwfpo_al := al
- ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b]