- destruct case_ECoApp.
- simpl.
- apply flatten in e.
- eapply ECoApp.
- unfold mkHaskCoercionKind in *.
- simpl in γ.
- apply flattenCoercion in γ.
- unfold coMap in γ at 2.
- apply γ.
- apply e.
-
- destruct case_ETyLam.
- apply flatten in e.
- set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
- unfold HaskTAll in *.
- unfold typeMap_ in *.
- rewrite <- foo in e'.
- unfold typeMap in e'.
- simpl in e'.
- apply ETyLam.
-
-Set Printing Implicit.
-idtac.
-idtac.
-
-
- admit.
-
- destruct case_ECase.
- admit.
-
- destruct case_ELetRec.
- admit.
- Defined.
-
- (* This proof will work for any dynamic semantics you like, so
- * long as those semantics are an ND_Relation (associativity,
- * neutrality, etc) *)
- Context (dynamic_semantics : @ND_Relation _ Rule).
-
- Section SystemFC_Category.
-
- Context {Γ:TypeEnv}
- {Δ:CoercionEnv Γ}.
-
- Definition Context := Tree ??(LeveledHaskType Γ ★).
-
- Notation "a |= b" := (Γ >> Δ > a |- b).
-
- (*
- 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 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.
-
- Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
- admit.
- Defined.
-
- Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
- admit.
- Qed.
-
- Definition append_brak_to_id : forall {c},
- @ND_FC V
- (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
- (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
- admit.
- Defined.
-
- Definition append_brak : forall {h c}
- (pf:@ND_FC V
- h
- (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
- @ND_FC V
- h
- (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
-
- refine (fix append_brak h c nd {struct nd} :=
- ((match nd
- as nd'
- in @ND _ _ H C
- return
- (H=h) ->
- (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
- ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
- with
- | nd_id0 => let case_nd_id0 := tt in _
- | nd_id1 h => let case_nd_id1 := tt in _
- | nd_weak h => let case_nd_weak := tt in _
- | nd_copy h => let case_nd_copy := tt in _
- | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
- | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
- | nd_rule _ _ rule => let case_nd_rule := tt in _
- | nd_cancell _ => let case_nd_cancell := tt in _
- | nd_cancelr _ => let case_nd_cancelr := tt in _
- | nd_llecnac _ => let case_nd_llecnac := tt in _
- | nd_rlecnac _ => let case_nd_rlecnac := tt in _
- | nd_assoc _ _ _ => let case_nd_assoc := tt in _
- | nd_cossa _ _ _ => let case_nd_cossa := tt in _
- end) (refl_equal _) (refl_equal _)
- ));
- simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
- destruct case_nd_id0. apply nd_id0.
- destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
- destruct case_nd_weak. apply nd_weak.
-
- destruct case_nd_copy.
- (*
- destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
- inversion H0; subst.
- simpl.*)
- idtac.
- clear H0.
- admit.
-
- destruct case_nd_prod.
- eapply nd_prod.
- apply (append_brak _ _ lpf).
- apply (append_brak _ _ rpf).
-
- destruct case_nd_comp.
- apply append_brak in bot.
- apply (nd_comp top bot).
-
- destruct case_nd_cancell.
- eapply nd_comp; [ apply nd_cancell | idtac ].
- apply append_brak_to_id.
-
- destruct case_nd_cancelr.
- eapply nd_comp; [ apply nd_cancelr | idtac ].
- apply append_brak_to_id.
-
- destruct case_nd_llecnac.
- eapply nd_comp; [ idtac | apply nd_llecnac ].
- apply append_brak_to_id.
-
- destruct case_nd_rlecnac.
- eapply nd_comp; [ idtac | apply nd_rlecnac ].
- apply append_brak_to_id.
-
- destruct case_nd_assoc.
- eapply nd_comp; [ apply nd_assoc | idtac ].
- repeat rewrite fixit.
- apply append_brak_to_id.
-
- destruct case_nd_cossa.
- eapply nd_comp; [ idtac | apply nd_cossa ].
- repeat rewrite fixit.
- apply append_brak_to_id.
-
- destruct case_nd_rule
-
-
-
- Defined.
-
- Definition append_brak {h c} : forall
- pf:@ND_FC V
- (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
- c,
- @ND_FC V
- (fixify Γ past (EscBrak_Functor_Fobj h))
- c.
- admit.
- Defined.
-*)
-*)
-End HaskProofCategory.