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 HaskLiteralsAndTyCons.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskWeakVars.
  20
  21 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  22  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
  23  * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
  24  * in environment T1.  This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
  25  * types *)
  26 Inductive Judg  :=
  27   mkJudg :
  28   forall Γ:TypeEnv,
  29   forall Δ:CoercionEnv Γ,
  30   Tree ??(LeveledHaskType Γ ★) ->
  31   Tree ??(LeveledHaskType Γ ★) ->
  32   Judg.
  33   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
  34
  35 (* information needed to define a case branch in a HaskProof *)
  36 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
  37 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
  38 ; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
  39                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
  40                   (vec2list (sac_types sac Γ avars))))
  41                 |- [weakLT' (branchtype @@ lev)]
  42 }.
  43 Implicit Arguments ProofCaseBranch [ ].
  44
  45 (* Figure 3, production $\vdash_E$, Uniform rules *)
  46 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
  47 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
  48 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
  49 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
  50 | RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
  51 | RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
  52 | RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
  53 | RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
  54 | RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
  55 | RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
  56 | RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
  57 | RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
  58 | RComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
  59 .
  60
  61 (* Figure 3, production $\vdash_E$, all rules *)
  62 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
  63
  64 | RArrange  : ∀ Γ Δ Σ₁ Σ₂ Σ,         Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁     |- Σ              ]   [Γ > Δ > Σ₂    |- Σ              ]
  65
  66 (* λ^α rules *)
  67 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
  68 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t    @@ (v::l)]]
  69
  70 (* Part of GHC, but not explicitly in System FC *)
  71 | RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule [Γ > Δ > Σ      |- [τ        @@ l]]   [Γ > Δ > Σ     |- [τ          @@l]]
  72 | RLit    : ∀ Γ Δ v       l,                          Rule [                                 ]   [Γ > Δ > []|- [literalType v  @@l]]
  73
  74 (* SystemFC rules *)
  75 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
  76 | RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
  77 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
  78 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
  79                    HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁@@l]        ]   [Γ>Δ>    Σ     |- [σ₂         @@l]]
  80
  81 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
  82
  83 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
  84
  85 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
  86
  87 | RVoid    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
  88
  89 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
  90 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  91   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
  92        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
  93
  94 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
  95     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
  96 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
  97    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
  98         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
  99
 100 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 101 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 102   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
 103                    Rule
 104                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
 105                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
 106                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 107 .
 108
 109
 110 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 111 (* TODO: change this to (if RBrak/REsc -> False) *)
 112 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 113 | Flat_RArrange         : ∀ Γ Δ  h c r          a ,  Rule_Flat (RArrange Γ Δ h c r a)
 114 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 115 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 116 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 117 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 118 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 119 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 120 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 121 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 122 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 123 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 124 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 125 | Flat_RJoin    : ∀ q a b c d e ,  Rule_Flat (RJoin q a b c d e)
 126 | Flat_RVoid      : ∀ q a                  ,  Rule_Flat (RVoid q a)
 127 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 128 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 129
 130 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 131   intros.
 132   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 133   Qed.
 134
 135 Lemma no_rules_with_multiple_conclusions : forall c h,
 136   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 137   intros.
 138   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 139     try apply no_urules_with_empty_conclusion in u; try apply u.
 140     destruct X0; destruct s; inversion e.
 141     auto.
 142     destruct X0; destruct s; inversion e.
 143     destruct X0; destruct s; inversion e.
 144     destruct X0; destruct s; inversion e.
 145     destruct X0; destruct s; inversion e.
 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     Qed.
 161
 162 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 163   intros.
 164   eapply no_rules_with_multiple_conclusions.
 165   apply r.
 166   exists c1.
 167   exists c2.
 168   auto.
 169   Qed.
 170
 171