From fdebbea0c0303b8bba05779f2635c9a0e5c459b7 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:10:10 -0700 Subject: [PATCH] add n-ary form of nd_weak --- src/NaturalDeduction.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index cd225da..5cf67db 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -182,6 +182,13 @@ Section Natural_Deduction. | 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. @@ -189,6 +196,16 @@ Section Natural_Deduction. 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 := -- 1.7.10.4