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 HaskGeneral.
  16 Require Import HaskLiterals.
  17 Require Import HaskStrongTypes.
  18
  19 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  20  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
  21  * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
  22  * in environment T1.  This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
  23  * types *)
  24 Inductive Judg  :=
  25   mkJudg :
  26   forall Γ:TypeEnv,
  27   forall Δ:CoercionEnv Γ,
  28   Tree ??(LeveledHaskType Γ) ->
  29   Tree ??(LeveledHaskType Γ) ->
  30   Judg.
  31   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
  32
  33 (* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
  34  * uniform context throughout the whole proof.  Such proofs are important because (1) we can do left and right context
  35  * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
  36 Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
  37   mkUJudg :
  38   Tree ??(LeveledHaskType Γ) ->
  39   Tree ??(LeveledHaskType Γ) ->
  40   UJudg Γ Δ.
  41   Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
  42   Notation "'ext_tree_left'"    := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t)  s end).
  43   Notation "'ext_tree_right'"   := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end).
  44
  45 (* we can turn a UJudg into a Judg by simply internalizing the index *)
  46 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
  47   match ej with mkUJudg t s => Γ > Δ > t |- s end.
  48   Coercion UJudg2judg : UJudg >-> Judg.
  49
  50 (* information needed to define a case branch in a HaskProof *)
  51 Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} :=
  52 { cbi_cbi              :  @StrongAltConInContext n tc Γ avars
  53 ; cbri_freevars        :  Tree ??(LeveledHaskType Γ)
  54 ; cbri_judg            := cbi_Γ cbi_cbi > cbi_Δ  cbi_cbi
  55                           > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi)))
  56                           |- [weakLT' (branchtype @@ lev)]
  57 }.
  58 Implicit Arguments ProofCaseBranch [ ].
  59
  60 (* Figure 3, production $\vdash_E$, Uniform rules *)
  61 Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
  62 | RCanL   : ∀ t a        ,                          URule  [Γ>>Δ>    [],,a   |- t         ]      [Γ>>Δ>       a   |- t           ]
  63 | RCanR   : ∀ t a        ,                          URule  [Γ>>Δ>    a,,[]   |- t         ]      [Γ>>Δ>       a   |- t           ]
  64 | RuCanL  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  [],,a    |- t           ]
  65 | RuCanR  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  a,,[]    |- t           ]
  66 | RAssoc  : ∀ t a b c    ,                          URule  [Γ>>Δ>a,,(b,,c)   |- t         ]      [Γ>>Δ>(a,,b),,c  |- t           ]
  67 | RCossa  : ∀ t a b c    ,                          URule  [Γ>>Δ>(a,,b),,c   |- t         ]      [Γ>>Δ> a,,(b,,c) |- t           ]
  68 | RLeft   : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_left  x) h) (mapOptionTree (ext_tree_left  x) c)
  69 | RRight  : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
  70 | RExch   : ∀ t a b      ,                          URule  [Γ>>Δ>   (b,,a)   |- t         ]      [Γ>>Δ>  (a,,b)   |- t           ]
  71 | RWeak   : ∀ t a        ,                          URule  [Γ>>Δ>       []   |- t         ]      [Γ>>Δ>       a   |- t           ]
  72 | RCont   : ∀ t a        ,                          URule  [Γ>>Δ>  (a,,a)    |- t         ]      [Γ>>Δ>       a   |- t           ].
  73
  74
  75 (* Figure 3, production $\vdash_E$, all rules *)
  76 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
  77
  78 | RURule  : ∀ Γ Δ h c,                  @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
  79
  80 (* λ^α rules *)
  81 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
  82 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t  @@ (v::l)  ]]
  83
  84 (* Part of GHC, but not explicitly in System FC *)
  85 | RNote   : ∀ h c,                Note ->             Rule  h                                    [ c ]
  86 | RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
  87
  88 (* SystemFC rules *)
  89 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
  90 | RLam    : ∀ Γ Δ Σ tx te l,     Γ ⊢ᴛy tx : ★      -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
  91 | RCast   : ∀ Γ Δ Σ σ τ γ l,     Δ ⊢ᴄᴏ γ  : σ ∼ τ  -> Rule [Γ>Δ> Σ         |- [σ@@l]         ]   [Γ>Δ>    Σ     |- [τ          @@l]]
  92 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
  93 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
  94 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
  95 | REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
  96 | RAppT   : ∀ Γ Δ Σ κ σ τ l,     Γ ⊢ᴛy τ  : κ      -> Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
  97 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  98   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
  99        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
 100 | RAppCo  : forall Γ Δ Σ κ σ₁ σ₂ σ γ l,   Δ ⊢ᴄᴏ γ  : σ₁∼σ₂ ->
 101     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
 102 | RAbsCo  : ∀ Γ Δ Σ κ σ σ₁ σ₂ l,
 103    Γ ⊢ᴛy σ₁:κ ->
 104    Γ ⊢ᴛy σ₂:κ ->
 105    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
 106         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]]
 107 | RLetRec        : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
 108 | RCase          : forall Γ Δ lev n tc Σ avars tbranches
 109   (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)),
 110                    Rule
 111                        ((mapOptionTree cbri_judg alts),,
 112                         [Γ > Δ >                                               Σ |- [ caseType tc avars @@ lev ] ])
 113                         [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
 114 .
 115 Coercion RURule : URule >-> Rule.
 116
 117
 118 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 119 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 120 | Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
 121 | Flat_RNote            : ∀ x y z              ,  Rule_Flat (RNote x y z)
 122 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 123 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    l,  Rule_Flat (RLam Γ Δ  Σ tx te      q l)
 124 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q    l,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q l)
 125 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 126 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    l,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q l)
 127 | Flat_RAppCo           : ∀ Γ Δ  Σ κ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ κ σ₁ σ₂ σ γ  q l)
 128 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2 q3 x )
 129 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 130 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 131 | Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
 132 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q).
 133
 134 (* given a proof that uses only uniform rules, we can produce a general proof *)
 135 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
 136   := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
 137
 138