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 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
  86
  87 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
  88
  89 | RVoid    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
  90
  91 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
  92 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  93   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
  94        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
  95
  96 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
  97     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
  98 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
  99    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
 100         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 101
 102 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 103 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 104   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
 105                    Rule
 106                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
 107                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
 108                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 109 .
 110
 111
 112 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 113 (* TODO: change this to (if RBrak/REsc -> False) *)
 114 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 115 | Flat_RArrange         : ∀ Γ Δ  h c r          a ,  Rule_Flat (RArrange Γ Δ h c r a)
 116 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 117 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 118 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 119 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 120 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 121 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 122 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 123 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 124 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 125 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 126 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 127 | Flat_RJoin    : ∀ q a b c d e ,  Rule_Flat (RJoin q a b c d e)
 128 | Flat_RVoid      : ∀ q a                  ,  Rule_Flat (RVoid q a)
 129 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 130 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 131
 132 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 133   intros.
 134   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 135   Qed.
 136
 137 Lemma no_rules_with_multiple_conclusions : forall c h,
 138   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 139   intros.
 140   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 141     try apply no_urules_with_empty_conclusion in u; try apply u.
 142     destruct X0; destruct s; inversion e.
 143     auto.
 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     destruct X0; destruct s; inversion e.
 161     destruct X0; destruct s; inversion e.
 162     Qed.
 163
 164 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 165   intros.
 166   eapply no_rules_with_multiple_conclusions.
 167   apply r.
 168   exists c1.
 169   exists c2.
 170   auto.
 171   Qed.
 172
 173 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
 174 Definition arrangeMap :
 175   forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
 176     Arrange Σ₁ Σ₂ ->
 177     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
 178   intros.
 179   induction X; simpl.
 180   apply RId.
 181   apply RCanL.
 182   apply RCanR.
 183   apply RuCanL.
 184   apply RuCanR.
 185   apply RAssoc.
 186   apply RCossa.
 187   apply RExch.
 188   apply RWeak.
 189   apply RCont.
 190   apply RLeft; auto.
 191   apply RRight; auto.
 192   eapply RComp; [ apply IHX1 | apply IHX2 ].
 193   Defined.
 194
 195 (* a frequently-used Arrange *)
 196 Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
 197   Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
 198   eapply RComp.
 199   apply RCossa.
 200   eapply RComp.
 201   eapply RLeft.
 202   eapply RComp.
 203   eapply RAssoc.
 204   eapply RRight.
 205   apply RExch.
 206   eapply RComp.
 207   eapply RLeft.
 208   eapply RCossa.
 209   eapply RAssoc.
 210   Defined.