(*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq *)
+(* NaturalDeduction: *)
+(* *)
+(* Structurally explicit natural deduction proofs. *)
+(* *)
(*********************************************************************************************************************************)
Generalizable All Variables.
Require Import Coq.Strings.String.
(*
- * IMPORTANT!!!
- *
- * Unlike most formalizations, this library offers TWO different ways
+ * Unlike most formalizations, this library offers two different ways
* to represent a natural deduction proof. To demonstrate this,
* consider the signature of the propositional calculus:
*
* (NaturalDeduction.v) and are designed specifically in order to
* circumvent the problem in the previous paragraph.
*
+ * These proofs are actually structurally explicit on (potentially)
+ * two different levels. The beginning of this file formalizes
+ * natural deduction proofs with explicit structural operations for
+ * manipulating lists of judgments – for example, the open
+ * hypotheses of an incomplete proof. The class
+ * TreeStructuralRules further down in the file instantiates ND
+ * such that Judgments is actually a pair of trees of propositions,
+ * and there will be a whole *other* set of rules for manipulating
+ * the structure of a tree of propositions *within* a single
+ * judgment.
+ *
+ * The flattening functor ends up mapping the first kind of
+ * structural operation (moving around judgments) onto the second
+ * kind (moving around propositions/types). That's why everything
+ * is so laboriously explicit - there's important information in
+ * those structural operations.
*)
(*
forall conclusions:Tree ??Judgment,
Type :=
- (* natural deduction: you may infer anything from itself -- "identity proof" *)
+ (* natural deduction: you may infer nothing from nothing *)
| nd_id0 : [ ] /⋯⋯/ [ ]
+
+ (* natural deduction: you may infer anything from itself -- "identity proof" *)
| nd_id1 : forall h, [ h ] /⋯⋯/ [ h ]
(* natural deduction: you may discard conclusions *)
`(pf2: x /⋯⋯/ c),
( h /⋯⋯/ c)
- (* structural rules on lists of judgments *)
+ (* Structural rules on lists of judgments - note that this is completely separate from the structural
+ * rules for *contexts* within a sequent. The rules below manipulate lists of *judgments* rather than
+ * lists of *propositions*. *)
| nd_cancell : forall {a}, [] ,, a /⋯⋯/ a
| nd_cancelr : forall {a}, a ,, [] /⋯⋯/ a
| nd_llecnac : forall {a}, a /⋯⋯/ [] ,, a
| T_Branch a b => nd_prod (nd_id a) (nd_id b)
end.
+ 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
+ end.
+
Hint Constructors Structural.
Lemma nd_id_structural : forall sl, Structural (nd_id sl).
intros.
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 :=
(* 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
+
(* 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
+
+ (* any two proofs of nothing are "equally good" *)
+ ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
}.
(*
- * Single-conclusion proofs; this is an alternate representation
- * where each inference has only a single conclusion. These have
- * worse compositionality properties than ND's, but are easier to
- * emit as LaTeX code.
+ * Natural Deduction proofs which are Structurally Implicit on the
+ * level of judgments. These proofs have poor compositionality
+ * properties (vertically, they look more like lists than trees) but
+ * are easier to do induction over.
*)
- Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
- | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
- | scnd_weak : forall c , SCND c []
- | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
- | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
+ Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type :=
+ | scnd_weak : forall c , SIND c []
+ | scnd_comp : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c]
+ | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2)
.
- Hint Constructors SCND.
+ Hint Constructors SIND.
- (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SCND. *)
- Definition mkSCND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
- : forall h x c, ND x c -> SCND h x -> SCND h c.
+ (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *)
+ Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False)
+ : forall h x c, ND x c -> SIND h x -> SIND h c.
intros h x c nd.
induction nd; intro k.
apply k.
inversion k; subst; inversion X0; subst; auto.
destruct c.
destruct o.
- apply scnd_leaf. eapply scnd_comp. apply k. apply r.
+ eapply scnd_comp. apply k. apply r.
apply scnd_weak.
set (all_rules_one_conclusion _ _ _ r) as bogus.
inversion bogus.
Defined.
- (* a "ClosedND" is a proof with no open hypotheses and no multi-conclusion rules *)
- Inductive ClosedND : Tree ??Judgment -> Type :=
- | cnd_weak : ClosedND []
- | cnd_rule : forall h c , ClosedND h -> Rule h c -> ClosedND c
- | cnd_branch : forall c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2)
+ (* 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 SCND without hypotheses into a ClosedND *)
- Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
- refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
- (match pn2 in SCND H C return H=h -> C=c -> _ with
+ (* 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_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' 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 _
+ let q1 := closedFromPnodes _ _ pn' in
+ let q2 := closedFromPnodes _ _ pn'' in _
end (refl_equal _) (refl_equal _))) h c pn2 cnd).
- destruct case_comp.
- intros.
- clear pn2.
- apply (cnd_rule ct).
- apply qq.
- subst.
- apply cnd0.
- apply rule.
-
destruct case_weak.
intros; subst.
apply cnd_weak.
- destruct case_leaf.
+ destruct case_comp.
intros.
+ clear pn2.
+ apply (cnd_rule ct).
apply qq.
subst.
apply cnd0.
+ apply rule.
destruct case_branch.
intros.
Defined.
(* undo the above *)
- Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
- match cnd in ClosedND C return ND [] C with
+ 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.
+ (* 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}.
+ 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 ]
+ }.
+
+ (* 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
+ }.
+
+ End Sequents.
+
+ (* 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]
+ }.
+
+ 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)
+ }.
+ End SequentsOfTrees.
+
Close Scope nd_scope.
Open Scope pf_scope.
End Natural_Deduction.
+Coercion nd_cut : CutRule >-> Funclass.
+
Implicit Arguments ND [ Judgment ].
Hint Constructors Structural.
Hint Extern 1 => apply nd_id_structural.
| 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)
+| scnd_property_comp : forall h x c r cnd',
+ P x [c] r ->
+ @scnd_property _ _ P h x cnd' ->
+ @scnd_property _ _ P h _ (scnd_comp _ _ _ cnd' r)
+| scnd_property_branch :
+ forall x c1 c2 cnd1 cnd2,
+ @scnd_property _ _ P x c1 cnd1 ->
+ @scnd_property _ _ P x c2 cnd2 ->
+ @scnd_property _ _ P x _ (scnd_branch _ _ _ cnd1 cnd2).
+
+(* renders a proof as LaTeX code *)
+Section ToLatex.
+
+ Context {Judgment : Type}.
+ Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
+ Context {JudgmentToLatexMath : ToLatexMath Judgment}.
+ Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}.
+
+ Open Scope string_scope.
+
+ Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
+
+ Definition eolL : LatexMath := rawLatexMath eol.
+
+ (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
+ Section SIND_toLatex.
+
+ (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
+ Context (hideRule : forall h c (r:Rule h c), bool).
+
+ Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath :=
+ match pns with
+ | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2
+ | scnd_weak c => rawLatexMath ""
+ | scnd_comp ht ct c pns rule => if hideRule _ _ rule
+ then SIND_toLatexMath pns
+ else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
+ SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
+ toLatexMath c +++ rawLatexMath "}" +++ eolL
+ end.
+ End SIND_toLatex.
+
+ (* this is a work-in-progress; please use SIND_toLatexMath for now *)
+ Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
+ match nd with
+ | nd_id0 => rawLatexMath indent +++
+ rawLatexMath "% nd_id0 " +++ eolL
+ | nd_id1 h' => rawLatexMath indent +++
+ rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
+ | nd_weak 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_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% prod " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " & " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% comp " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " \\ " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_cancell a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
+ | nd_cancelr a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
+ | nd_llecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
+ | nd_rlecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
+ | nd_assoc a b c => rawLatexMath ""
+ | nd_cossa a b c => rawLatexMath ""
+ | nd_rule h c r => toLatexMath r
+ end.
+
+End ToLatex.
+
Close Scope pf_scope.
Close Scope nd_scope.
projects / coq-hetmet.git / blobdiff