| nd_id1 : forall h, [ h ] /⋯⋯/ [ h ]
(* natural deduction: you may discard conclusions *)
- | nd_weak : forall h, [ h ] /⋯⋯/ [ ]
+ | nd_weak1 : forall h, [ h ] /⋯⋯/ [ ]
(* natural deduction: you may duplicate conclusions *)
| nd_copy : forall h, h /⋯⋯/ (h,,h)
+ (* natural deduction: you may re-order conclusions *)
+ | nd_exch : forall x y, (x,,y) /⋯⋯/ (y,,x)
+
(* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
| nd_prod : forall {h1 h2 c1 c2}
(pf1: h1 /⋯⋯/ c1 )
Open Scope nd_scope.
Open Scope pf_scope.
- (* a proof is "structural" iff it does not contain any invocations of nd_rule *)
+ (* a predicate on proofs *)
+ Definition NDPredicate := forall h c, h /⋯⋯/ c -> Prop.
+
+ (* the structural inference rules are those which do not change, add, remove, or re-order the judgments *)
Inductive Structural : forall {h c}, h /⋯⋯/ c -> Prop :=
| nd_structural_id0 : Structural nd_id0
| nd_structural_id1 : forall h, Structural (nd_id1 h)
- | nd_structural_weak : forall h, Structural (nd_weak h)
- | nd_structural_copy : forall h, Structural (nd_copy h)
- | nd_structural_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1**pf2)
- | nd_structural_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2), Structural pf1 -> Structural pf2 -> Structural (pf1;;pf2)
| nd_structural_cancell : forall {a}, Structural (@nd_cancell a)
| nd_structural_cancelr : forall {a}, Structural (@nd_cancelr a)
| nd_structural_llecnac : forall {a}, Structural (@nd_llecnac a)
| nd_structural_cossa : forall {a b c}, Structural (@nd_cossa a b c)
.
+ (* the closure of an NDPredicate under nd_comp and nd_prod *)
+ Inductive NDPredicateClosure (P:NDPredicate) : forall {h c}, h /⋯⋯/ c -> Prop :=
+ | ndpc_p : forall h c f, P h c f -> NDPredicateClosure P f
+ | ndpc_prod : forall `(pf1:h1/⋯⋯/c1)`(pf2:h2/⋯⋯/c2),
+ NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1**pf2)
+ | ndpc_comp : forall `(pf1:h1/⋯⋯/x) `(pf2: x/⋯⋯/c2),
+ NDPredicateClosure P pf1 -> NDPredicateClosure P pf2 -> NDPredicateClosure P (pf1;;pf2).
+
+ (* proofs built up from structural rules via comp and prod *)
+ Definition StructuralND {h}{c} f := @NDPredicateClosure (@Structural) h c f.
+
+ (* The Predicate (BuiltFrom f P h) asserts that "h" was built from a single occurrence of "f" and proofs which satisfy P *)
+ Inductive BuiltFrom {h'}{c'}(f:h'/⋯⋯/c')(P:NDPredicate) : forall {h c}, h/⋯⋯/c -> Prop :=
+ | builtfrom_refl : BuiltFrom f P f
+ | builtfrom_P : forall h c g, @P h c g -> BuiltFrom f P g
+ | builtfrom_prod1 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f1 ** f2)
+ | builtfrom_prod2 : forall h1 c1 f1 h2 c2 f2, P h1 c1 f1 -> @BuiltFrom _ _ f P h2 c2 f2 -> BuiltFrom f P (f2 ** f1)
+ | builtfrom_comp1 : forall h x c f1 f2, P h x f1 -> @BuiltFrom _ _ f P x c f2 -> BuiltFrom f P (f1 ;; f2)
+ | builtfrom_comp2 : forall h x c f1 f2, P x c f1 -> @BuiltFrom _ _ f P h x f2 -> BuiltFrom f P (f2 ;; f1).
+
(* multi-judgment generalization of nd_id0 and nd_id1; making nd_id0/nd_id1 primitive and deriving all other *)
Fixpoint nd_id (sl:Tree ??Judgment) : sl /⋯⋯/ sl :=
match sl with
| T_Branch a b => nd_prod (nd_id a) (nd_id b)
end.
- Fixpoint nd_weak' (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
+ Fixpoint nd_weak (sl:Tree ??Judgment) : sl /⋯⋯/ [] :=
match sl as SL return SL /⋯⋯/ [] with
| T_Leaf None => nd_id0
- | T_Leaf (Some x) => nd_weak x
- | T_Branch a b => nd_prod (nd_weak' a) (nd_weak' b) ;; nd_cancelr
+ | T_Leaf (Some x) => nd_weak1 x
+ | T_Branch a b => nd_prod (nd_weak a) (nd_weak b) ;; nd_cancelr
end.
Hint Constructors Structural.
- Lemma nd_id_structural : forall sl, Structural (nd_id sl).
+ Hint Constructors BuiltFrom.
+ Hint Constructors NDPredicateClosure.
+ Hint Unfold StructuralND.
+
+ Lemma nd_id_structural : forall sl, StructuralND (nd_id sl).
intros.
induction sl; simpl; auto.
destruct a; auto.
Defined.
- Lemma weak'_structural : forall a, Structural (nd_weak' a).
- intros.
- induction a.
- destruct a; auto.
- simpl.
- auto.
- simpl.
- auto.
- Qed.
-
(* An equivalence relation on proofs which is sensitive only to the logical content of the proof -- insensitive to
* structural variations *)
Class ND_Relation :=
(* the relation must respect composition, be associative wrt composition, and be left and right neutral wrt the identity proof *)
; ndr_comp_respects : forall {a b c}(f f':a/⋯⋯/b)(g g':b/⋯⋯/c), f === f' -> g === g' -> f;;g === f';;g'
; ndr_comp_associativity : forall `(f:a/⋯⋯/b)`(g:b/⋯⋯/c)`(h:c/⋯⋯/d), (f;;g);;h === f;;(g;;h)
- ; ndr_comp_left_identity : forall `(f:a/⋯⋯/c), nd_id _ ;; f === f
- ; ndr_comp_right_identity : forall `(f:a/⋯⋯/c), f ;; nd_id _ === f
(* the relation must respect products, be associative wrt products, and be left and right neutral wrt the identity proof *)
; ndr_prod_respects : forall {a b c d}(f f':a/⋯⋯/b)(g g':c/⋯⋯/d), f===f' -> g===g' -> f**g === f'**g'
; ndr_prod_associativity : forall `(f:a/⋯⋯/a')`(g:b/⋯⋯/b')`(h:c/⋯⋯/c'), (f**g)**h === nd_assoc ;; f**(g**h) ;; nd_cossa
- ; ndr_prod_left_identity : forall `(f:a/⋯⋯/b), (nd_id0 ** f ) === nd_cancell ;; f ;; nd_llecnac
- ; ndr_prod_right_identity : forall `(f:a/⋯⋯/b), (f ** nd_id0) === nd_cancelr ;; f ;; nd_rlecnac
(* products and composition must distribute over each other *)
; ndr_prod_preserves_comp : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
- (* products and duplication must distribute over each other *)
- ; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b
+ (* Given a proof f, any two proofs built from it using only structural rules are indistinguishable. Keep in mind that
+ * nd_weak and nd_copy aren't considered structural, so the hypotheses and conclusions of such proofs will be an identical
+ * list, differing only in the "parenthesization" and addition or removal of empty leaves. *)
+ ; ndr_builtfrom_structural : forall `(f:a/⋯⋯/b){a' b'}(g1 g2:a'/⋯⋯/b'),
+ BuiltFrom f (@StructuralND) g1 ->
+ BuiltFrom f (@StructuralND) g2 ->
+ g1 === g2
- ; ndr_comp_preserves_cancell : forall `(f:a/⋯⋯/b), nd_cancell;; f === nd_id _ ** f ;; nd_cancell
- ; ndr_comp_preserves_cancelr : forall `(f:a/⋯⋯/b), nd_cancelr;; f === f ** nd_id _ ;; nd_cancelr
- ; ndr_comp_preserves_assoc : forall `(f:a/⋯⋯/b)`(g:a1/⋯⋯/b1)`(h:a2/⋯⋯/b2),
- nd_assoc;; (f ** (g ** h)) === ((f ** g) ** h) ;; nd_assoc
+ (* proofs of nothing are not distinguished from each other *)
+ ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
- (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
- ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g
+ (* products and duplication must distribute over each other *)
+ ; ndr_prod_preserves_copy : forall `(f:a/⋯⋯/b), nd_copy a;; f**f === f ;; nd_copy b
- (* any two proofs of nothing are "equally good" *)
- ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
+ (* duplicating a hypothesis and discarding it is irrelevant *)
+ ; ndr_copy_then_weak_left : forall a, nd_copy a;; (nd_weak _ ** nd_id _) ;; nd_cancell === nd_id _
+ ; ndr_copy_then_weak_right : forall a, nd_copy a;; (nd_id _ ** nd_weak _) ;; nd_cancelr === nd_id _
}.
(*
apply k.
apply scnd_weak.
eapply scnd_branch; apply k.
+ inversion k; subst; auto.
inversion k; subst.
apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
apply IHnd2.
inversion bogus.
Defined.
- (* a "ClosedSIND" is a proof with no open hypotheses and no multi-conclusion rules *)
- Inductive ClosedSIND : Tree ??Judgment -> Type :=
- | cnd_weak : ClosedSIND []
- | cnd_rule : forall h c , ClosedSIND h -> Rule h c -> ClosedSIND c
- | cnd_branch : forall c1 c2, ClosedSIND c1 -> ClosedSIND c2 -> ClosedSIND (c1,,c2)
- .
-
- (* we can turn an SIND without hypotheses into a ClosedSIND *)
- Definition closedFromSIND h c (pn2:SIND h c)(cnd:ClosedSIND h) : ClosedSIND c.
- refine ((fix closedFromPnodes h c (pn2:SIND h c)(cnd:ClosedSIND h) {struct pn2} :=
- (match pn2 in SIND H C return H=h -> C=c -> _ with
- | scnd_weak c => let case_weak := tt in _
- | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _
- | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in
- let q1 := closedFromPnodes _ _ pn' in
- let q2 := closedFromPnodes _ _ pn'' in _
-
- end (refl_equal _) (refl_equal _))) h c pn2 cnd).
-
- destruct case_weak.
- intros; subst.
- apply cnd_weak.
+ (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
+ Section SequentND.
+ Context {S:Type}. (* type of sequent components *)
+ Context {sequent:S->S->Judgment}. (* pairing operation which forms a sequent from its halves *)
+ Notation "a |= b" := (sequent a b).
- destruct case_comp.
- intros.
- clear pn2.
- apply (cnd_rule ct).
- apply qq.
- subst.
- apply cnd0.
- apply rule.
-
- destruct case_branch.
- intros.
- apply cnd_branch.
- apply q1. subst. apply cnd0.
- apply q2. subst. apply cnd0.
- Defined.
+ (* a SequentND is a natural deduction whose judgments are sequents, has initial sequents, and has a cut rule *)
+ Class SequentND :=
+ { snd_initial : forall a, [ ] /⋯⋯/ [ a |= a ]
+ ; snd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
+ }.
- (* undo the above *)
- Fixpoint closedNDtoNormalND {c}(cnd:ClosedSIND c) : ND [] c :=
- match cnd in ClosedSIND C return ND [] C with
- | cnd_weak => nd_id0
- | cnd_rule h c cndh rhc => closedNDtoNormalND cndh ;; nd_rule rhc
- | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
- end.
+ Context (sequentND:SequentND).
+ Context (ndr:ND_Relation).
- (* Natural Deduction systems whose judgments happen to be pairs of the same type *)
- Section Sequents.
- Context {S:Type}. (* type of sequent components *)
- Context {sequent:S->S->Judgment}.
- Context {ndr:ND_Relation}.
+ (*
+ * A predicate singling out structural rules, initial sequents,
+ * and cut rules.
+ *
+ * Proofs using only structural rules cannot add or remove
+ * judgments - their hypothesis and conclusion judgment-trees will
+ * differ only in "parenthesization" and the presence/absence of
+ * empty leaves. This means that a proof involving only
+ * structural rules, cut, and initial sequents can ADD new
+ * non-empty judgment-leaves only via snd_initial, and can only
+ * REMOVE non-empty judgment-leaves only via snd_cut. Since the
+ * initial sequent is a left and right identity for cut, and cut
+ * is associative, any two proofs (with the same hypotheses and
+ * conclusions) using only structural rules, cut, and initial
+ * sequents are logically indistinguishable - their differences
+ * are logically insignificant.
+ *
+ * Note that it is important that nd_weak and nd_copy aren't
+ * considered to be "structural".
+ *)
+ Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | snd_inert_initial : forall a, SequentND_Inert _ _ (snd_initial a)
+ | snd_inert_cut : forall a b c, SequentND_Inert _ _ (snd_cut a b c)
+ | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
+ .
+
+ (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
+ * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
+ Class SequentND_Relation :=
+ { sndr_ndr := ndr
+ ; sndr_inert : forall a b (f g:a/⋯⋯/b),
+ NDPredicateClosure SequentND_Inert f ->
+ NDPredicateClosure SequentND_Inert g ->
+ ndr_eqv f g }.
+
+ End SequentND.
+
+ (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
+ Section ContextND.
+ Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
+ Context {snd:SequentND(sequent:=sequent)}.
Notation "a |= b" := (sequent a b).
- Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
- (* Sequent systems with initial sequents *)
- Class SequentCalculus :=
- { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
+ (* Note that these rules mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
+ Class ContextND :=
+ { cnd_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x ]
+ ; cnd_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x ]
+ ; cnd_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x ]
+ ; cnd_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x ]
+ ; cnd_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x ]
+ ; cnd_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x ]
+ ; cnd_expand_left : forall a b c , ND [ a |= b] [ c,,a |= c,,b]
+ ; cnd_expand_right : forall a b c , ND [ a |= b] [ a,,c |= b,,c]
+ ; cnd_snd := snd
}.
- (* Sequent systems with a cut rule *)
- Class CutRule (nd_cutrule_seq:SequentCalculus) :=
- { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
- ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell
- ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr
- ; nd_cut_associativity : forall {a b c d},
- (nd_id1 (a|=b) ** nd_cut b c d) ;; (nd_cut a b d) === nd_cossa ;; (nd_cut a b c ** nd_id1 (c|=d)) ;; nd_cut a c d
+ Context `(ContextND).
+
+ (*
+ * A predicate singling out initial sequents, cuts, context expansion,
+ * and structural rules.
+ *
+ * Any two proofs (with the same hypotheses and conclusions) whose
+ * non-structural rules do nothing other than expand contexts,
+ * re-arrange contexts, or introduce additional initial-sequent
+ * conclusions are indistinguishable. One important consequence
+ * is that asking for a small initial sequent and then expanding
+ * it using cnd_expand_{right,left} is no different from simply
+ * asking for the larger initial sequent in the first place.
+ *
+ *)
+ Inductive ContextND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | cnd_inert_initial : forall a, ContextND_Inert _ _ (snd_initial a)
+ | cnd_inert_cut : forall a b c, ContextND_Inert _ _ (snd_cut a b c)
+ | cnd_inert_structural : forall a b f, Structural f -> ContextND_Inert a b f
+ | cnd_inert_cnd_ant_assoc : forall x a b c, ContextND_Inert _ _ (cnd_ant_assoc x a b c)
+ | cnd_inert_cnd_ant_cossa : forall x a b c, ContextND_Inert _ _ (cnd_ant_cossa x a b c)
+ | cnd_inert_cnd_ant_cancell : forall x a , ContextND_Inert _ _ (cnd_ant_cancell x a)
+ | cnd_inert_cnd_ant_cancelr : forall x a , ContextND_Inert _ _ (cnd_ant_cancelr x a)
+ | cnd_inert_cnd_ant_llecnac : forall x a , ContextND_Inert _ _ (cnd_ant_llecnac x a)
+ | cnd_inert_cnd_ant_rlecnac : forall x a , ContextND_Inert _ _ (cnd_ant_rlecnac x a)
+ | cnd_inert_se_expand_left : forall t g s , ContextND_Inert _ _ (@cnd_expand_left _ t g s)
+ | cnd_inert_se_expand_right : forall t g s , ContextND_Inert _ _ (@cnd_expand_right _ t g s).
+
+ Class ContextND_Relation {ndr}{sndr:SequentND_Relation _ ndr} :=
+ { cndr_inert : forall {a}{b}(f g:a/⋯⋯/b),
+ NDPredicateClosure ContextND_Inert f ->
+ NDPredicateClosure ContextND_Inert g ->
+ ndr_eqv f g
+ ; cndr_sndr := sndr
}.
- End Sequents.
+ (* a proof is Analytic if it does not use cut *)
+ (*
+ Definition Analytic_Rule : NDPredicate :=
+ fun h c f => forall c, not (snd_cut _ _ c = f).
+ Definition AnalyticND := NDPredicateClosure Analytic_Rule.
- (* Sequent systems in which each side of the sequent is a tree of something *)
- Section SequentsOfTrees.
- Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}.
- Context (ndr:ND_Relation).
- Notation "a |= b" := (sequent a b).
- Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope.
-
- (* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules
- * mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *)
- Class TreeStructuralRules :=
- { tsr_ant_assoc : forall x a b c, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
- ; tsr_ant_cossa : forall x a b c, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
- ; tsr_ant_cancell : forall x a , ND [ [],,a |= x] [ a |= x]
- ; tsr_ant_cancelr : forall x a , ND [a,,[] |= x] [ a |= x]
- ; tsr_ant_llecnac : forall x a , ND [ a |= x] [ [],,a |= x]
- ; tsr_ant_rlecnac : forall x a , ND [ a |= x] [ a,,[] |= x]
+ (* a proof system has cut elimination if, for every proof, there is an analytic proof with the same conclusion *)
+ Class CutElimination :=
+ { ce_eliminate : forall h c, h/⋯⋯/c -> h/⋯⋯/c
+ ; ce_analytic : forall h c f, AnalyticND (ce_eliminate h c f)
}.
- Notation "[# a #]" := (nd_rule a) : nd_scope.
-
- (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *)
- Context `{se_cut : @CutRule _ sequent ndr sc}.
- Class SequentExpansion :=
- { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
- ; se_expand_right : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
-
- (* left and right expansion must commute with cut *)
- ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; se_expand_left c === nd_seq_reflexive (c,, a)
- ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; se_expand_right c === nd_seq_reflexive (a,, c)
- ; se_cut_left : ∀ a b c d, (se_expand_left _)**(se_expand_left _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_left c)
- ; se_cut_right : ∀ a b c d, (se_expand_right _)**(se_expand_right _);;nd_cut _ _ _===nd_cut a b d;;(se_expand_right c)
+ (* cut elimination is strong if the analytic proof is furthermore equivalent to the original proof *)
+ Class StrongCutElimination :=
+ { sce_ce <: CutElimination
+ ; ce_strong : forall h c f, f === ce_eliminate h c f
}.
- End SequentsOfTrees.
+ *)
+
+ End ContextND.
Close Scope nd_scope.
Open Scope pf_scope.
End Natural_Deduction.
-Coercion nd_cut : CutRule >-> Funclass.
+Coercion snd_cut : SequentND >-> Funclass.
+Coercion cnd_snd : ContextND >-> SequentND.
+Coercion sndr_ndr : SequentND_Relation >-> ND_Relation.
+Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation.
Implicit Arguments ND [ Judgment ].
-Hint Constructors Structural.
-Hint Extern 1 => apply nd_id_structural.
-Hint Extern 1 => apply ndr_structural_indistinguishable.
(* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
* of proofs. When only one kind of proof is in use, it's quite helpful though. *)
Notation "[# a #]" := (nd_rule a) : nd_scope.
Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope.
+Hint Constructors Structural.
+Hint Constructors ND_Relation.
+Hint Constructors BuiltFrom.
+Hint Constructors NDPredicateClosure.
+Hint Constructors ContextND_Inert.
+Hint Constructors SequentND_Inert.
+Hint Unfold StructuralND.
+
(* enable setoid rewriting *)
Open Scope nd_scope.
Open Scope pf_scope.
+Hint Extern 2 (StructuralND (nd_id _)) => apply nd_id_structural.
+Hint Extern 2 (NDPredicateClosure _ ( _ ;; _ ) ) => apply ndpc_comp.
+Hint Extern 2 (NDPredicateClosure _ ( _ ** _ ) ) => apply ndpc_prod.
+Hint Extern 2 (NDPredicateClosure (@Structural _ _) (nd_id _)) => apply nd_id_structural.
+Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp1.
+Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp2.
+Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod1.
+Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod2.
+
+(* Hint Constructors has failed me! *)
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id0 _ _)) => apply nd_structural_id0.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id1 _ _ _)) => apply nd_structural_id1.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cancell _ _ _)) => apply nd_structural_cancell.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cancelr _ _ _)) => apply nd_structural_cancelr.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_llecnac _ _ _)) => apply nd_structural_llecnac.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_rlecnac _ _ _)) => apply nd_structural_rlecnac.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_assoc _ _ _ _ _)) => apply nd_structural_assoc.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cossa _ _ _ _ _)) => apply nd_structural_cossa.
+
+Hint Extern 4 (NDPredicateClosure _ _) => apply ndpc_p.
+
Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c))
symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c))
intros; apply ndr_prod_respects; auto.
Defined.
+Section ND_Relation_Facts.
+ Context `{ND_Relation}.
+
+ (* useful *)
+ Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f.
+ intros; apply (ndr_builtfrom_structural f). auto.
+ auto.
+ Defined.
+
+ (* useful *)
+ Lemma ndr_comp_left_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (nd_id h ;; f) f.
+ intros; apply (ndr_builtfrom_structural f); auto.
+ Defined.
+
+ Ltac nd_prod_preserves_comp_ltac P EQV :=
+ match goal with
+ [ |- context [ (?A ** ?B) ;; (?C ** ?D) ] ] =>
+ set (@ndr_prod_preserves_comp _ _ EQV _ _ A _ _ B _ C _ D) as P
+ end.
+
+ Lemma nd_swap A B C D (f:ND _ A B) (g:ND _ C D) :
+ (f ** nd_id C) ;; (nd_id B ** g) ===
+ (nd_id A ** g) ;; (f ** nd_id D).
+ setoid_rewrite <- ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ setoid_rewrite ndr_comp_right_identity.
+ reflexivity.
+ Qed.
+
+ (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
+ Ltac nd_swap_ltac P EQV :=
+ match goal with
+ [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
+ set (@nd_swap _ _ EQV _ _ _ _ F G) as P
+ end.
+
+ Lemma nd_prod_split_left A B C D (f:ND _ A B) (g:ND _ B C) :
+ nd_id D ** (f ;; g) ===
+ (nd_id D ** f) ;; (nd_id D ** g).
+ setoid_rewrite <- ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ reflexivity.
+ Qed.
+
+ Lemma nd_prod_split_right A B C D (f:ND _ A B) (g:ND _ B C) :
+ (f ;; g) ** nd_id D ===
+ (f ** nd_id D) ;; (g ** nd_id D).
+ setoid_rewrite <- ndr_prod_preserves_comp.
+ setoid_rewrite ndr_comp_left_identity.
+ reflexivity.
+ Qed.
+
+End ND_Relation_Facts.
+
(* a generalization of the procedure used to build (nd_id n) from nd_id0 and nd_id1 *)
Definition nd_replicate
: forall
with
| nd_id0 => let case_nd_id0 := tt in _
| nd_id1 h => let case_nd_id1 := tt in _
- | nd_weak h => let case_nd_weak := tt in _
+ | nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
+ | nd_exch x y => let case_nd_exch := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
| nd_rule _ _ rule => let case_nd_rule := tt in _
destruct case_nd_id1. apply nd_id1.
destruct case_nd_weak. apply nd_weak.
destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_exch. apply nd_exch.
destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
destruct case_nd_cancell. apply nd_cancell.
with
| nd_id0 => let case_nd_id0 := tt in _
| nd_id1 h => let case_nd_id1 := tt in _
- | nd_weak h => let case_nd_weak := tt in _
+ | nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
+ | nd_exch x y => let case_nd_exch := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
| nd_rule _ _ rule => let case_nd_rule := tt in _
destruct case_nd_id1. apply nd_id1.
destruct case_nd_weak. apply nd_weak.
destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_exch. apply nd_exch.
destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
destruct case_nd_cancell. apply nd_cancell.
| nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r).
Hint Constructors nd_property.
-(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedSIND) *)
-Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedSIND Judgment Rule c -> Prop :=
-| cnd_property_weak : @cnd_property _ _ P _ cnd_weak
-| cnd_property_rule : forall h c r cnd',
- P h c r ->
- @cnd_property _ _ P h cnd' ->
- @cnd_property _ _ P c (cnd_rule _ _ cnd' r)
-| cnd_property_branch :
- forall c1 c2 cnd1 cnd2,
- @cnd_property _ _ P c1 cnd1 ->
- @cnd_property _ _ P c2 cnd2 ->
- @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2).
-
(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SIND) *)
Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SIND Judgment Rule h c -> Prop :=
| scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c)
rawLatexMath "% nd_id0 " +++ eolL
| nd_id1 h' => rawLatexMath indent +++
rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
- | nd_weak h' => rawLatexMath indent +++
+ | nd_weak1 h' => rawLatexMath indent +++
rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
| nd_copy h' => rawLatexMath indent +++
rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
+ | nd_exch x y => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=exch]{"+++judgments2latex h+++
+ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
| nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
rawLatexMath "% prod " +++ eolL +++
rawLatexMath indent +++
projects / coq-hetmet.git / blobdiff