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 | RCut           : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
  72 | RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
  73 | RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
  74
  75 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
  76
  77 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]
  78 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
  79   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
  80        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   ]@l]
  81
  82 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
  83     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ>    Σ     |- [σ        ]@l]
  84 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
  85    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
  86         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
  87
  88 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
  89 | RCase          : forall Γ Δ lev tc Σ avars tbranches
  90   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
  91                    Rule
  92                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
  93                         [Γ > Δ >                                              Σ |- [ caseType tc avars  ] @lev])
  94                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
  95 .
  96
  97 Definition RCut'  : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
  98   ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
  99   intros.
 100   eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 101   eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
 102   apply nd_prod.
 103   apply nd_id.
 104   apply nd_rule.
 105   apply RArrange.
 106   apply AuCanL.
 107   Defined.
 108
 109 Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,
 110   ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l].
 111   intros.
 112   eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 113   eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
 114   apply nd_prod.
 115   apply nd_id.
 116   eapply nd_rule; eapply RArrange; eapply AuCanL.
 117   Defined.
 118
 119 Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,
 120   ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l].
 121   intros.
 122   eapply nd_comp; [ apply nd_exch | idtac ].
 123   eapply nd_rule; eapply RCut.
 124   Defined.
 125
 126 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 127 (* TODO: change this to (if RBrak/REsc -> False) *)
 128 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 129 | Flat_RArrange         : ∀ Γ Δ  h c r          a l ,  Rule_Flat (RArrange Γ Δ h c r a l)
 130 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 131 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 132 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 133 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 134 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 135 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 136 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 137 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 138 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 139 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 140 | Flat_RVoid      : ∀ q a                  l,  Rule_Flat (RVoid q a l)
 141 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 142 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 143
 144 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 145   intros.
 146   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 147   Qed.
 148
 149 Lemma no_rules_with_multiple_conclusions : forall c h,
 150   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 151   intros.
 152   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 153     try apply no_urules_with_empty_conclusion in u; try apply u.
 154     destruct X0; destruct s; inversion e.
 155     auto.
 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     destruct X0; destruct s; inversion e.
 166     destruct X0; destruct s; inversion e.
 167     destruct X0; destruct s; inversion e.
 168     destruct X0; destruct s; inversion e.
 169     destruct X0; destruct s; inversion e.
 170     destruct X0; destruct s; inversion e.
 171     destruct X0; destruct s; inversion e.
 172     destruct X0; destruct s; inversion e.
 173     destruct X0; destruct s; inversion e.
 174     destruct X0; destruct s; inversion e.
 175     Qed.
 176
 177 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 178   intros.
 179   eapply no_rules_with_multiple_conclusions.
 180   apply r.
 181   exists c1.
 182   exists c2.
 183   auto.
 184   Qed.
 185