src/HaskProofCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofCategory:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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.
  21
  22 Section HaskProofCategory.
  23 (*
  24
  25   Context (flat_dynamic_semantics : @ND_Relation _ Rule).
  26   Context (ml_dynamic_semantics   : @ND_Relation _ Rule).
  27
  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).
  33
  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))
  46         (ob2judgment past).
  47
  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).
  58
  59     Section EscBrak_Functor.
  60       Context
  61         (past:@Past V)
  62         (n:V)
  63         (Σ₁:Tree ??(@LeveledHaskType V)).
  64
  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 ]>])).
  69
  70       Definition append_brak
  71       : forall {c}, ND_ML
  72           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        c )
  73           (mapOptionTree (ob2judgment                   past )  (EscBrak_Functor_Fobj c)).
  74         intros.
  75         unfold ND_ML.
  76         unfold EscBrak_Functor_Fobj.
  77         rewrite mapOptionTree_comp.
  78         simpl in *.
  79         apply nd_replicate.
  80         intro o; destruct o.
  81         apply nd_rule.
  82         apply MLRBrak.
  83         Defined.
  84
  85       Definition prepend_esc
  86       : forall {h}, ND_ML
  87           (mapOptionTree (ob2judgment                  past )  (EscBrak_Functor_Fobj h))
  88           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        h ).
  89         intros.
  90         unfold ND_ML.
  91         unfold EscBrak_Functor_Fobj.
  92         rewrite mapOptionTree_comp.
  93         simpl in *.
  94         apply nd_replicate.
  95         intro o; destruct o.
  96         apply nd_rule.
  97         apply MLREsc.
  98         Defined.
  99
 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).
 103         intros.
 104         eapply nd_comp.
 105         apply prepend_esc.
 106         eapply nd_comp.
 107         eapply Flat_to_ML.
 108         apply f.
 109         apply append_brak.
 110         Defined.
 111
 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))).
 115          admit.
 116          Qed.
 117
 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)).
 121          admit.
 122          Qed.
 123
 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.
 130           auto.
 131         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 132           set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
 133           setoid_rewrite 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.
 143           clear q.
 144           set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
 145           setoid_rewrite q.
 146           reflexivity.
 147         Defined.
 148
 149     End EscBrak_Functor.
 150
 151
 152
 153   Ltac rule_helper_tactic' :=
 154     match goal with
 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
 170     end.
 171
 172   Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
 173     admit.
 174     Defined.
 175
 176   Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
 177     admit.
 178     Qed.
 179
 180   Definition append_brak_to_id : forall {c},
 181   @ND_FC V
 182       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
 183       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 184   admit.
 185   Defined.
 186
 187   Definition append_brak : forall {h c}
 188     (pf:@ND_FC V
 189       h
 190       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
 191     @ND_FC V
 192        h
 193       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 194
 195       refine (fix append_brak h c nd {struct nd} :=
 196        ((match nd
 197             as nd'
 198             in @ND _ _ H C
 199             return
 200             (H=h) ->
 201             (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
 202             ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
 203           with
 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 _)
 218        ));
 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.
 223
 224        destruct case_nd_copy.
 225          (*
 226          destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
 227          inversion H0; subst.
 228          simpl.*)
 229          idtac.
 230          clear H0.
 231          admit.
 232
 233        destruct case_nd_prod.
 234          eapply nd_prod.
 235          apply (append_brak _ _ lpf).
 236          apply (append_brak _ _ rpf).
 237
 238        destruct case_nd_comp.
 239          apply append_brak in bot.
 240          apply (nd_comp top bot).
 241
 242        destruct case_nd_cancell.
 243          eapply nd_comp; [ apply nd_cancell | idtac ].
 244          apply append_brak_to_id.
 245
 246        destruct case_nd_cancelr.
 247          eapply nd_comp; [ apply nd_cancelr | idtac ].
 248          apply append_brak_to_id.
 249
 250        destruct case_nd_llecnac.
 251          eapply nd_comp; [ idtac | apply nd_llecnac ].
 252          apply append_brak_to_id.
 253
 254        destruct case_nd_rlecnac.
 255          eapply nd_comp; [ idtac | apply nd_rlecnac ].
 256          apply append_brak_to_id.
 257
 258        destruct case_nd_assoc.
 259          eapply nd_comp; [ apply nd_assoc | idtac ].
 260          repeat rewrite fixit.
 261          apply append_brak_to_id.
 262
 263        destruct case_nd_cossa.
 264          eapply nd_comp; [ idtac | apply nd_cossa ].
 265          repeat rewrite fixit.
 266          apply append_brak_to_id.
 267
 268        destruct case_nd_rule
 269
 270
 271
 272     Defined.
 273
 274   Definition append_brak {h c} : forall
 275       pf:@ND_FC V
 276         (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
 277         c,
 278       @ND_FC V
 279         (fixify Γ                past  (EscBrak_Functor_Fobj h))
 280         c.
 281     admit.
 282     Defined.
 283 *)
 284 End HaskProofCategory.