src/HaskProof.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProof:                                                                                                                    *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term.  Proofs use explicit structural rules (Gentzen-style)    *)
   5 (*    and are in System FC extended with modal types indexed by Taha-Nielsen environment classifiers (λ^α)                       *)
   6 (*                                                                                                                               *)
   7 (*********************************************************************************************************************************)
   8
   9 Generalizable All Variables.
  10 Require Import Preamble.
  11 Require Import General.
  12 Require Import NaturalDeduction.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskLiterals.
  18 Require Import HaskTyCons.
  19 Require Import HaskStrongTypes.
  20 Require Import HaskWeakVars.
  21
  22 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  23  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
  24  * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
  25  * in environment T1.  This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
  26  * types *)
  27 Inductive Judg  :=
  28   mkJudg :
  29   forall Γ:TypeEnv,
  30   forall Δ:CoercionEnv Γ,
  31   Tree ??(LeveledHaskType Γ ★) ->
  32   Tree ??(HaskType Γ ★) ->
  33   HaskLevel Γ ->
  34   Judg.
  35   Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50).
  36
  37 (* information needed to define a case branch in a HaskProof *)
  38 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
  39 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
  40 ; pcb_judg           := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
  41                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
  42                   (vec2list (sac_types sac Γ avars))))
  43                 |- [weakT' branchtype ] @ weakL' lev
  44 }.
  45 Implicit Arguments ProofCaseBranch [ ].
  46
  47 (* Figure 3, production $\vdash_E$, Uniform rules *)
  48 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
  49 | RId     : forall a        ,                Arrange           a                  a
  50 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
  51 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
  52 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
  53 | RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
  54 | RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
  55 | RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
  56 | RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
  57 | RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
  58 | RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
  59 | RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
  60 | RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
  61 | RComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
  62 .
  63
  64 (* Figure 3, production $\vdash_E$, all rules *)
  65 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
  66
  67 | RArrange  : ∀ Γ Δ Σ₁ Σ₂ Σ l,       Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁     |- Σ            @l]   [Γ > Δ > Σ₂    |- Σ            @l]
  68
  69 (* λ^α rules *)
  70 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t]@(v::l)     ]   [Γ > Δ > Σ     |- [<[v|-t]>   ] @l]
  71 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ     |- [<[v|-t]>   ] @l]   [Γ > Δ > Σ     |- [t]@(v::l)      ]
  72
  73 (* Part of GHC, but not explicitly in System FC *)
  74 | RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule [Γ > Δ > Σ      |- [τ        ]  @l]   [Γ > Δ > Σ     |- [τ          ] @l]
  75 | RLit    : ∀ Γ Δ v       l,                          Rule [                                 ]   [Γ > Δ > []|- [literalType v ]  @l]
  76
  77 (* SystemFC rules *)
  78 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          ] @l]
  79 | RGlobal : forall Γ Δ l   (g:Global Γ) v,            Rule [                                 ]   [Γ>Δ>     []   |- [g v        ] @l]
  80 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te]         @l]   [Γ>Δ>    Σ     |- [tx--->te   ] @l]
  81 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
  82                    HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁]         @l]   [Γ>Δ>    Σ     |- [σ₂         ] @l]
  83
  84 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l,   Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂       @l ]
  85
  86 (* order is important here; we want to be able to skolemize without introducing new RExch'es *)
  87 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l])  [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
  88
  89 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
  90 | RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
  91
  92 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
  93
  94 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]
  95 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  96   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
  97        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   ]@l]
  98
  99 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
 100     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ>    Σ     |- [σ        ]@l]
 101 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
 102    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
 103         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
 104
 105 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
 106 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 107   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
 108                    Rule
 109                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
 110                         [Γ > Δ >                                              Σ |- [ caseType tc avars  ] @lev])
 111                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
 112 .
 113
 114
 115 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 116 (* TODO: change this to (if RBrak/REsc -> False) *)
 117 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 118 | Flat_RArrange         : ∀ Γ Δ  h c r          a l ,  Rule_Flat (RArrange Γ Δ h c r a l)
 119 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 120 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 121 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 122 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 123 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 124 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 125 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 126 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 127 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 128 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 129 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 130 | Flat_RJoin    : ∀ q a b c d e l,  Rule_Flat (RJoin q a b c d e l)
 131 | Flat_RVoid      : ∀ q a                  l,  Rule_Flat (RVoid q a l)
 132 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 133 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 134
 135 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 136   intros.
 137   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 138   Qed.
 139
 140 Lemma no_rules_with_multiple_conclusions : forall c h,
 141   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 142   intros.
 143   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 144     try apply no_urules_with_empty_conclusion in u; try apply u.
 145     destruct X0; destruct s; inversion e.
 146     auto.
 147     destruct X0; destruct s; inversion e.
 148     destruct X0; destruct s; inversion e.
 149     destruct X0; destruct s; inversion e.
 150     destruct X0; destruct s; inversion e.
 151     destruct X0; destruct s; inversion e.
 152     destruct X0; destruct s; inversion e.
 153     destruct X0; destruct s; inversion e.
 154     destruct X0; destruct s; inversion e.
 155     destruct X0; destruct s; inversion e.
 156     destruct X0; destruct s; inversion e.
 157     destruct X0; destruct s; inversion e.
 158     destruct X0; destruct s; inversion e.
 159     destruct X0; destruct s; inversion e.
 160     destruct X0; destruct s; inversion e.
 161     destruct X0; destruct s; inversion e.
 162     destruct X0; destruct s; inversion e.
 163     destruct X0; destruct s; inversion e.
 164     destruct X0; destruct s; inversion e.
 165     destruct X0; destruct s; inversion e.
 166     Qed.
 167
 168 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 169   intros.
 170   eapply no_rules_with_multiple_conclusions.
 171   apply r.
 172   exists c1.
 173   exists c2.
 174   auto.
 175   Qed.
 176
 177 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
 178 Definition arrangeMap :
 179   forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
 180     Arrange Σ₁ Σ₂ ->
 181     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
 182   intros.
 183   induction X; simpl.
 184   apply RId.
 185   apply RCanL.
 186   apply RCanR.
 187   apply RuCanL.
 188   apply RuCanR.
 189   apply RAssoc.
 190   apply RCossa.
 191   apply RExch.
 192   apply RWeak.
 193   apply RCont.
 194   apply RLeft; auto.
 195   apply RRight; auto.
 196   eapply RComp; [ apply IHX1 | apply IHX2 ].
 197   Defined.
 198
 199 (* a frequently-used Arrange *)
 200 Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
 201   Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
 202   eapply RComp.
 203   apply RCossa.
 204   eapply RComp.
 205   eapply RLeft.
 206   eapply RComp.
 207   eapply RAssoc.
 208   eapply RRight.
 209   apply RExch.
 210   eapply RComp.
 211   eapply RLeft.
 212   eapply RCossa.
 213   eapply RAssoc.
 214   Defined.