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.
14 Require Import HaskKinds.
15 Require Import HaskCoreTypes.
16 Require Import HaskLiteralsAndTyCons.
17 Require Import HaskStrongTypes.
18 Require Import HaskProof.
19 Require Import NaturalDeduction.
20 Require Import NaturalDeductionCategory.
22 Section HaskProofCategory.
25 Context (flat_dynamic_semantics : @ND_Relation _ Rule).
26 Context (ml_dynamic_semantics : @ND_Relation _ Rule).
28 Section SystemFC_Category.
29 Context (encodeTypeTree_reduce : @LeveledHaskType V -> @LeveledHaskType V -> @LeveledHaskType V).
30 Context (encodeTypeTree_empty : @LeveledHaskType V).
31 Context (encodeTypeTree_flat_empty : @CoreType V).
32 Context (encodeTypeTree_flat_reduce : @CoreType V -> @CoreType V -> @CoreType V).
34 Definition encodeTypeTree :=
35 @treeReduce _ _ (fun x => match x with None => encodeTypeTree_empty | Some q => q end) encodeTypeTree_reduce.
36 Definition encodeTypeTree_flat :=
37 @treeReduce _ _ (fun x => match x with None => encodeTypeTree_flat_empty | Some q => q end) encodeTypeTree_flat_reduce.
38 (* the full category of judgments *)
39 Definition ob2judgment past :=
40 fun q:Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V) =>
41 let (a,s):=q in (Γ > past : a |- (encodeTypeTree s) ).
42 Definition SystemFC_Cat past :=
43 @Judgments_Category_monoidal _ Rule
44 (@ml_dynamic_semantics V)
45 (Tree ??(@LeveledHaskType V) * Tree ??(@LeveledHaskType V))
48 (* the category of judgments with no variables or succedents in the "future" –- still may have code types *)
49 (* technically this should be a subcategory of SystemFC_Cat *)
50 Definition ob2judgment_flat past :=
51 fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
52 let (a,s):=q in (Γ > past : ``a |- `(encodeTypeTree_flat s) ).
53 Definition SystemFC_Cat_Flat past :=
54 @Judgments_Category_monoidal _ Rule
55 (@flat_dynamic_semantics V)
56 (Tree ??(@CoreType V) * Tree ??(@CoreType V))
57 (ob2judgment_flat past).
59 Section EscBrak_Functor.
63 (Σ₁:Tree ??(@LeveledHaskType V)).
65 Definition EscBrak_Functor_Fobj
66 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
67 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
68 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
70 Definition append_brak
72 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
73 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
76 unfold EscBrak_Functor_Fobj.
77 rewrite mapOptionTree_comp.
85 Definition prepend_esc
87 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
88 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
91 unfold EscBrak_Functor_Fobj.
92 rewrite mapOptionTree_comp.
100 Definition EscBrak_Functor_Fmor
101 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
102 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
112 Lemma esc_then_brak_is_id : forall a,
113 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
114 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
118 Lemma brak_then_esc_is_id : forall a,
119 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
120 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
124 Instance EscBrak_Functor
125 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
126 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
127 intros; unfold EscBrak_Functor_Fmor; simpl in *.
128 apply ndr_comp_respects; try reflexivity.
129 apply ndr_comp_respects; try reflexivity.
131 intros; unfold EscBrak_Functor_Fmor; simpl in *.
132 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
134 apply esc_then_brak_is_id.
135 intros; unfold EscBrak_Functor_Fmor; simpl in *.
136 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
137 repeat setoid_rewrite q.
138 apply ndr_comp_respects; try reflexivity.
139 apply ndr_comp_respects; try reflexivity.
140 repeat setoid_rewrite <- q.
141 apply ndr_comp_respects; try reflexivity.
142 setoid_rewrite brak_then_esc_is_id.
144 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
153 Ltac rule_helper_tactic' :=
155 | [ H : ?A = ?A |- _ ] => clear H
156 | [ H : [?A] = [] |- _ ] => inversion H; clear H
157 | [ H : [] = [?A] |- _ ] => inversion H; clear H
158 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
159 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
160 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
161 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
162 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
163 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
164 (* | [ H : Sequent T |- _ ] => destruct H *)
165 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
166 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
167 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
168 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
169 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
172 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
176 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
180 Definition append_brak_to_id : forall {c},
182 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
183 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
187 Definition append_brak : forall {h c}
190 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
193 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
195 refine (fix append_brak h c nd {struct nd} :=
201 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
202 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
204 | nd_id0 => let case_nd_id0 := tt in _
205 | nd_id1 h => let case_nd_id1 := tt in _
206 | nd_weak h => let case_nd_weak := tt in _
207 | nd_copy h => let case_nd_copy := tt in _
208 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
209 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
210 | nd_rule _ _ rule => let case_nd_rule := tt in _
211 | nd_cancell _ => let case_nd_cancell := tt in _
212 | nd_cancelr _ => let case_nd_cancelr := tt in _
213 | nd_llecnac _ => let case_nd_llecnac := tt in _
214 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
215 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
216 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
217 end) (refl_equal _) (refl_equal _)
219 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
220 destruct case_nd_id0. apply nd_id0.
221 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
222 destruct case_nd_weak. apply nd_weak.
224 destruct case_nd_copy.
226 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
233 destruct case_nd_prod.
235 apply (append_brak _ _ lpf).
236 apply (append_brak _ _ rpf).
238 destruct case_nd_comp.
239 apply append_brak in bot.
240 apply (nd_comp top bot).
242 destruct case_nd_cancell.
243 eapply nd_comp; [ apply nd_cancell | idtac ].
244 apply append_brak_to_id.
246 destruct case_nd_cancelr.
247 eapply nd_comp; [ apply nd_cancelr | idtac ].
248 apply append_brak_to_id.
250 destruct case_nd_llecnac.
251 eapply nd_comp; [ idtac | apply nd_llecnac ].
252 apply append_brak_to_id.
254 destruct case_nd_rlecnac.
255 eapply nd_comp; [ idtac | apply nd_rlecnac ].
256 apply append_brak_to_id.
258 destruct case_nd_assoc.
259 eapply nd_comp; [ apply nd_assoc | idtac ].
260 repeat rewrite fixit.
261 apply append_brak_to_id.
263 destruct case_nd_cossa.
264 eapply nd_comp; [ idtac | apply nd_cossa ].
265 repeat rewrite fixit.
266 apply append_brak_to_id.
268 destruct case_nd_rule
274 Definition append_brak {h c} : forall
276 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
279 (fixify Γ past (EscBrak_Functor_Fobj h))
284 End HaskProofCategory.