From 6ef9f270b138fc7aab48013d55a8192ff022c0f1 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 29 Mar 2011 11:03:35 -0700 Subject: [PATCH] formatting fixes --- src/GeneralizedArrowFromReification.v | 22 +++++++---- src/HaskProof.v | 8 ++-- src/HaskProofCategory.v | 68 ++++++++++++++++----------------- src/HaskProofFlattener.v | 24 ++++++------ src/HaskProofStratified.v | 44 ++++++++++----------- src/HaskProofToLatex.v | 12 +++--- src/HaskProofToStrong.v | 16 ++++---- src/HaskStrongToProof.v | 6 +-- src/NaturalDeduction.v | 60 ++++++++++++++--------------- 9 files changed, 133 insertions(+), 127 deletions(-) diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 356ee57..4a9e790 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -118,7 +118,6 @@ Section GArrowFromReification. setoid_rewrite left_identity; reflexivity). Qed. - Opaque homset_tensor_iso. (* the "step2_functor" is the section of the Hom(I,-) functor *) Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C). @@ -126,19 +125,26 @@ Section GArrowFromReification. (* the generalized arrow is the composition of the two steps *) Definition garrow_functor := step1_functor >>>> step2_functor. - Lemma garrow_functor_monoidal_niso - : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor. - unfold garrow_functor. + Lemma garrow_functor_monoidal_iso_i + : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)). admit. Defined. - Lemma garrow_functor_monoidal_iso - : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)). + + Lemma garrow_functor_monoidal_iso : + forall X Y:enr_v_mon K, + garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y). admit. Defined. + Definition garrow_functor_monoidal_niso + : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor. + admit. + Defined. + Opaque homset_tensor_iso. + Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor := - { mf_coherence := garrow_functor_monoidal_niso - ; mf_id := garrow_functor_monoidal_iso + { mf_coherence := garrow_functor_monoidal_niso + ; mf_id := garrow_functor_monoidal_iso_i }. admit. admit. diff --git a/src/HaskProof.v b/src/HaskProof.v index 72d59cb..a5e4abd 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -78,13 +78,13 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] -| RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] +| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] -| REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] +| RVoid : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] | RAbsT : ∀ Γ Δ Σ κ σ l, @@ -122,8 +122,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 ) | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) -| Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e) -| Flat_REmptyGroup : ∀ q a , Rule_Flat (REmptyGroup q a) +| Flat_RJoin : ∀ q a b c d e , Rule_Flat (RJoin q a b c d e) +| Flat_RVoid : ∀ q a , Rule_Flat (RVoid q a) | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v index cf1fb86..4140f7d 100644 --- a/src/HaskProofCategory.v +++ b/src/HaskProofCategory.v @@ -115,10 +115,10 @@ Section HaskProofCategory. Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]] (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil)) - | PCF_REmptyGroup : Rule_PCF ec [ ] [ pcfjudg [] [] ] (REmptyGroup Γ Δ ) + | PCF_RVoid : Rule_PCF ec [ ] [ pcfjudg [] [] ] (RVoid Γ Δ ) (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*) - | PCF_RBindingGroup : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)] - (RBindingGroup Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). + | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)] + (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). (* need int/boolean case *) Implicit Arguments Rule_PCF [ ]. @@ -228,24 +228,24 @@ Section HaskProofCategory. Require Import Coq.Logic.Eqdep. Lemma magic a b c d ec e : - ClosedND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> - ClosedND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. + ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> + ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. admit. Defined. - Definition orgify : forall Γ Δ Σ τ (pf:ClosedND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. + Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. refine ( - fix orgify_fc' Γ Δ Σ τ (pf:ClosedND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := + fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := let case_main := tt in _ - with orgify_fc c (pf:ClosedND c) {struct pf} : Alternating c := + with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c := (match c as C return C=c -> Alternating C with | T_Leaf None => fun _ => alt_nil | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _ | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _ end (refl_equal _)) with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments pcfj j) - (pf:ClosedND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j := + (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j := let case_pcf := tt in _ for orgify_fc'). @@ -296,13 +296,13 @@ Section HaskProofCategory. Admitted. Definition pcfify Γ Δ ec : forall Σ τ, - ClosedND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] + ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ]. refine (( - fix pcfify Σ τ (pn:@ClosedND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} + fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] := - (match pn in @ClosedND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with + (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with | cnd_weak => let case_nil := tt in _ | cnd_rule h c cnd' r => let case_rule := tt in _ | cnd_branch _ _ c1 c2 => let case_branch := tt in _ @@ -361,14 +361,14 @@ Section HaskProofCategory. exists (RVar _ _ _ _). apply PCF_RVar. apply nd_rule. - exists (REmptyGroup _ _ ). - apply PCF_REmptyGroup. + exists (RVoid _ _ ). + apply PCF_RVoid. eapply nd_comp. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply (nd_prod IHa1 IHa2). apply nd_rule. - exists (RBindingGroup _ _ _ _ _ _). - apply PCF_RBindingGroup. + exists (RJoin _ _ _ _ _ _). + apply PCF_RJoin. Defined. Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z]. @@ -417,7 +417,7 @@ Section HaskProofCategory. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. apply nd_rule. - set (@PCF_RBindingGroup Γ Δ lev a b a c) as q'. + set (@PCF_RJoin Γ Δ lev a b a c) as q'. refine (existT _ _ _). apply q'. Defined. @@ -426,7 +426,7 @@ Section HaskProofCategory. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. apply nd_rule. - set (@PCF_RBindingGroup Γ Δ lev b a c a) as q'. + set (@PCF_RJoin Γ Δ lev b a c a) as q'. refine (existT _ _ _). apply q'. Defined. @@ -484,13 +484,13 @@ Section HaskProofCategory. apply org_fc with (r:=RVar _ _ _ _). auto. apply nd_rule. - apply org_fc with (r:=REmptyGroup _ _ ). + apply org_fc with (r:=RVoid _ _ ). auto. eapply nd_comp. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply (nd_prod IHa1 IHa2). apply nd_rule. - apply org_fc with (r:=RBindingGroup _ _ _ _ _ _). + apply org_fc with (r:=RJoin _ _ _ _ _ _). auto. Defined. @@ -534,7 +534,7 @@ Section HaskProofCategory. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. apply nd_rule. - apply org_fc with (r:=RBindingGroup Γ Δ a b a c). + apply org_fc with (r:=RJoin Γ Δ a b a c). auto. Defined. @@ -542,7 +542,7 @@ Section HaskProofCategory. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. apply nd_rule. - apply org_fc with (r:=RBindingGroup Γ Δ b a c a). + apply org_fc with (r:=RJoin Γ Δ b a c a). auto. Defined. @@ -632,22 +632,22 @@ Section HaskProofCategory. induction X; simpl. - (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *) - apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto. + (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *) + apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto. (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *) apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto. - (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *) + (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *) eapply nd_comp; [ idtac | eapply nd_rule ; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RWeak _))) ; auto ]. eapply nd_rule. - eapply (org_fc _ _ (REmptyGroup _ _)); auto. + eapply (org_fc _ _ (RVoid _ _)); auto. - (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *) + (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *) eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa Γ Δ)) @@ -657,15 +657,15 @@ Section HaskProofCategory. apply q. apply q. apply nd_rule. - eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). auto. auto. - (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *) + (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *) eapply nd_comp. apply (nd_llecnac ;; nd_prod IHX1 IHX2). apply nd_rule. - eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). auto. (* nd_comp becomes pl_subst (aka nd_cut) *) @@ -719,8 +719,8 @@ Section HaskProofCategory. | PCF_RLam Σ tx te => let case_RLam := tt in _ | PCF_RApp Σ tx te p => let case_RApp := tt in _ | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _ - | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _ - | PCF_REmptyGroup => let case_REmptyGroup := tt in _ + | PCF_RJoin b c d e => let case_RJoin := tt in _ + | PCF_RVoid => let case_RVoid := tt in _ (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*) (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*) end); simpl in *. @@ -820,11 +820,11 @@ Section HaskProofCategory. (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *) admit. - destruct case_REmptyGroup. + destruct case_RVoid. (* ga_id u *) admit. - destruct case_RBindingGroup. + destruct case_RJoin. (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *) admit. diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v index 980697d..c37079f 100644 --- a/src/HaskProofFlattener.v +++ b/src/HaskProofFlattener.v @@ -142,22 +142,22 @@ Section HaskProofFlattener. induction X; simpl. - (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *) - apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto. + (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *) + apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto. (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *) apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto. - (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *) + (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *) eapply nd_comp; [ idtac | eapply nd_rule ; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RWeak _))) ; auto ]. eapply nd_rule. - eapply (org_fc _ _ (REmptyGroup _ _)); auto. + eapply (org_fc _ _ (RVoid _ _)); auto. - (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *) + (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *) eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ)) @@ -167,15 +167,15 @@ Section HaskProofFlattener. apply q. apply q. apply nd_rule. - eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). auto. auto. - (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *) + (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *) eapply nd_comp. apply (nd_llecnac ;; nd_prod IHX1 IHX2). apply nd_rule. - eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). auto. (* nd_comp becomes pl_subst (aka nd_cut) *) @@ -229,8 +229,8 @@ Section HaskProofFlattener. | PCF_RLam Σ tx te => let case_RLam := tt in _ | PCF_RApp Σ tx te p => let case_RApp := tt in _ | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _ - | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _ - | PCF_REmptyGroup => let case_REmptyGroup := tt in _ + | PCF_RJoin b c d e => let case_RJoin := tt in _ + | PCF_RVoid => let case_RVoid := tt in _ (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*) (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*) end); simpl in *. @@ -330,11 +330,11 @@ Section HaskProofFlattener. (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *) admit. - destruct case_REmptyGroup. + destruct case_RVoid. (* ga_id u *) admit. - destruct case_RBindingGroup. + destruct case_RJoin. (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *) admit. diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v index 8f70b31..d6058e5 100644 --- a/src/HaskProofStratified.v +++ b/src/HaskProofStratified.v @@ -116,10 +116,10 @@ Section HaskProofStratified. Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]] (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil)) - | PCF_REmptyGroup : Rule_PCF ec [ ] [ pcfjudg [] [] ] (REmptyGroup Γ Δ ) + | PCF_RVoid : Rule_PCF ec [ ] [ pcfjudg [] [] ] (RVoid Γ Δ ) (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*) - | PCF_RBindingGroup : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)] - (RBindingGroup Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). + | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)] + (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). (* need int/boolean case *) Implicit Arguments Rule_PCF [ ]. @@ -229,24 +229,24 @@ Section HaskProofStratified. Require Import Coq.Logic.Eqdep. Lemma magic a b c d ec e : - ClosedND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> - ClosedND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. + ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> + ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. admit. Defined. - Definition orgify : forall Γ Δ Σ τ (pf:ClosedND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. + Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. refine ( - fix orgify_fc' Γ Δ Σ τ (pf:ClosedND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := + fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := let case_main := tt in _ - with orgify_fc c (pf:ClosedND c) {struct pf} : Alternating c := + with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c := (match c as C return C=c -> Alternating C with | T_Leaf None => fun _ => alt_nil | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _ | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _ end (refl_equal _)) with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments pcfj j) - (pf:ClosedND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j := + (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j := let case_pcf := tt in _ for orgify_fc'). @@ -297,13 +297,13 @@ Section HaskProofStratified. Admitted. Definition pcfify Γ Δ ec : forall Σ τ, - ClosedND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] + ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ]. refine (( - fix pcfify Σ τ (pn:@ClosedND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} + fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] := - (match pn in @ClosedND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with + (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with | cnd_weak => let case_nil := tt in _ | cnd_rule h c cnd' r => let case_rule := tt in _ | cnd_branch _ _ c1 c2 => let case_branch := tt in _ @@ -362,14 +362,14 @@ Section HaskProofStratified. exists (RVar _ _ _ _). apply PCF_RVar. apply nd_rule. - exists (REmptyGroup _ _ ). - apply PCF_REmptyGroup. + exists (RVoid _ _ ). + apply PCF_RVoid. eapply nd_comp. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply (nd_prod IHa1 IHa2). apply nd_rule. - exists (RBindingGroup _ _ _ _ _ _). - apply PCF_RBindingGroup. + exists (RJoin _ _ _ _ _ _). + apply PCF_RJoin. Defined. Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z]. @@ -418,7 +418,7 @@ Section HaskProofStratified. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. apply nd_rule. - set (@PCF_RBindingGroup Γ Δ lev a b a c) as q'. + set (@PCF_RJoin Γ Δ lev a b a c) as q'. refine (existT _ _ _). apply q'. Defined. @@ -427,7 +427,7 @@ Section HaskProofStratified. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. apply nd_rule. - set (@PCF_RBindingGroup Γ Δ lev b a c a) as q'. + set (@PCF_RJoin Γ Δ lev b a c a) as q'. refine (existT _ _ _). apply q'. Defined. @@ -485,13 +485,13 @@ Section HaskProofStratified. apply org_fc with (r:=RVar _ _ _ _). auto. apply nd_rule. - apply org_fc with (r:=REmptyGroup _ _ ). + apply org_fc with (r:=RVoid _ _ ). auto. eapply nd_comp. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply (nd_prod IHa1 IHa2). apply nd_rule. - apply org_fc with (r:=RBindingGroup _ _ _ _ _ _). + apply org_fc with (r:=RJoin _ _ _ _ _ _). auto. Defined. @@ -535,7 +535,7 @@ Section HaskProofStratified. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ]. apply nd_rule. - apply org_fc with (r:=RBindingGroup Γ Δ a b a c). + apply org_fc with (r:=RJoin Γ Δ a b a c). auto. Defined. @@ -543,7 +543,7 @@ Section HaskProofStratified. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ]. apply nd_rule. - apply org_fc with (r:=RBindingGroup Γ Δ b a c a). + apply org_fc with (r:=RJoin Γ Δ b a c a). auto. Defined. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index bdcf1e6..4773eff 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -187,12 +187,12 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" - | RBindingGroup _ _ _ _ _ _ => "RBindingGroup" + | RJoin _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" | REsc _ _ _ _ _ _ => "Esc" - | REmptyGroup _ _ => "REmptyGroup" + | RVoid _ _ => "RVoid" end. Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := @@ -215,8 +215,8 @@ Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with | RArrange _ _ _ _ _ r => nd_hideURule r - | REmptyGroup _ _ => true - | RBindingGroup _ _ _ _ _ _ => true + | RVoid _ _ => true + | RJoin _ _ _ _ _ _ => true | _ => false end. @@ -224,5 +224,5 @@ Instance ToLatexMathRule h c : ToLatexMath (Rule h c) := { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }. Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) := -@SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _ - (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])). +@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _ + (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])). diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 2b63c4a..d38286d 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -520,8 +520,8 @@ Section HaskProofToStrong. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _ - | REmptyGroup _ _ => let case_REmptyGroup := tt in _ + | RJoin Γ p lri m x q => let case_RJoin := tt in _ + | RVoid _ _ => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ @@ -601,7 +601,7 @@ Section HaskProofToStrong. apply ileaf in X. simpl in X. apply X. - destruct case_RBindingGroup. + destruct case_RJoin. apply ILeaf; simpl; intros. inversion X_. apply ileaf in X. @@ -669,7 +669,7 @@ Section HaskProofToStrong. apply X0'. apply X1'. - destruct case_REmptyGroup. + destruct case_RVoid. apply ILeaf; simpl; intros. refine (return _). apply INone. @@ -758,10 +758,10 @@ Section HaskProofToStrong. apply H2. Defined. - Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c. + Definition closed2expr : forall c (pn:@ClosedSIND _ Rule c), ITree _ judg2exprType c. refine (( - fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j := - match pn in @ClosedND _ _ J return ITree _ judg2exprType J with + 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) @@ -804,7 +804,7 @@ Section HaskProofToStrong. {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] -> FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). intro pf. - set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. + set (closedFromSIND _ _ (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. apply closed2expr in cnd. apply ileaf in cnd. simpl in *. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index d5e57f8..c1e54aa 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -581,12 +581,12 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : |- (mapOptionTree (@snd _ _) tree) @@@ lev ]. intro X; induction X; intros; simpl in *. apply nd_rule. - apply REmptyGroup. + apply RVoid. set (ξ v) as q in *. destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. Defined. @@ -639,7 +639,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. rewrite ξlemma. diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index dde0a0c..ced66c4 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -261,16 +261,16 @@ Section Natural_Deduction. * properties (vertically, they look more like lists than trees) but * are easier to do induction over. *) - Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type := - | scnd_weak : forall c , SCND c [] - | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c] - | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2) + Inductive SIND : Tree ??Judgment -> Tree ??Judgment -> Type := + | scnd_weak : forall c , SIND c [] + | scnd_comp : forall ht ct c , SIND ht ct -> Rule ct [c] -> SIND ht [c] + | scnd_branch : forall ht c1 c2, SIND ht c1 -> SIND ht c2 -> SIND ht (c1,,c2) . - Hint Constructors SCND. + Hint Constructors SIND. - (* 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. + (* Any ND whose primitive Rules have at most one conclusion (note that nd_prod is allowed!) can be turned into an SIND. *) + Definition mkSIND (all_rules_one_conclusion : forall h c1 c2, Rule h (c1,,c2) -> False) + : forall h x c, ND x c -> SIND h x -> SIND h c. intros h x c nd. induction nd; intro k. apply k. @@ -296,17 +296,17 @@ Section Natural_Deduction. inversion bogus. Defined. - (* 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_branch : forall c1 c2, ClosedND c1 -> ClosedND c2 -> ClosedND (c1,,c2) + (* 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 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 + (* 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 @@ -336,8 +336,8 @@ Section Natural_Deduction. Defined. (* undo the above *) - Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c := - match cnd in ClosedND C return ND [] C with + 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) @@ -563,8 +563,8 @@ 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 ClosedND) *) -Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedND Judgment Rule c -> Prop := +(* 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 -> @@ -576,8 +576,8 @@ Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : foral @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 SCND) *) -Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SCND Judgment Rule h c -> Prop := +(* 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) | scnd_property_comp : forall h x c r cnd', P x [c] r -> @@ -604,24 +604,24 @@ Section ToLatex. Definition eolL : LatexMath := rawLatexMath eol. (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *) - Section SCND_toLatex. + Section SIND_toLatex. (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *) Context (hideRule : forall h c (r:Rule h c), bool). - Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath := + Fixpoint SIND_toLatexMath {h}{c}(pns:SIND(Rule:=Rule) h c) : LatexMath := match pns with - | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2 + | scnd_branch ht c1 c2 pns1 pns2 => SIND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SIND_toLatexMath pns2 | scnd_weak c => rawLatexMath "" | scnd_comp ht ct c pns rule => if hideRule _ _ rule - then SCND_toLatexMath pns + then SIND_toLatexMath pns else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++ - SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++ + SIND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++ toLatexMath c +++ rawLatexMath "}" +++ eolL end. - End SCND_toLatex. + End SIND_toLatex. - (* this is a work-in-progress; please use SCND_toLatexMath for now *) + (* this is a work-in-progress; please use SIND_toLatexMath for now *) Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) := match nd with | nd_id0 => rawLatexMath indent +++ -- 1.7.10.4