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).
(* 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.
| 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,
| 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).
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 [ ].
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').
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 _
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].
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.
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.
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.
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.
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.
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 Γ Δ))
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) *)
| 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 *.
(* 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.
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 _ Γ Δ))
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) *)
| 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 *.
(* 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.
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 [ ].
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').
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 _
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].
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.
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.
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.
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.
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.
| 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 :=
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.
{ 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 [])).
| 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 _
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.
apply X0'.
apply X1'.
- destruct case_REmptyGroup.
+ destruct case_RVoid.
apply ILeaf; simpl; intros.
refine (return _).
apply INone.
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)
{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 *.
|- (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.
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.
* 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.
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
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)
| 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 ->
@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 ->
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 +++
projects / coq-hetmet.git / commitdiff