X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FNaturalDeduction.v;h=74ecaeff2980151909ed0b55bdfd4ef5e1e99254;hb=562e94b529f34fb3854be7914a49190c5243c55a;hp=acb21d0f61343a8d968960b043355ed203cafbbf;hpb=148579e5c8f6b60209a442222b932cf59f163cca;p=coq-hetmet.git diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index acb21d0..74ecaef 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -12,9 +12,7 @@ Require Import Coq.Strings.Ascii. 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: * @@ -82,6 +80,22 @@ Require Import Coq.Strings.String. * (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. *) (* @@ -116,8 +130,10 @@ Section Natural_Deduction. 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 *) @@ -139,7 +155,9 @@ Section Natural_Deduction. `(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 @@ -230,6 +248,11 @@ Section Natural_Deduction. (* 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 + ; 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 + (* 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 @@ -238,21 +261,21 @@ Section Natural_Deduction. }. (* - * Single-conclusion proofs; this is an alternate representation - * where each inference has only a single conclusion. These have - * worse compositionality properties than ND's (they don't form a - * category), 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_weak : forall c , SCND c [] - | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [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. @@ -278,22 +301,22 @@ Section Natural_Deduction. 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_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). @@ -318,13 +341,14 @@ Section Natural_Deduction. 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}. @@ -332,10 +356,12 @@ Section Natural_Deduction. 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 @@ -345,25 +371,28 @@ Section Natural_Deduction. }. End Sequents. -(*Implicit Arguments SequentCalculus [ S ]*) -(*Implicit Arguments CutRule [ S ]*) + + (* 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] + { 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] @@ -539,8 +568,8 @@ Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall | 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 *) -Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedND Judgment Rule c -> Prop := +(* 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 -> @@ -552,7 +581,8 @@ Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : foral @cnd_property _ _ P c2 cnd2 -> @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2). -Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SCND Judgment Rule h c -> Prop := +(* 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 -> @@ -564,5 +594,84 @@ Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : fora @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.