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