- (*
- SystemFCa
- PCF
- SystemFCa_two_level
- SystemFCa_initial_GArrow
- *)
-
- Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
- Check (@ProgrammingLanguage).
- Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
- (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
- Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
- Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
-
- (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
- * code types are still permitted! *)
- Section SingleLevel.
- Context (lev:HaskLevel Γ).
-
- Inductive ContextAtLevel : Context -> Prop :=
- | contextAtLevel_nil : ContextAtLevel []
- | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
- | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
-
- Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
- | judgmentsAtLevel_nil : JudgmentsAtLevel []
- | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
- | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
-
- Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
- Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
- End SingleLevel.
-
- End SystemFC_Category.
-
- Implicit Arguments TypesFC [ ].
-
-(*
- Section EscBrak_Functor.
- Context
- (past:@Past V)
- (n:V)
- (Σ₁:Tree ??(@LeveledHaskType V)).
-
- Definition EscBrak_Functor_Fobj
- : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
- := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
- let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
-
- Definition append_brak
- : forall {c}, ND_ML
- (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
- (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
- intros.
- unfold ND_ML.
- unfold EscBrak_Functor_Fobj.
- rewrite mapOptionTree_comp.
- simpl in *.
- apply nd_replicate.
- intro o; destruct o.
- apply nd_rule.
- apply MLRBrak.
- Defined.
-
- Definition prepend_esc
- : forall {h}, ND_ML
- (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
- (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
- intros.
- unfold ND_ML.
- unfold EscBrak_Functor_Fobj.
- rewrite mapOptionTree_comp.
- simpl in *.
- apply nd_replicate.
- intro o; destruct o.
- apply nd_rule.
- apply MLREsc.
- Defined.
-
- Definition EscBrak_Functor_Fmor
- : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
- (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
- intros.
- eapply nd_comp.
- apply prepend_esc.
- eapply nd_comp.
- eapply Flat_to_ML.
- apply f.
- apply append_brak.
- Defined.
-
- Lemma esc_then_brak_is_id : forall a,
- ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
- (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
- admit.
- Qed.
-
- Lemma brak_then_esc_is_id : forall a,
- ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
- (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
- admit.
- Qed.
-
- Instance EscBrak_Functor
- : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
- { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
- intros; unfold EscBrak_Functor_Fmor; simpl in *.
- apply ndr_comp_respects; try reflexivity.
- apply ndr_comp_respects; try reflexivity.
- auto.
- intros; unfold EscBrak_Functor_Fmor; simpl in *.
- set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
- setoid_rewrite q.
- apply esc_then_brak_is_id.
- intros; unfold EscBrak_Functor_Fmor; simpl in *.
- set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
- repeat setoid_rewrite q.
- apply ndr_comp_respects; try reflexivity.
- apply ndr_comp_respects; try reflexivity.
- repeat setoid_rewrite <- q.
- apply ndr_comp_respects; try reflexivity.
- setoid_rewrite brak_then_esc_is_id.
- clear q.
- set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
- setoid_rewrite q.
- reflexivity.
- Defined.
-
- End EscBrak_Functor.
-
-
-
- Ltac rule_helper_tactic' :=
- match goal with
- | [ H : ?A = ?A |- _ ] => clear H
- | [ H : [?A] = [] |- _ ] => inversion H; clear H
- | [ H : [] = [?A] |- _ ] => inversion H; clear H
- | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
- | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
- | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
- | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
- | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
- | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
-(* | [ H : Sequent T |- _ ] => destruct H *)
-(* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
- | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
- | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
- | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
- | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
- end.