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