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