Require Import HaskStrong.
Require Import HaskProof.
-Axiom fail : forall {A}, string -> A.
- Extract Inlined Constant fail => "Prelude.error".
-
Section HaskStrongToProof.
(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
* expansion on an entire uniform proof *)
-Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ))
+Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
:= @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
-Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ))
+Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
:= @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
Definition pivotContext {Γ}{Δ} a b c τ :
Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
match exp as E in Expr Γ Δ ξ τ with
+ | EGlobal Γ Δ ξ _ _ => []
| EVar Γ Δ ξ ev => [ev]
| ELit Γ Δ ξ lit lev => []
| EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
- | ELam Γ Δ ξ t1 t2 lev v pf e => stripOutVars (v::nil) (expr2antecedent e)
+ | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
| ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
| EEsc Γ Δ ξ ec t lev e => expr2antecedent e
| EBrak Γ Δ ξ ec t lev e => expr2antecedent e
- | ECast Γ Δ ξ γ t1 t2 lev wfco e => expr2antecedent e
+ | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
| ENote Γ Δ ξ t n e => expr2antecedent e
| ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
- | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => expr2antecedent e
- | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => expr2antecedent e
- | ETyApp Γ Δ κ σ τ ξ l pf e => expr2antecedent e
+ | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
+ | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
+ | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
| ELetRec Γ Δ ξ l τ vars branches body =>
let branch_context := eLetRecContext branches
in let all_contexts := (expr2antecedent body),,branch_context
in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
- | ECase Γ Δ ξ lev tc avars tbranches e' alts =>
+ | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
((fix varsfromalts (alts:
- Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc avars
+ Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
& Expr (sac_Γ scb Γ)
- (sac_Δ scb Γ avars (weakCK'' Δ))
- (scbwv_ξ scb ξ lev)
- (weakLT' (tbranches@@lev)) }
+ (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l)
+ (weakLT' (tbranches@@l)) }
): Tree ??VV :=
match alts with
| T_Leaf None => []
with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => expr2antecedent e
+ | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
end.
-(*
-Definition caseBranchRuleInfoFromEStrongAltCon
- `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
- @StrongAltConRuleInfo n tc Γ lev tbranches.
- set (ecase2antecedent _ _ _ _ _ _ _ _ ecb) as Σ.
- destruct ecb.
- apply Build_StrongAltConRuleInfo with (pcb_scb := alt)(pcb_Σ := mapOptionTree ξ Σ).
- Defined.
-
-Definition judgFromEStrongAltCon
- `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
- Judg.
- apply caseBranchRuleInfoFromEStrongAltCon in ecb.
- destruct ecb.
- eapply pcb_judg.
- Defined.
-
-Implicit Arguments caseBranchRuleInfoFromEStrongAltCon [ [Γ] [Δ] [ξ] [lev] [tc] [avars] [tbranches] ].
-*)
-Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
-Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ) :=
+Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
+ (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
+ & Expr (sac_Γ scb Γ)
+ (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l)
+ (weakLT' (tbranches@@l)) })
+ : ProofCaseBranch tc Γ Δ l tbranches atypes.
+ exact
+ {| pcb_scb := projT1 alt
+ ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
+ |}.
+ Defined.
+
+Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev]
+ | ELR_leaf Γ Δ ξ lev v e => [ξ v]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
end.
Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [v]
+ | ELR_leaf Γ Δ ξ lev v e => [v]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
end.
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ):=
+Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
match elrb with
| ELR_nil Γ Δ ξ lev => []
- | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)]
+ | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)]
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
end.
Lemma stripping_nothing_is_inert
{Γ:TypeEnv}
- (ξ:VV -> LeveledHaskType Γ)
+ (ξ:VV -> LeveledHaskType Γ ★)
tree :
stripOutVars nil tree = tree.
induction tree.
v (* variable to be pivoted, if found *)
ctx (* initial context *)
τ (* type of succedent *)
- (ξ:VV -> LeveledHaskType Γ)
+ (ξ:VV -> LeveledHaskType Γ ★)
:
(* a proof concluding in a context where that variable does not appear *)
rewrite H.
clear H.
- (* FIXME TOTAL BOGOSITY *)
+ (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
assert ((stripOutVars (leaves v2) v1) = v1).
admit.
rewrite H.
Definition update_ξ'' {Γ} ξ tree lev :=
(update_ξ ξ
- (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩)
+ (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
(leaves tree))).
-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree lev :
+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
= mapOptionTree ξ (stripOutVars (v :: nil) tree).
induction tree; simpl in *; try reflexivity; auto.
Lemma updating_stripped_tree_is_inert'
{Γ} lev
- (ξ:VV -> LeveledHaskType Γ)
+ (ξ:VV -> LeveledHaskType Γ ★)
tree tree2 :
mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
= mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
Lemma updating_stripped_tree_is_inert''
{Γ}
- (ξ:VV -> LeveledHaskType Γ)
+ (ξ:VV -> LeveledHaskType Γ ★)
v tree lev :
mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
= mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree).
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v e,
- (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [((unlev (ξ v) @@ lev))]]) ->
- LetRecSubproofs Γ Δ ξ lev [(v, (unlev (ξ v)))] (ELR_leaf _ _ _ _ _ _ e)
+ (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
+ LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
| lrsp_cons : forall t1 t2 b1 b2,
LetRecSubproofs Γ Δ ξ lev t1 b1 ->
LetRecSubproofs Γ Δ ξ lev t2 b2 ->
LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
-Lemma dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
-
+Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
eLetRecTypes branches =
mapOptionTree (update_ξ'' ξ tree lev)
(mapOptionTree (@fst _ _) tree).
admit.
admit.
Qed.
+Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
+mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
+=
+(*
+((mapOptionTreeAndFlatten
+(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
+ (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
+*)
+((mapOptionTreeAndFlatten pcb_freevars
+ (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
+admit.
+Qed.
+Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
+ admit.
+ Qed.
+Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
+admit.
+Qed.
Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
: LetRecSubproofs Γ Δ ξ lev tree branches ->
induction X; intros; simpl in *.
apply nd_rule.
apply REmptyGroup.
- unfold mapOptionTree.
- simpl.
+ set (ξ v) as q in *.
+ destruct q.
+ simpl in *.
+ assert (h0=lev).
+ admit.
+ rewrite H.
apply n.
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
Defined.
-Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ) tree z lev,
+Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
admit.
Qed.
intro pf.
intro lrsp.
set ((update_ξ ξ
- (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩)
+ (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
(leaves tree)))) as ξ' in *.
set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
set (mapOptionTree (@fst _ _) tree) as pctx.
eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
- rewrite dork in q.
+ rewrite cheat1 in q.
set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
unfold update_ξ'' in *.
rewrite <- zz in q.
apply q.
Defined.
-(*
-Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx),
- unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars).
-admit.
+
+Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
+ mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
+ (stripOutVars (vec2list (scbwv_exprvars x)) t)
+ =
+ mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) t).
+ admit.
Qed.
-*)
-Lemma cheat : forall {T} (a b:T), a=b.
- admit.
- Defined.
+
+
+Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
+(x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
+(e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
+ (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) ,
+mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
+unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
+=
+mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
+ mapOptionTree
+ (update_ξ (weakLT' ○ ξ)
+ (vec2list
+ (vec_map
+ (fun
+ x0 : VV *
+ HaskType
+ (app (vec2list (sac_ekinds x)) Γ)
+ ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩)
+ (vec_zip (scbwv_exprvars x)
+ (sac_types x Γ atypes)))))
+ (unleaves (vec2list (scbwv_exprvars x)))
+.
+admit.
+Qed.
+
+
+
Definition expr2proof :
forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
: ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
match exp as E in Expr Γ Δ ξ τ with
+ | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
| EVar Γ Δ ξ ev => let case_EVar := tt in _
| ELit Γ Δ ξ lit lev => let case_ELit := tt in _
| EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
- let e1' := expr2proof _ _ _ _ e1 in
- let e2' := expr2proof _ _ _ _ e2 in _
- | ELam Γ Δ ξ t1 t2 lev v pf e => let case_ELam := tt in
- let e' := expr2proof _ _ _ _ e in _
+ (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
+ | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
| ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
- let pf_let := (expr2proof _ _ _ _ ev) in
- let pf_body := (expr2proof _ _ _ _ ebody) in _
+ (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
| ELetRec Γ Δ ξ lev t tree branches ebody =>
- let e' := expr2proof _ _ _ _ ebody in
let ξ' := update_ξ'' ξ tree lev in
- let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ''))
+ let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
+((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
(branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
: LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
- | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
- | ELR_leaf Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e)
- | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
+ | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
+ | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
+ | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
end
- ) _ _ _ _ tree branches) in
- let case_ELetRec := tt in _
- | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _
- | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _
- | ECast Γ Δ ξ γ t1 t2 lev wfco e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _
- | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _
- | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _
- | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _
- | ETyApp Γ Δ κ σ τ ξ l pf e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _
- | ECase Γ Δ ξ lev tbranches tc avars e alts =>
-(*
+ ) _ _ _ _ tree branches)
+ | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
let dcsp :=
((fix mkdcsp (alts:
- Tree ??{ scb : StrongCaseBranchWithVVs tc avars
+ Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
& Expr (sac_Γ scb Γ)
- (sac_Δ scb Γ avars (weakCK'' Δ))
- (scbwv_ξ scb ξ lev)
- (weakLT' (tbranches@@lev)) })
- : ND Rule [] (mapOptionTree judgFromEStrongAltCon alts) :=
- match alts as ALTS return ND Rule [] (mapOptionTree judgFromEStrongAltCon ALTS) with
+ (sac_Δ scb Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l)
+ (weakLT' (tbranches@@l)) })
+ : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
+ match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
| T_Leaf None => let case_nil := tt in _
| T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
- | T_Branch b1 b2 => let case_branch := tt in _
- end) alts)
- in *) let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+ | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
+ end) alts')
+ in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
end
-); clear exp ξ' τ' Γ' Δ'; simpl in *.
+); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+
+ destruct case_EGlobal.
+ apply nd_rule.
+ simpl.
+ destruct t as [t lev].
+ apply (RGlobal _ _ _ _ wev).
destruct case_EVar.
apply nd_rule.
eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; auto.
+ apply e1'.
+ apply e2'.
destruct case_ELam; intros.
unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
apply n.
auto.
inversion H.
- apply pf.
- destruct case_ELet; intros.
+ destruct case_ELet; intros; simpl in *.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod; [ idtac | apply pf_let].
apply e'.
destruct case_ECast.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast with (γ:=γ)].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
apply e'.
auto.
destruct case_ENote.
+ destruct t.
eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
apply e'.
auto.
- destruct case_ETyApp; intros.
+ destruct case_ETyApp; simpl in *; intros.
eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
apply e'.
auto.
- destruct case_ECoLam; intros.
+ destruct case_ECoLam; simpl in *; intros.
eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
apply e'.
- auto.
- auto.
- destruct case_ECoApp; intros.
- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) σ₁ σ₂ σ γ l) ].
+ destruct case_ECoApp; simpl in *; intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
apply e'.
auto.
unfold mapOptionTree.
apply e'.
+ destruct case_leaf.
+ unfold pcb_judg.
+ simpl.
+ repeat rewrite <- mapOptionTree_compose in *.
+ set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
+ (unleaves (vec2list (scbwv_exprvars (projT1 x))))
+ (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
+ _ _
+ ))) as q.
+ rewrite cheat4 in q.
+ rewrite cheat3.
+ unfold weakCK'' in q.
+ simpl in q.
+ rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q.
+ Ltac cheater Q :=
+ match goal with
+ [ Q:?Y |- ?Z ] =>
+ assert (Y=Z) end.
+ cheater q.
+ admit.
+ rewrite <- H.
+ clear H.
+ apply q.
+
+ destruct case_nil.
+ apply nd_id0.
+
+ destruct case_branch.
+ simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply b1'.
+ apply b2'.
+
destruct case_ECase.
- unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
- apply (fail "ECase not implemented").
- (*
+ rewrite cheat2.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
rewrite <- mapOptionTree_compose.
apply dcsp.
apply e'.
- *)
- destruct case_elr_leaf; intros.
- assert (unlev (ξ0 v) = t0).
- apply cheat.
- set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q.
- rewrite H in q.
- apply q.
- apply e'0.
-
- destruct case_ELetRec; intros.
+ destruct case_ELetRec; simpl in *; intros.
set (@letRecSubproofsToND') as q.
simpl in q.
apply q.
apply e'.
apply subproofs.
- (*
- destruct case_leaf.
- unfold pcb_judg.
- simpl.
- clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u.
- repeat rewrite <- mapOptionTree_compose in *.
- set (nd_comp ecb'
- (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q.
- idtac.
- assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
- apply update_ξ_and_reapply.
- rewrite H.
- simpl in q.
- unfold mapOptionTree in q; simpl in q.
- set (@updating_stripped_tree_is_inert''') as u.
- unfold mapOptionTree in u.
- rewrite u in q.
- clear u H.
- unfold weakenX' in *.
- admit.
- unfold mapOptionTree in *.
- replace
- (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0))
- with
- (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
- apply q.
- apply cheat.
-
- destruct case_branch.
- simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply nd_prod.
- apply (mkdcsp b1).
- apply (mkdcsp b2).
- *)
-
Defined.
End HaskStrongToProof.
-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
-| DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
-| DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
- mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
projects / coq-hetmet.git / blobdiff