-(*
- Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
- refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
- match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
- | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
- | EVar Γ Δ ξ ev => EVar _ _ _ ev
- | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
- | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
- | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
- | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
- | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
- | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
- | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
- | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
- | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
- | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
- | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
-
- | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
- | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
- end); clear exp ξ' τ' Γ' Δ'.
-
- destruct case_ELit.
- simpl.
- rewrite lit_lemma.
- apply ELit.
-
- destruct case_ELam.
- set (flatten _ _ _ _ e) as q.
- rewrite update_typeMap in q.
- apply (@ELam _ _ _ _ _ _ _ _ v q).
-
- destruct case_ELet.
- set (flatten _ _ _ _ ebody) as ebody'.
- set (flatten _ _ _ _ elet) as elet'.
- rewrite update_typeMap in ebody'.
- apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
-
- destruct case_EEsc.
- admit.
- destruct case_EBrak.
- admit.
-
- destruct case_ECast.
- apply flatten in e.
- eapply ECast in e.
- apply e.
- apply flattenCoercion in γ.
- apply γ.
-
- destruct case_ETyApp.
- apply flatten in e.
- simpl in e.
- unfold HaskTAll in e.
- unfold typeMap_ in e.
- simpl in e.
- eapply ETyApp in e.
- rewrite <- foo in e.
- apply e.
-
- destruct case_ECoLam.
- apply flatten in e.
- simpl in e.
- set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
- simpl in x.
- simpl.
- unfold typeMap_.
- simpl.
- apply x.
-
- 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.