From 4ec2860679a25b16cba9df2de6ea971064200756 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 22 May 2011 23:55:56 -0700 Subject: [PATCH] NaturalDeduction: add nd_exch --- src/NaturalDeduction.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 3aeb7db..caa4dcf 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -142,6 +142,9 @@ Section Natural_Deduction. (* 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 ) @@ -295,6 +298,7 @@ Section Natural_Deduction. 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. @@ -603,6 +607,7 @@ Definition nd_map | nd_id1 h => let case_nd_id1 := 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 _ @@ -618,6 +623,7 @@ Definition nd_map 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. @@ -651,6 +657,7 @@ Definition nd_map' | nd_id1 h => let case_nd_id1 := 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 _ @@ -666,6 +673,7 @@ Definition nd_map' 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. @@ -744,6 +752,9 @@ Section ToLatex. | 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 +++ -- 1.7.10.4