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 ??(LeveledHaskType Γ ★) ->
  33   Judg.
  34   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
  35
  36 (* information needed to define a case branch in a HaskProof *)
  37 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
  38 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
  39 ; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
  40                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
  41                   (vec2list (sac_types sac Γ avars))))
  42                 |- [weakLT' (branchtype @@ lev)]
  43 }.
  44 Implicit Arguments ProofCaseBranch [ ].
  45
  46 (* Figure 3, production $\vdash_E$, Uniform rules *)
  47 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
  48 | RId     : forall a        ,                Arrange           a                  a
  49 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
  50 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
  51 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
  52 | RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
  53 | RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
  54 | RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
  55 | RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
  56 | RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
  57 | RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
  58 | RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
  59 | RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
  60 | RComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
  61 .
  62
  63 (* Figure 3, production $\vdash_E$, all rules *)
  64 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
  65
  66 | RArrange  : ∀ Γ Δ Σ₁ Σ₂ Σ,         Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁     |- Σ              ]   [Γ > Δ > Σ₂    |- Σ              ]
  67
  68 (* λ^α rules *)
  69 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
  70 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t    @@ (v::l)]]
  71
  72 (* Part of GHC, but not explicitly in System FC *)
  73 | RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule [Γ > Δ > Σ      |- [τ        @@ l]]   [Γ > Δ > Σ     |- [τ          @@l]]
  74 | RLit    : ∀ Γ Δ v       l,                          Rule [                                 ]   [Γ > Δ > []|- [literalType v  @@l]]
  75
  76 (* SystemFC rules *)
  77 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
  78 | RGlobal : forall Γ Δ l   (g:Global Γ) v,            Rule [                                 ]   [Γ>Δ>     []   |- [g v        @@l]]
  79 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
  80 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
  81                    HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁@@l]        ]   [Γ>Δ>    Σ     |- [σ₂         @@l]]
  82
  83 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
  84
  85 (* order is important here; we want to be able to skolemize without introducing new RExch'es *)
  86 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
  87
  88 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   @@l]]
  89 | RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂   @@l]]
  90
  91 | RVoid    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
  92
  93 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
  94 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  95   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
  96        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
  97
  98 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
  99     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
 100 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
 101    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
 102         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 103
 104 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 105 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 106   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
 107                    Rule
 108                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
 109                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
 110                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 111 .
 112
 113
 114 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 115 (* TODO: change this to (if RBrak/REsc -> False) *)
 116 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 117 | Flat_RArrange         : ∀ Γ Δ  h c r          a ,  Rule_Flat (RArrange Γ Δ h c r a)
 118 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 119 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 120 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 121 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 122 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 123 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 124 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 125 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 126 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 127 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 128 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 129 | Flat_RJoin    : ∀ q a b c d e ,  Rule_Flat (RJoin q a b c d e)
 130 | Flat_RVoid      : ∀ q a                  ,  Rule_Flat (RVoid q a)
 131 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 132 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 133
 134 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 135   intros.
 136   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 137   Qed.
 138
 139 Lemma no_rules_with_multiple_conclusions : forall c h,
 140   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 141   intros.
 142   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 143     try apply no_urules_with_empty_conclusion in u; try apply u.
 144     destruct X0; destruct s; inversion e.
 145     auto.
 146     destruct X0; destruct s; inversion e.
 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     Qed.
 166
 167 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 168   intros.
 169   eapply no_rules_with_multiple_conclusions.
 170   apply r.
 171   exists c1.
 172   exists c2.
 173   auto.
 174   Qed.
 175
 176 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
 177 Definition arrangeMap :
 178   forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
 179     Arrange Σ₁ Σ₂ ->
 180     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
 181   intros.
 182   induction X; simpl.
 183   apply RId.
 184   apply RCanL.
 185   apply RCanR.
 186   apply RuCanL.
 187   apply RuCanR.
 188   apply RAssoc.
 189   apply RCossa.
 190   apply RExch.
 191   apply RWeak.
 192   apply RCont.
 193   apply RLeft; auto.
 194   apply RRight; auto.
 195   eapply RComp; [ apply IHX1 | apply IHX2 ].
 196   Defined.
 197
 198 (* a frequently-used Arrange *)
 199 Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
 200   Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
 201   eapply RComp.
 202   apply RCossa.
 203   eapply RComp.
 204   eapply RLeft.
 205   eapply RComp.
 206   eapply RAssoc.
 207   eapply RRight.
 208   apply RExch.
 209   eapply RComp.
 210   eapply RLeft.
 211   eapply RCossa.
 212   eapply RAssoc.
 213   Defined.