X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=7e3ef1c508b9e609cbc49a0ba6ad9fec26223889;hp=606b667723acb7cada6a7c63f2ee10d248ac29f5;hb=786b693ac8d5f2081db75b49bba838a6cff7e2f6;hpb=061af1379740c1118e42ae7c37ea294b4c2174f3

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 606b667..7e3ef1c 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -12,9 +12,11 @@ Require Import General.
 Require Import NaturalDeduction.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
 
 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
@@ -25,8 +27,8 @@ Inductive Judg  :=
   mkJudg :
   forall Γ:TypeEnv,
   forall Δ:CoercionEnv Γ,
-  Tree ??(LeveledHaskType Γ) ->
-  Tree ??(LeveledHaskType Γ) ->
+  Tree ??(LeveledHaskType Γ ★) ->
+  Tree ??(LeveledHaskType Γ ★) ->
   Judg.
   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
 
@@ -35,12 +37,12 @@ Inductive Judg  :=
  * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
 Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
   mkUJudg :
-  Tree ??(LeveledHaskType Γ) ->
-  Tree ??(LeveledHaskType Γ) ->
+  Tree ??(LeveledHaskType Γ ★) ->
+  Tree ??(LeveledHaskType Γ ★) ->
   UJudg Γ Δ.
   Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
-  Notation "'ext_tree_left'"    := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t)  s end).
-  Notation "'ext_tree_right'"   := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end).
+  Definition ext_tree_left  {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
+  Definition ext_tree_right {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
 
 (* we can turn a UJudg into a Judg by simply internalizing the index *)
 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
@@ -48,13 +50,14 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
   Coercion UJudg2judg : UJudg >-> Judg.
 
 (* information needed to define a case branch in a HaskProof *)
-Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} :=
-{ cbi_cbi              :  @StrongAltConInContext n tc Γ avars
-; cbri_freevars        :  Tree ??(LeveledHaskType Γ)
-; cbri_judg            := cbi_Γ cbi_cbi > cbi_Δ  cbi_cbi
-                          > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi)))
-                          |- [weakLT' (branchtype @@ lev)]
+Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
+{ pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
+; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
+                > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
+                  (vec2list (sac_types sac Γ avars))))
+                |- [weakLT' (branchtype @@ lev)]
 }.
+(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
 Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
@@ -82,35 +85,36 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t  @@ (v::l)  ]]
 
 (* Part of GHC, but not explicitly in System FC *)
-| RNote   : ∀ h c,                Note ->             Rule  h                                    [ c ]
+| RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule  [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
 | RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
 
 (* SystemFC rules *)
 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
-| RLam    : ∀ Γ Δ Σ tx te l,     Γ ⊢ᴛy tx : ★      -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
-| RCast   : ∀ Γ Δ Σ σ τ γ l,     Δ ⊢ᴄᴏ γ  : σ ∼ τ  -> Rule [Γ>Δ> Σ         |- [σ@@l]         ]   [Γ>Δ>    Σ     |- [τ          @@l]]
+| RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
+| RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
+| RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
+HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
+ Rule [Γ>Δ> Σ         |- [σ₁@@l]         ]   [Γ>Δ>    Σ     |- [σ₂          @@l]]
 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 | REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
-| RAppT   : ∀ Γ Δ Σ κ σ τ l,     Γ ⊢ᴛy τ  : κ      -> Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
+| RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
-| RAppCo  : forall Γ Δ Σ κ σ₁ σ₂ σ γ l,   Δ ⊢ᴄᴏ γ  : σ₁∼σ₂ ->
-    Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂:κ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
-| RAbsCo  : ∀ Γ Δ Σ κ σ σ₁ σ₂ l,
-   Γ ⊢ᴛy σ₁:κ ->
-   Γ ⊢ᴛy σ₂:κ ->
+| RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
+    Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
+| RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
-        [Γ > Δ >                         Σ |- [σ₁∼∼σ₂:κ⇒ σ @@l]]
-| RLetRec        : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
-| RCase          : forall Γ Δ lev n tc Σ avars tbranches
-  (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)),
+        [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
+| RCase          : forall Γ Δ lev tc Σ avars tbranches
+  (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
-                       ((mapOptionTree cbri_judg alts),,
-                        [Γ > Δ >                                               Σ |- [ caseType tc avars @@ lev ] ])
-                        [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
+                       ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
+                        [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
+                        [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 .
 Coercion RURule : URule >-> Rule.
 
@@ -118,18 +122,21 @@ Coercion RURule : URule >-> Rule.
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
-| Flat_RNote            : ∀ x y z              ,  Rule_Flat (RNote x y z)
+| Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
+| Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
-| Flat_RLam             : ∀ Γ Δ  Σ tx te    q    l,  Rule_Flat (RLam Γ Δ  Σ tx te      q l)
-| Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q    l,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q l)
+| Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
+| Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 | Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
-| Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    l,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q l)
-| Flat_RAppCo           : ∀ Γ Δ  Σ κ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ κ σ₁ σ₂ σ γ  q l)
-| Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2 q3 x )
+| Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
+| Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
+| Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 | Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
-| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q).
+| Flat_REmptyGroup      : ∀ q a                  ,  Rule_Flat (REmptyGroup q a)
+| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
+| Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 
 (* given a proof that uses only uniform rules, we can produce a general proof *)
 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
@@ -156,12 +163,12 @@ Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
   intro.
   intro.
   induction 1; intros.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
 
   apply IHX.
   destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
@@ -175,9 +182,9 @@ Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
     inversion e.
     exists c1. exists c2. auto.
 
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
+  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
   Qed.
 
 Lemma no_rules_with_multiple_conclusions : forall c h,
@@ -205,6 +212,7 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
+    destruct X0; destruct s; inversion e.
     Qed.
 
 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.