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}{sac:@StrongAltCon tc} :=
  54 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
  55 ; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
  56                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
  57                   (vec2list (sac_types sac Γ 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   : ∀ Γ Δ Σ τ l,          Note ->             Rule  [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
  89 | RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
  90
  91 (* SystemFC rules *)
  92 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
  93 | RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
  94 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
  95 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
  96 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
  97  Rule [Γ>Δ> Σ         |- [σ₁@@l]         ]   [Γ>Δ>    Σ     |- [σ₂          @@l]]
  98 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
  99 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 100 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 101 | REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
 102 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
 103 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
 104   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
 105        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
 106 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
 107     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
 108 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
 109    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
 110         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 111 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 112 | RCase          : forall Γ Δ lev tc Σ avars tbranches
 113   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
 114                    Rule
 115                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
 116                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
 117                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 118 .
 119 Coercion RURule : URule >-> Rule.
 120
 121
 122 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 123 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 124 | Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
 125 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 126 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 127 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 128 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 129 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
 130 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 131 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 132 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 133 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 134 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 135 | Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
 136 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
 137
 138 (* given a proof that uses only uniform rules, we can produce a general proof *)
 139 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
 140   := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
 141
 142 Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
 143   intro.
 144   intro.
 145   induction 1; intros; inversion H.
 146   simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
 147   simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
 148   Qed.
 149
 150 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
 151   intros.
 152   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 153   apply no_urules_with_empty_conclusion in u.
 154   apply u.
 155   auto.
 156   Qed.
 157
 158 Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
 159   @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
 160   intro.
 161   intro.
 162   induction 1; intros.
 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   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 169
 170   apply IHX.
 171   destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
 172     inversion e.
 173     inversion e.
 174     exists c1. exists c2. auto.
 175
 176   apply IHX.
 177   destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
 178     inversion e.
 179     inversion e.
 180     exists c1. exists c2. auto.
 181
 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   inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 185   Qed.
 186
 187 Lemma no_rules_with_multiple_conclusions : forall c h,
 188   Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
 189   intros.
 190   destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
 191     try apply no_urules_with_empty_conclusion in u; try apply u.
 192     destruct X0; destruct s; inversion e.
 193     auto.
 194     apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto.
 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     destruct X0; destruct s; inversion e.
 212     destruct X0; destruct s; inversion e.
 213     Qed.
 214
 215 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
 216   intros.
 217   eapply no_rules_with_multiple_conclusions.
 218   apply r.
 219   exists c1.
 220   exists c2.
 221   auto.
 222   Qed.
 223
 224