From 9e7ea73d3a6f4bbfba279164a806490cf95efec4 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 24 Apr 2011 22:52:09 -0700 Subject: [PATCH 1/1] remove ClosedSIND (use "SIND []" instead) --- src/HaskProofStratified.v | 4 +-- src/HaskProofToStrong.v | 18 ++++++-------- src/NaturalDeduction.v | 60 --------------------------------------------- 3 files changed, 10 insertions(+), 72 deletions(-) diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v index ee475da..177bd6d 100644 --- a/src/HaskProofStratified.v +++ b/src/HaskProofStratified.v @@ -231,7 +231,7 @@ Section HaskProofStratified. Alternating c'. Require Import Coq.Logic.Eqdep. - +(* Lemma magic a b c d ec e : ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. @@ -318,7 +318,7 @@ Section HaskProofStratified. destruct c; try destruct o; inversion H. destruct j. Admitted. - +*) (* any proof in organized form can be "dis-organized" *) (* Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 06f97a1..52f2154 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -758,15 +758,12 @@ Section HaskProofToStrong. apply H2. Defined. - Definition closed2expr : forall c (pn:@ClosedSIND _ Rule c), ITree _ judg2exprType c. - refine (( - fix closed2expr' j (pn:@ClosedSIND _ Rule j) {struct pn} : ITree _ judg2exprType j := - match pn in @ClosedSIND _ _ J return ITree _ judg2exprType J with - | cnd_weak => let case_nil := tt in INone _ _ - | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd') - | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2) - end)); clear closed2expr'; intros; subst. - Defined. + Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j := + match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with + | scnd_weak _ => let case_nil := tt in fun _ => INone _ _ + | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q) + | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q) + end. Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★), FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }. @@ -804,7 +801,7 @@ Section HaskProofToStrong. {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). intro pf. - set (closedFromSIND _ _ (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. + set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd. apply closed2expr in cnd. apply ileaf in cnd. simpl in *. @@ -819,6 +816,7 @@ Section HaskProofToStrong. refine (return OK _). exists ξ. apply (ileaf it). + apply INone. Defined. End HaskProofToStrong. diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 4ecc166..719e714 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -325,53 +325,6 @@ Section Natural_Deduction. inversion bogus. Defined. - (* 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. - (* Natural Deduction systems whose judgments happen to be pairs of the same type *) Section SequentND. Context {S:Type}. (* type of sequent components *) @@ -751,19 +704,6 @@ 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 (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 -> - @cnd_property _ _ P h cnd' -> - @cnd_property _ _ P c (cnd_rule _ _ cnd' r) -| cnd_property_branch : - forall c1 c2 cnd1 cnd2, - @cnd_property _ _ P c1 cnd1 -> - @cnd_property _ _ P c2 cnd2 -> - @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2). - (* 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) -- 1.7.10.4