1 (*********************************************************************************************************************************)
2 (* HaskProofCategory: *)
4 (* Natural Deduction proofs of the well-typedness of a Haskell term form a category *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskProof.
20 Require Import NaturalDeduction.
21 Require Import NaturalDeductionCategory.
23 Require Import Algebras_ch4.
24 Require Import Categories_ch1_3.
25 Require Import Functors_ch1_4.
26 Require Import Isomorphisms_ch1_5.
27 Require Import ProductCategories_ch1_6_1.
28 Require Import OppositeCategories_ch1_6_2.
29 Require Import Enrichment_ch2_8.
30 Require Import Subcategories_ch7_1.
31 Require Import NaturalTransformations_ch7_4.
32 Require Import NaturalIsomorphisms_ch7_5.
33 Require Import MonoidalCategories_ch7_8.
34 Require Import Coherence_ch7_8.
36 Require Import FreydCategories.
39 Section HaskProofCategory.
41 (* This proof will work for any dynamic semantics you like, so
42 * long as those semantics are an ND_Relation (associativity,
44 Context (dynamic_semantics : @ND_Relation _ Rule).
46 Section SystemFC_Category.
51 Definition Context := Tree ??(LeveledHaskType Γ ★).
53 Notation "a |= b" := (Γ >> Δ > a |- b).
55 (* category of judgments in a fixed type/coercion context *)
56 Definition JudgmentsFC :=
57 @Judgments_Category_monoidal _ Rule dynamic_semantics (UJudg Γ Δ) UJudg2judg.
59 Definition identityProof t : [] ~~{JudgmentsFC}~~> [t |= t].
64 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsFC}~~> [a |= c].
69 Definition TypesFC : ECategory JudgmentsFC Context (fun x y => [Γ >> Δ > x |- y]).
71 {| eid := identityProof
74 apply MonoidalCat_all_central.
75 apply MonoidalCat_all_central.
81 Definition TypesEnrichedInJudgments : Enrichment.
82 refine {| enr_c := TypesFC |}.
86 Definition TwoLevelLanguage L2 :=
88 Reification (TypesEnrichedInJudgments L1) (TypesEnrichedInJudgments L2) }
90 Inductive NLevelLanguage : nat -> Language -> Type :=
91 | NLevelLanguage_zero : forall lang, NLevelLanguage O lang
92 | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2
94 Definition OmegaLevelLanguage : Language -> Type :=
95 forall n:nat, NLevelLanguage n L.
99 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
100 * code types are still permitted! *)
102 Context (lev:HaskLevel Γ).
104 Inductive ContextAtLevel : Context -> Prop :=
105 | contextAtLevel_nil : ContextAtLevel []
106 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
107 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
109 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
110 | judgmentsAtLevel_nil : JudgmentsAtLevel []
111 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
112 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
114 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
115 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
118 End SystemFC_Category.
120 Implicit Arguments TypesFC [ ].
122 Definition Types_first c : EFunctor (TypesFC nil nil) (TypesFC nil nil) (fun x => x,,c ).
125 Definition Types_second c : EFunctor (TypesFC nil nil) (TypesFC nil nil) (fun x => c,,x ).
129 Definition Types_binoidal : BinoidalCat (TypesFC nil nil) (@T_Branch _).
131 {| bin_first := Types_first
132 ; bin_second := Types_second
136 Definition Types_premonoidal : PreMonoidalCat Types_binoidal [].
141 Definition ArrowInProgrammingLanguage :=
142 FreydCategory Types_premonoidal Types_premonoidal.
146 InitialGArrowsAllowFlattening
153 SystemFCa_initial_GArrow
160 Section EscBrak_Functor.
164 (Σ₁:Tree ??(@LeveledHaskType V)).
166 Definition EscBrak_Functor_Fobj
167 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
168 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
169 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
171 Definition append_brak
173 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
174 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
177 unfold EscBrak_Functor_Fobj.
178 rewrite mapOptionTree_comp.
186 Definition prepend_esc
188 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
189 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
192 unfold EscBrak_Functor_Fobj.
193 rewrite mapOptionTree_comp.
201 Definition EscBrak_Functor_Fmor
202 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
203 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
213 Lemma esc_then_brak_is_id : forall a,
214 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
215 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
219 Lemma brak_then_esc_is_id : forall a,
220 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
221 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
225 Instance EscBrak_Functor
226 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
227 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
228 intros; unfold EscBrak_Functor_Fmor; simpl in *.
229 apply ndr_comp_respects; try reflexivity.
230 apply ndr_comp_respects; try reflexivity.
232 intros; unfold EscBrak_Functor_Fmor; simpl in *.
233 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
235 apply esc_then_brak_is_id.
236 intros; unfold EscBrak_Functor_Fmor; simpl in *.
237 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
238 repeat setoid_rewrite q.
239 apply ndr_comp_respects; try reflexivity.
240 apply ndr_comp_respects; try reflexivity.
241 repeat setoid_rewrite <- q.
242 apply ndr_comp_respects; try reflexivity.
243 setoid_rewrite brak_then_esc_is_id.
245 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
254 Ltac rule_helper_tactic' :=
256 | [ H : ?A = ?A |- _ ] => clear H
257 | [ H : [?A] = [] |- _ ] => inversion H; clear H
258 | [ H : [] = [?A] |- _ ] => inversion H; clear H
259 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
260 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
261 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
262 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
263 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
264 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
265 (* | [ H : Sequent T |- _ ] => destruct H *)
266 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
267 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
268 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
269 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
270 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
273 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
277 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
281 Definition append_brak_to_id : forall {c},
283 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
284 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
288 Definition append_brak : forall {h c}
291 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
294 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
296 refine (fix append_brak h c nd {struct nd} :=
302 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
303 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
305 | nd_id0 => let case_nd_id0 := tt in _
306 | nd_id1 h => let case_nd_id1 := tt in _
307 | nd_weak h => let case_nd_weak := tt in _
308 | nd_copy h => let case_nd_copy := tt in _
309 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
310 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
311 | nd_rule _ _ rule => let case_nd_rule := tt in _
312 | nd_cancell _ => let case_nd_cancell := tt in _
313 | nd_cancelr _ => let case_nd_cancelr := tt in _
314 | nd_llecnac _ => let case_nd_llecnac := tt in _
315 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
316 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
317 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
318 end) (refl_equal _) (refl_equal _)
320 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
321 destruct case_nd_id0. apply nd_id0.
322 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
323 destruct case_nd_weak. apply nd_weak.
325 destruct case_nd_copy.
327 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
334 destruct case_nd_prod.
336 apply (append_brak _ _ lpf).
337 apply (append_brak _ _ rpf).
339 destruct case_nd_comp.
340 apply append_brak in bot.
341 apply (nd_comp top bot).
343 destruct case_nd_cancell.
344 eapply nd_comp; [ apply nd_cancell | idtac ].
345 apply append_brak_to_id.
347 destruct case_nd_cancelr.
348 eapply nd_comp; [ apply nd_cancelr | idtac ].
349 apply append_brak_to_id.
351 destruct case_nd_llecnac.
352 eapply nd_comp; [ idtac | apply nd_llecnac ].
353 apply append_brak_to_id.
355 destruct case_nd_rlecnac.
356 eapply nd_comp; [ idtac | apply nd_rlecnac ].
357 apply append_brak_to_id.
359 destruct case_nd_assoc.
360 eapply nd_comp; [ apply nd_assoc | idtac ].
361 repeat rewrite fixit.
362 apply append_brak_to_id.
364 destruct case_nd_cossa.
365 eapply nd_comp; [ idtac | apply nd_cossa ].
366 repeat rewrite fixit.
367 apply append_brak_to_id.
369 destruct case_nd_rule
375 Definition append_brak {h c} : forall
377 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
380 (fixify Γ past (EscBrak_Functor_Fobj h))
385 End HaskProofCategory.