- (* 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.
-
- 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.
-
- (* 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.
-