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 (* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
  36  * uniform context throughout the whole proof.  Such proofs are important because (1) we can do left and right context
  37  * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
  38 Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
  39   mkUJudg :
  40   Tree ??(LeveledHaskType Γ ★) ->
  41   Tree ??(LeveledHaskType Γ ★) ->
  42   UJudg Γ Δ.
  43   Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
  44   Definition ext_tree_left  {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
  45   Definition ext_tree_right {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
  46
  47 (* we can turn a UJudg into a Judg by simply internalizing the index *)
  48 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
  49   match ej with mkUJudg t s => Γ > Δ > t |- s end.
  50   Coercion UJudg2judg : UJudg >-> Judg.
  51
  52 (* information needed to define a case branch in a HaskProof *)
  53 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars} :=
  54 { pcb_scb            :  @StrongAltCon tc
  55 ; pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
  56 ; pcb_judg           := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ)
  57                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
  58                   (vec2list (sac_types pcb_scb Γ avars))))
  59                 |- [weakLT' (branchtype @@ lev)]
  60 }.
  61 Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.
  62 Implicit Arguments ProofCaseBranch [ ].
  63
  64 (* Figure 3, production $\vdash_E$, Uniform rules *)
  65 Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
  66 | RCanL   : ∀ t a        ,                          URule  [Γ>>Δ>    [],,a   |- t         ]      [Γ>>Δ>       a   |- t           ]
  67 | RCanR   : ∀ t a        ,                          URule  [Γ>>Δ>    a,,[]   |- t         ]      [Γ>>Δ>       a   |- t           ]
  68 | RuCanL  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  [],,a    |- t           ]
  69 | RuCanR  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  a,,[]    |- t           ]
  70 | RAssoc  : ∀ t a b c    ,                          URule  [Γ>>Δ>a,,(b,,c)   |- t         ]      [Γ>>Δ>(a,,b),,c  |- t           ]
  71 | RCossa  : ∀ t a b c    ,                          URule  [Γ>>Δ>(a,,b),,c   |- t         ]      [Γ>>Δ> a,,(b,,c) |- t           ]
  72 | RLeft   : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_left  x) h) (mapOptionTree (ext_tree_left  x) c)
  73 | RRight  : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
  74 | RExch   : ∀ t a b      ,                          URule  [Γ>>Δ>   (b,,a)   |- t         ]      [Γ>>Δ>  (a,,b)   |- t           ]
  75 | RWeak   : ∀ t a        ,                          URule  [Γ>>Δ>       []   |- t         ]      [Γ>>Δ>       a   |- t           ]
  76 | RCont   : ∀ t a        ,                          URule  [Γ>>Δ>  (a,,a)    |- t         ]      [Γ>>Δ>       a   |- t           ].
  77
  78
  79 (* Figure 3, production $\vdash_E$, all rules *)
  80 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
  81
  82 | RURule  : ∀ Γ Δ h c,                  @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
  83
  84 (* λ^α rules *)
  85 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
  86 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t  @@ (v::l)  ]]
  87
  88 (* Part of GHC, but not explicitly in System FC *)
  89 | RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule  [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
  90 | RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
  91
  92 (* SystemFC rules *)
  93 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
  94 | RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
  95 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
  96 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
  97 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
  98  Rule [Γ>Δ> Σ         |- [σ₁@@l]         ]   [Γ>Δ>    Σ     |- [σ₂          @@l]]
  99 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 100 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 101 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 102 | REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
 103 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
 104 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
 105   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
 106        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
 107 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
 108     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
 109 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
 110    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
 111         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 112 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ]
 113 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 114   (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
 115                    Rule
 116                        ((mapOptionTree pcb_judg alts),,
 117                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
 118                         [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
 119 .
 120 Coercion RURule : URule >-> Rule.
 121
 122
 123 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 124 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 125 | Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
 126 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 127 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 128 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 129 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 130 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 131 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 132 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 133 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 134 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 135 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 136 | Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
 137 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
 138
 139 (* given a proof that uses only uniform rules, we can produce a general proof *)
 140 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
 141   := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
 142
 143 Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
 144   intro.
 145   intro.
 146   induction 1; intros; inversion H.
 147   simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
 148   simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
 149   Qed.
 150
 151 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 152   intros.
 153   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 154   apply no_urules_with_empty_conclusion in u.
 155   apply u.
 156   auto.
 157   Qed.
 158
 159 Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
 160   @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
 161   intro.
 162   intro.
 163   induction 1; intros.
 164   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 165   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 166   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 167   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 168   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 169   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 170
 171   apply IHX.
 172   destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
 173     inversion e.
 174     inversion e.
 175     exists c1. exists c2. auto.
 176
 177   apply IHX.
 178   destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
 179     inversion e.
 180     inversion e.
 181     exists c1. exists c2. auto.
 182
 183   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 184   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 185   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 186   Qed.
 187
 188 Lemma no_rules_with_multiple_conclusions : forall c h,
 189   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 190   intros.
 191   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 192     try apply no_urules_with_empty_conclusion in u; try apply u.
 193     destruct X0; destruct s; inversion e.
 194     auto.
 195     apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto.
 196     destruct X0; destruct s; inversion e.
 197     destruct X0; destruct s; inversion e.
 198     destruct X0; destruct s; inversion e.
 199     destruct X0; destruct s; inversion e.
 200     destruct X0; destruct s; inversion e.
 201     destruct X0; destruct s; inversion e.
 202     destruct X0; destruct s; inversion e.
 203     destruct X0; destruct s; inversion e.
 204     destruct X0; destruct s; inversion e.
 205     destruct X0; destruct s; inversion e.
 206     destruct X0; destruct s; inversion e.
 207     destruct X0; destruct s; inversion e.
 208     destruct X0; destruct s; inversion e.
 209     destruct X0; destruct s; inversion e.
 210     destruct X0; destruct s; inversion e.
 211     destruct X0; destruct s; inversion e.
 212     destruct X0; destruct s; inversion e.
 213     destruct X0; destruct s; inversion e.
 214     Qed.
 215
 216 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 217   intros.
 218   eapply no_rules_with_multiple_conclusions.
 219   apply r.
 220   exists c1.
 221   exists c2.
 222   auto.
 223   Qed.
 224
 225