(*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq *)
+(* NaturalDeduction: *)
+(* *)
+(* Structurally explicit natural deduction proofs. *)
+(* *)
(*********************************************************************************************************************************)
Generalizable All Variables.
| 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
}.
(*
* emit as LaTeX code.
*)
Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type :=
- | scnd_axiom : forall c , SCND [] [c]
| 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]
.
Hint Constructors SCND.
- Definition mkSCNDAxioms (h:Tree ??Judgment) : SCND [] h.
- induction h.
- destruct a.
- apply scnd_leaf. apply scnd_axiom.
- apply scnd_weak.
- apply scnd_branch; auto.
- Defined.
-
(* 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.
(* 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_rule : forall h c , ClosedND h -> Rule h c -> ClosedND c
| cnd_branch : forall c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (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
| scnd_weak c => let case_weak := tt in _
| scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _
- | scnd_axiom c => let case_axiom := 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
end (refl_equal _) (refl_equal _))) h c pn2 cnd).
- destruct case_axiom.
- intros; subst.
- (* FIXME *)
-
destruct case_comp.
intros.
clear pn2.
apply q1. subst. apply cnd0.
apply q2. subst. apply cnd0.
Defined.
- *)
+
+ (* undo the above *)
+ Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
+ match cnd in ClosedND 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.
+
+ 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.
+
+ Class SequentCalculus :=
+ { nd_seq_reflexive : forall a, ND [ ] [ a |= a ]
+ }.
+
+ 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.
+(*Implicit Arguments SequentCalculus [ S ]*)
+(*Implicit Arguments CutRule [ S ]*)
+ 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.
+
+ 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.
+
+ 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.
projects / coq-hetmet.git / blobdiff